智能合约函数的建模与验证研究

叶昊榀，刘 阳

(南京财经大学信息工程学院，江苏 南京 210023)

1 引言

近年来区块链技术得到了快速的发展与推广。作为可编程金融的区块链2.0时代的代表技术[1]，智能合约在不远的未来将得到大量的推广与应用。智能合约无需可信中介、可以控制并处理大量的数字资产与交易，具有很高的经济价值。截至目前，市面上最为流行的智能合约应用平台以太坊的市值已经超过1800亿美元、完成了6.75亿次交易。智能合约极高的经济价值也吸引了大量的不法分子利用智能合约本身存在的漏洞实施非法攻击从而窃取数字资产。据相关研究表明，目前约有89%的智能合约都含有安全性漏洞，保守估计这些安全性漏洞所导致的损失已超过20亿美元[2]。为了给智能合约提供高层次的保障性，使用形式化方法对智能合约进行验证成为了许多学者的选择。Nicola Atzei等人[3]从Solidity语言、EVM和区块链三个层次对以太坊智能合约所存在的安全性隐患进行了总结。Joshua Ellul 和 Gordon Pace[4]展示了如何在智能合约领域中应用运行时验证的标准化技术。胡凯等人[5]提出了一种可以应用于智能合约生命周期的形式化验证框架和验证方法。Anastasia Mavridou[6]提出了用于智能合约形式化验证的VeriSolid框架、该框架同样支持对合约函数体进行建模。Anton Permenev等人[7]提出了VERX，能够证明以太坊智能合约的函数属性的自动验证器。Thomas Osterlanda等人[8]提出对Solidity语言的语义语法的形式化定义，并提出了一种将Solidity语言建模为PROMELA模型的转换方法。Zheng Yang等人[9]发展并证明了一种用于证明以太坊智能合约的可靠性与安全性的全新的形式化符号进程虚拟机。……