技术篇|智能合约安全问题以及解决办法

智能合约极大地扩展了区块链的应用场景与现实意义，但频发的安全事故严重阻碍了它的发展，智能合约安全性问题的研究就显得尤为关键。本文讨论了形式化验证、模糊测试和符号执行等主流的智能合约漏洞检测手段，对于象链科技当前联盟链安全性问题的研究方向有着深远的指导意义，并明确了下一步工作的目标，采用不同的检测方法组合，着力提高漏洞挖掘的准确性、效率和自动化程度，满足智能合约规模和复杂度与日俱增的漏洞挖掘需求。

1智能合约安全性问题

随着智能合约数量的增多，去中心化应用（Decentralized Application， DApp）的推广，智能合约涉及的数字资产呈指数级别增长。相比传统软件，智能合约的安全问题更加棘手，现实情况也更加严峻。

1）智能合约的可信度源自其不可篡改性，一旦被部署上线便无法修改。任何人都可对合约存在的安全漏洞发起攻击，如果合约没有相应的防御措施，便将无法遏止安全问题的恶化，从而严重损害合约本身的经济价值以及公众对项目的信任。

2）很多项目会公开智能合约源码。源码的公开透明虽能提升用户对合约的信任度，却也大幅度降低了黑客攻击的成本，每一个暴露在开放网络上的智能合约都有可能成为专业黑客团队的金矿和攻击目标。

3）智能合约的开发过程存在纰漏。由于起步晚，发展时间短，智能合约本身就有很多不足;同时市面上专业的技术人员严重匮乏，不严谨的代码参考、拷贝和修改等人为因素都会引起漏洞。

智能合约中出现频率最高的10类安全问题为分别：代码重入、访问控制、整数溢出、未严格判断不安全函数调用返回值、拒绝服务（Denial of Service， DoS）、可预测的随机处理、竞争条件/非法预先交易、时间戳依赖、短地址攻击以及其他未知漏洞类型。

2智能合约漏洞检测手段及相关工作

出于“代码即规则”，智能合约一旦被部署便不可更改，即便有恶意交易被记录下来，也不可以将其从区块链中删除。回滚交易的唯一方法是执行硬分叉，即通过修改区块链中的共识协议把区块链中的数据恢复到过去某一状态，而这无法回避开发者客观上存在滥用“专业垄断”的质疑，一定程度上冲击了区块链系统去中心化的理念。

因此必须在智能合约上线之前，对其进行全面深入的代码安全审计与测试，充分分析潜在的安全威胁，尽可能规避漏洞。

针对智能合约安全问题，应该从开发人员使用安全库进行开发、安全团队开展合约测试、合约审计这三个角度采取措施。

2.1 形式化验证

形式化验证用逻辑语言对智能合约文档和代码进行形式化建模，通过严密的数学推理逻辑和证明，检查智能合约的功能正确性和安全属性，克服了用传统测试手段无法穷举所有可能输入的缺陷，能完全覆盖代码的运行期行为，可以确保在一定范围内的绝对正确，弥补了合约测试和合约审计工作的局限性，因此形式化验证已初步应用于高铁、航天、核电等安全攸关的领域，并且取得了非常好的效果。

Bhargavan等提出了一个智能合约分析和验证框架，该框架通过Solidity*和EVM*工具将智能合约源码和字节码转化成函数编程语言F*，以便分析和验证合约运行时安全性和功能正确性。目前，Coq、Isabelle/HOL、Why3等工具也实现了EVM的语义表示，并做了一些形式化验证智能合约的工作。

2.2 模糊测试

模糊测试是一种通过构造非预期的输入数据并监视目标软件在运行过程中的异常结果来发现软件故障的方法。对智能合约进行模糊测试时，利用随机引擎生成大量的随机数据，构成可执行交易，参考测试结果的反馈，随机引擎动态调整生成的数据，从而探索尽可能多的智能合约状态空间。基于有限状态机分析每一笔交易的状态，检测是否存在攻击威胁。自动化工具Echidna采用了模糊测试技术来对EVM字节码进行检测，但是不能保证API功能的稳定性。

2.3 符号执行

符号执行的核心思想是使用符号值代替具体值执行程序。对于程序分析过程中任意不确定值的变量，包括环境变量和输入等，都可以用符号值代替。符号执行中的“执行”是指解析程序可执行路径上的指令，根据其语义更新程序执行状态，等同于解释执行[19]。借助符号执行检测智能合约漏洞的一般过程为，首先将按需将智能合约中不确定值的变量符号化，然后逐条解释执行程序中的指令，在解释执行过程中更新执行状态、搜集路径约束，并在分支节点处做fork执行，以完成程序中所有可执行路径的探索，发现安全问题。约束求解技术能够对符号执行中搜集的路径约束进行求解，判断路径是否可达，并在特定的程序点上检测变量的取值是否符合程序安全的规定或者可能满足漏洞存在的条件。

2.4 污点分析

