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

• 作者: 王赫彬 郑长友 黄松 孙金磊 丁一先
• 来源期刊: 计算机技术与发展
• 关键词: 以太坊 智能合约 形式化验证 定理证明 模型检测
• 年，卷（期）: 2021,（9）
• 所属期刊栏目: 网络与安全
• 页码范围: 104-111
• 页数: 8页
• 分类号: TP309|TP311
• 语种: 中文
• DOI: 10.3969/j.issn.1673-629X.2021.09.018

摘要

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