一种代币智能合约的形式化建模与验证方法  

A Formal Modeling and Verification Method for Token Smart Contract

作　　者：欧阳恒一 熊焰[2] 黄文超[2] OUYANG Hengyi;XIONG Yan;HUANG Wenchao(School of Cyberspace Security,University of Science and Technology of China,Hefei 230026,China;School of Computer Science and Technology,University of Science and Technology of China,Hefei 230026,China)

机构地区：[1]中国科学技术大学网络空间安全学院,合肥230026 [2]中国科学技术大学计算机科学与技术学院,合肥230026

出　　处：《计算机工程》2020年第10期41-45,51,共6页Computer Engineering

基　　金：国家自然科学基金(61972369,61572453,61520106007,61572454);国家重点研发计划(2018YFB2100300)。

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

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

分 类 号：TN915.08[电子电信—通信与信息系统]