本质上来说，污点分析是针对污点变量的数据流分析技术。污点分析的一般流程为：首先识别污点信息在智能合约中的产生点并对其进行标记;然后按照实际需求和污点传播规则进行前向或后向数据依赖分析，得到污点的数据依赖和被依赖关系的指令集合;最终在一些关键的程序点检查关键的操作是否会受到污点信息的影响。

3未来研究方向与改进思路

1）扩展形式化验证的应用范围。

对于目前学术界颇为关注的形式化验证方法，用数学推演来验证复杂系统，安全有效但难度很高。未来的研究应针对不同的业务目标定制对应的验证规范描述，突破成本昂贵、不适应大规模合约等技术限制，并扩展形式化验证的应用范围，从验证一般功能属性和安全属性、检测常见漏洞到逐步实现经济学、博弈论范畴中复杂业务逻辑及公平性等高阶性质的证明。

2）提取重点路径，缩减路径空间。

基于攻击者目标是非法窃取加密货币的假设，结合现有智能合约审计经验和已曝漏洞分析，寻找智能合约中易产生漏洞的高危指令，如SUICIDE、CALL、ORIGIN、ASSERT_FAIL等，定义涉及这些操作码的路径为重点路径。为了提高漏洞挖掘效率，实践中不必对所有可能的执行路径进行检查，仅符合执行关注的重点路径并进行漏洞验证，可以有效地缩减路径空间。

3）符号执行辅助的模糊测试。

现有的工具通常是对一种典型方法的具体实现，但是在执行具体漏洞挖掘任务时，因需求和重点不同，使用不同的辅助工具或者不同的检测方法组合往往能达到更好的效果。

未来可以研究动态符号执行辅助的模糊测试技术，使用动态符号执行弥补模糊测试理解语义的缺失，推断出到达特定程序状态的约束条件，通过约束求解产生能够触发测试者所关注逻辑的合理输入。据此恰当地改变模糊测试的输入，提供额外的测试用例，触发先前未覆盖的代码区域，因此本文设计一种符号执行辅助的智能合约模糊测试框架。

4）完善智能合约漏洞库，建立漏洞挖掘工具效率评价方法。

当前关于智能合约的测试尚未有标准的案例集，因此，为了验证智能合约漏洞挖掘工具的有效性，同时给智能合约的安全开发提供参考，下一步工作需要根据已爆发的安全事件以及合约审计经验，总结归纳出涵盖类型完善的智能合约漏洞库。

参考文献：

[1]NCC Group. Decentralized application security project top 10 of 2018 [EB/OL]. （2018-07-08） [2018-09-08]. https：//www.dasp.co/index. html.

[2]SECBIT. Frequent smart contracts events， security development requires standardization [EB/OL]. （2018-05-07）?[2018-10-20]. https：//www.jianshu.com/p/9d78f5110af1.

[3]MANNING A. Solidity security：comprehensive list of known attack vectors and common anti-patterns [EB/OL]. （2018-05-30） [2019-01-03]. https：//blog.sigmapri-me.io/solidity-security.html.

[4]ARIAS L， SPAGNUOLO F， GIORDANO F， et al. OpenZeppelin [EB/OL]. （2016-07-31）[2018-12-06]. https：//github.com/ OpenZeppelin/openzeppelin-Solidity.

[5]ATZEI N， BARTOLETTI M， CIMOLI T. A survey of attacks on Ethereum smart contracts （SoK） [C]// Proceedings of the 2017 International Conference on Principles of Security and Trust. Berlin：Springer， 2017：164-186.

[6]FEY G. Assessing system vulnerability using formal verification techniques[C]// Proceedings of the 2011 International Conference on Mathematical and Engineering Methods in Computer Science. Berlin：Springer， 2011：47-56.

[7]CSDN Research and Development Technology. Formal verification is a sharp weapon for smart contracts safety [EB/OL]. （2018-06-12） [2018-09-08]. https：//blog.csdn.net /CDLianan/article/details/80665162.

[8]BHARGAVAN K， SWAMY N， ZANELLA B S， et al. Formal verification of smart contracts：short paper[C]// Proceedings of the 2016 Association for Computing Machinery Workshop. New York：ACM， 2016：91-96.

[9]YANG X， YANG Z， SUN H Y， et al. Formal verification for Ethereum smart contract using Coq[J]. International Journal of Information and Communication Engineering， 2018， 12（6）：125-130

- END-

关于象链科技

象链科技（上海）有限公司，是一家快速成长的区块链领先企业，一直以“区块链技术 服务民生”为理念，致力于区块链基础研究和应用研发，为人工智能、智慧城市、智慧政务、民生服务的发展助力。象链科技的愿景是打造区块链+人工智能数字经济新生态，拥有首个融合ABCD（A-AI B-Blockchain C-Cloud D-BigData）产业的高性能自主研发公链底层兼容联盟链平台EleChain。

—-

编译者/作者：象链科技

玩币族申明：玩币族作为开放的资讯翻译/分享平台，所提供的所有资讯仅代表作者个人观点，与玩币族平台立场无关，且不构成任何投资理财建议。文章版权归原作者所有。