王赫彬，郑长友，黄 松，孙金磊，丁一先

(1.中国人民解放军陆军工程大学 指挥控制工程学院，江苏 南京 210007；2.中国人民解放军陆军工程大学 全军军事训练软件测评中心，江苏 南京 2100073.辽宁工程技术大学，辽宁 阜新 123000)

0 引 言

自2009年Satoshi Nakamoto的比特币发布以来，出现了各种各样的区块链实现。而自从2013年底Vitalik Buterin发布的以太坊白皮书将智能合约的概念引入到区块链之中，区块链技术的应用变得更加广泛，并使得比特币等加密货币的可编程能力更进一步。智能合约提供了一个框架，允许以可信任、去中心化的方式执行一个应用程序的业务逻辑。智能合约用户通常携带大量的价值数以亿计的货币，但是智能合约作为一种计算机代码可能具有未发现的和未知的漏洞，具有很大的安全隐患。2016年6月17日的The DAO攻击事件中，一名攻击者利用去中心化自治组织(decentralized autonomous organization，DAO)部署的智能合约代码中的多个漏洞，控制了当时价值约为5 000万美元的以太坊网络，并从合约中盗走了350多万以太币；2018年美链BEC上百亿项目归零、BAI(blockchain of artificial intelligence and internet of things)任意账户无限转账都是因为ERC20代币标准中出现的一系列漏洞，导致资金恶意发送转移，正常的矿工节点受到了危害。对于难以避免的智能合约安全性问题来说，在部署链上前发现并修复漏洞至关重要。

虽然现有的一些工作通过基于测试的检测方法来检测漏洞，但不能完备地发现智能合约源码和字节码中所有的漏洞，而且对于智能合约在一些概念和属性的正确表达缺乏全面的检查。……