摘要： 针对代币智能合约的安全问题，提出一种基于代币智能合约整数溢出漏洞的形式化建模与验证方法。分析现有The DAO和BEC等漏洞攻击事件，定义代币智能合约的安全属性，通过引入全局变量和数值比较等约束条件对代币智能合约的建模语言进行扩展，使其支持智能合约各类语句的形式化表示。借鉴数学归纳法的思想，优化SmartVerif模型验证过程，避免状态空间的无限遍历。实验结果表明，该方法能成功找出代币智能合约的整数溢出漏洞，并且具有较强的通用性。

关键词: 智能合约, 代币, 形式化建模, 形式化验证, 整数溢出漏洞

Abstract: To address the frequent security incidents of token smart contracts,this paper proposes a formal modeling and verification method based on integer overflow vulnerabilities of token smart contracts.The DAO and BEC vulnerability attacks are analyzed,and on this basis the security attributes of token smart contracts are defined.Then the method introduces global variables,numeric comparison and other constraints to extend the modeling language of token smart contracts,so as to enable it to support the formal representation of various statements of smart contracts.Finally,the idea of mathematical induction is used to optimize the model verification procedure of the SmartVerif tool in order to avoid infinite traversal of state space.Experimental results show that the proposed method can successfully find out the integer overflow vulnerabilities of token smart contracts,and has strong versatility.

Key words: smart contract, token, formal modeling, formal verification, integer overflow vulnerability

中图分类号: 

• TN915.08