区块链智能合约安全的逆向实时模型检测方法

摘要

区块链中的智能合约具有不可篡改性、去中心化、自治化等优点,使分散应用程序能够在缺乏信任的环境中实现交互和融合.若智能合约自身存在安全隐患,可能会威胁到用户的个人信息和财产安全,造成难以预估的损失.针对智能合约存在的安全问题,提出了基于时间自动机的区块链智能合约安全性的逆向模型检测方法.采用逆向方法对以太坊中的智能合约源代码进行分析,提取合约的逻辑流程,并进一步分析合约是否存有明显的安全隐患,若有则对合约代码进行优化或改进;针对智能合约采用模型检测的方法进行合约建模、性质刻画及自动验证.若验证通过则证明改进合约满足安全性质,否则通过反例找出代码漏洞继续对合约进行优化.以投票合约为实例对所提逆向方法进行具体介绍,证明了所提方法的有效性,能够保证改进后的投票合约系统的完备性与安全性.