论文部分内容阅读
随着以太坊区块链的发展,智能合约作为以太坊的核心技术也得到越来越多的应用,其中应用之一是用户通过代币智能合约进行新代币的开发。除以太币外,在以太坊主流代币标准协议ERC20的基础上,以太坊支持用户通过代币智能合约完成代币的构建发行、管理和交易。代币智能合约种类多,持有大量资金,易受到攻击者的攻击。目前代币智能合约已曝出存在多种类型的漏洞,也发生被攻击的安全事件,造成大量损失,因此保证合约的安全性并对合约进行安全审计是非常必要的。形式化验证方法是专门针对协议或系统的安全性所提出的一种检验分析方法,能够更全面、深入地研究合约的安全性。针对代币智能合约的安全问题,本文以代币智能合约的形式化建模与验证为研究重点,结合以太坊目前主流的ERC20代币标准协议,提出了面向ERC20标准的代币智能合约形式化模型,并将形式化模型应用到对代币智能合约造成威胁的高危漏洞的形式化分析中。具体研究内容如下:1.针对代币智能合约形式化建模的需求,提出了面向ERC20标准的代币智能合约形式化模型框架。描述了模型定义的具体函数行为和攻击者模型,对合约中函数行为进行抽象,利用多集合重写规则定义代币智能合约的建模规则。针对模型需要满足的安全属性,提出了基于ERC20标准的代币智能合约形式化安全属性,包括基本属性、交易属性和权限属性。模型对于分析ERC20标准的代币智能合约的安全性具有实际意义。2.为对代币智能合约造成大量损失的高危漏洞进行验证分析,本文对整数溢出漏洞进行了形式化建模和验证分析,解决了整数溢出漏洞的建模难点,利用上述代币智能合约形式化模型框架完成对整数溢出漏洞的形式化建模。进一步针对整数溢出漏洞隐患提出了相应的改进措施。通过SmartVerif工具完成了合约实例的验证工作,包括存在漏洞的合约和改进后的合约实例,结果表明成功找出合约中的漏洞,以及改进后的合约可避免原合约中存在的攻击。3.为对代币智能合约有高威胁风险的漏洞进行验证分析,本文选取重入漏洞进行了形式化建模和验证分析,结合上述形式化建模框架分析了重入漏洞的安全属性和建模方法,给出了重入漏洞的形式化分析过程,并解决了重入漏洞的建模难点。通过实验验证了具有重入漏洞的合约实例,实验结果表明合约实例均验证出存在安全隐患。进一步针对重入漏洞隐患提出相应改进措施,并对改进后的合约实例进行了验证,结果表明改进措施可避免攻击者攻击。