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

摘要：

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

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

所属期刊栏目：46

分类号：TN915.08

资助基金：国家自然科学基金;国家重点研发计划

在线出版日期：2020-11-06（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：41-45,51