计算机工程

作者：欧阳恒一, 熊焰, 黄文超

单位：中国科学技术大学 a. 网络空间安全学院;b. 计算机科学与技术学院, 合肥 230026

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

基金：国家自然科学基金（61972369，61572453，61520106007，61572454）；国家重点研发计划（2018YFB2100300）。

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

来源：2020年第10期

《计算机工程》期刊编辑部

查看计算机工程杂志2020年第10期