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

Reverse Real-time Model Detection Method for Blockchain Smart Contract Security

作　　者：李书霞 王国卿[1] 庄雷[1] LI Shu-xia;WANG Guo-qing;ZHUANG Lei(School of Information and Engineering,Zhengzhou University,Zhengzhou 450001,China)

机构地区：[1]郑州大学信息工程学院,郑州450001

出　　处：《小型微型计算机系统》2020年第10期2030-2035,共6页Journal of Chinese Computer Systems

基　　金：国家自然科学基金重点项目(U1604262)资助;河南省高等学校重点科研项目(19A520003,20A520038)资助;河南省重点研发与推广专项科技攻关计划项目(182102210189)资助。

摘　　要：区块链中的智能合约具有不可篡改性、去中心化、自治化等优点,使分散应用程序能够在缺乏信任的环境中实现交互和融合.若智能合约自身存在安全隐患,可能会威胁到用户的个人信息和财产安全,造成难以预估的损失.针对智能合约存在的安全问题,提出了基于时间自动机的区块链智能合约安全性的逆向模型检测方法.采用逆向方法对以太坊中的智能合约源代码进行分析,提取合约的逻辑流程,并进一步分析合约是否存有明显的安全隐患,若有则对合约代码进行优化或改进;针对智能合约采用模型检测的方法进行合约建模、性质刻画及自动验证.若验证通过则证明改进合约满足安全性质,否则通过反例找出代码漏洞继续对合约进行优化.以投票合约为实例对所提逆向方法进行具体介绍,证明了所提方法的有效性,能够保证改进后的投票合约系统的完备性与安全性.Smart contracts in the blockchain have the advantages of non-tampering,decentralization,and autonomy,enabling distributed applications to achieve interaction and integration in environments w here trust is lacking.If the smart contract itself has hidden security risks,it may threaten the security of users’personal information and property,causing unpredictable losses.Aiming at the security problem of smart contracts,a reverse model detection method for the security of blockchain smart contracts based on time automata is proposed.Use the reverse method to analyze the smart contract source code in Ethereum,extract the logical flow of the contract,and further analyze w hether the contract has obvious security risks.If so,optimize or improve the contract code;use model detection for smart contracts M ethod for contract modeling,characterization and automatic verification.If the verification is passed,it is proved that the improved contract meets the security nature,otherw ise,the code loopholes are found through counter examples to continue to optimize the contract.Taking the voting contract as an example,the proposed reverse method is specifically introduced,w hich proves the effectiveness of the proposed method and can guarantee the integrity and security of the improved voting contract system.

关 键 词：时间自动机 区块链 智能合约安全 实时模型检测 形式化验证 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]