以太坊智能合约安全形式化验证方法研究进展

来源：计算机技术与发展杂志2021年第09期北京时间：

作者：王赫彬;郑长友;黄摇松;孙金磊;丁一先

单位：1. 中国人民解放军陆军工程大学 指挥控制工程学院,江苏 南京 210007;2. 中国人民解放军陆军工程大学 全军军事训练软件测评中心,江苏 南京 210007;3. 辽宁工程技术大学,辽宁 阜新 123000

摘要：以太坊智能合约是区块链技术的典型应用和实现。 由于智能合约一旦部署就难以修改,智能合约在上链之前的正确性显得至关重要。 虽然很多当前工作都对于智能合约漏洞的检测与预防进行了一系列研究,但是对于检查合约属性和范式的形式化验证方法还没有比较全面的总结。 首先介绍了智能合约基本的表示和编译方式、常用的编程语言、出现的漏洞类型和常见的形式化验证方法,并分析了形式化验证方法在智能合约方面的研究现状;然后,通过实验结果分析验证了两种现有的有界模型检测工具的检测好坏,对于某些具体的合约攻击,漏报率达到 30% 以上,现有形式化验证方法漏报率高、应用范围受限以及验证语言安全性未知等一系列缺陷亟待解决;最后,针对现有形式化验证方法存在的不足之处展望了未来的研究方向。

关键词：以太坊;智能合约;形式化验证;定理证明;模型检测