Luu L, Chu D H, Olickel H, et al. Making Smart Contracts Smarter[C]// Acm Sigsac Conference on Computer Communications Security. 2016.
论文摘要：
加密货币在称为区块链的分散数据结构中记录交易。两种最流行的加密货币，即比特币和以太坊，它们支持对处理交易的规则或脚本进行编码的功能。此功能已经发展为实际形成智能合约或在区块链上运行的完整程序的想法。 最近，以太坊的智能合约系统已经稳步采用，支持数以万计的合约，持有价值数百万美元的虚拟硬币。
本文研究了基于以太坊的智能合约在加密货币等开放分布式网络中运行的安全性。我们引入了几个新的安全问题，其中攻击者可以操纵智能合约执行来获取利润。这些错误表明在理解底层平台的分布式语义方面存在细微的差距。作为一种改进，我们提出了增强以太坊操作语义的方法，以减少合同的脆弱性。对于为现有以太坊系统编写合同的开发人员，我们构建一个名为Oyente的符号执行工具，以发现潜在的安全漏洞。在现有的19366份以太坊合同中，Oyente将其中8833份标为易受攻击，包括导致2016年6月损失6000万美元的TheDAO漏洞。我们还讨论了几个案例研究中其他攻击的严重性，这些案例研究具有可用的源代码，并确认了主要以太坊网络中的攻击（仅针对我们的帐户）。
技术介绍：
在本文中，我们记录了以太坊智能合约的几个新安全漏洞（交易订购依赖
、时间戳依赖性、错误处理的例外情况和可重入漏洞），并举例说明了每个问题的实际实例。这些安全漏洞使合同容易被多方（包括矿工和合同用户）滥用。我们认为这些缺陷在实践中出现是因为合同编写者对底层执行语义的假设与智能合约系统的实际语义之间存在语义差异。具体来说，我们将展示不同的各方如何利用具有不同输出状态的合同，具体取决于事务的顺序和输入块时间戳。据我们所知，这些语义差距以前没有被确定过。我们还记录了其他严重但已知的问题，例如不正确处理的中止/异常和逻辑缺陷。以前的工作在概念上进行了讨论，通常用简单的自构建实例[1]。在我们的工作中，我们研究了它们对成千上万的现实合同的影响，展示了这些漏洞如何被用来破坏或窃取良性用户的硬币。
更重要的是，我们的工作强调智能合约语义中的微妙和/或缺失的抽象，导致开发人员产生错误的安全感。我们建议改进以太坊的协议，不需要更改现有的智能合约。但是，此类解决方案确实需要网络中的所有客户端进行升级，因此存在无法看到实际部署的风险。如果这样的要求是不可接受的，我们提供了一个名为Oyente的工具，供用户在部署前缓解中检测错误。 Oyente是一个专门用于分析以太坊智能合约的符号执行工具。它遵循以太坊智能合约的执行模型[2]，并直接与以太坊虚拟机（EVM）字节码一起使用，无需访问高级表示（例如，Solidity [3]，Serpent [4]）。这种设计选择至关重要，因为以太坊区块链只存储合同的EVM字节代码，而不是它们的来源。 Oyente是开源的，很快就会从我们的项目页面上公开使用[5]。
Oyente工具来帮助：（1）开发人员编写更好的合同; （2）用户避免调用有问题的合同。 重要的是，其他分析也可以作为独立插件实现，而不会干扰我们现有的功能。 例如，Oyente的直接扩展是计算更精确的合同最坏情况气体消耗估算。
我们的分析工具基于符号执行[6]。符号执行将程序变量的值表示为输入符号值的符号表达式。每个符号路径都有一个路径条件，它是通过累积约束构建的符号输入的公式。那些输入必须满足，以便执行遵循该路径。 如果路径条件不可满足，则路径是不可行的。 否则，路径是可行的。
我们选择符号执行，因为它可以逐个路径地静态推理程序。 一方面，这优于动态测试，这是关于程序输入的原因。对于以太坊，动态测试甚至需要更多的努力来模拟执行环境。 例如，为了检测事务排序依赖性，我们必须比较不同执行路径的交错结果。考虑到区块链行为的非确定性和复杂性，很难通过动态测试来解决这个问题。
另一方面，通过一次推理一条路径，与使用静态污点分析或一般数据流分析的传统方法相比，符号执行可以实现更好的精度（或更少的误报）。 在这些方法中，抽象程序状态经常被合并，承认从未在真实执行中发生的状态，并最终导致高误报。
图1：概述Oyente的体系结构。主要部件位于虚线区域内。阴影框是公开的。
设计概述
图1描绘了Oyente的架构概述。它需要两个输入，包括要分析的合同的字节码和当前的以太坊全局状态。 它回答合同是否存在任何安全问题（例如，TOD，时间戳依赖性，错误处理的异常），向用户输出“有问题”的符号路径。 我们工具的一个副产品是合同字节码的控制流图（CFG）。 我们计划在未来Oyente将能够作为交互式调试器工作，因此我们将CFG和有问题的路径提供给图形可视化工具.
字节码在区块链上公开，Oyente解释EVM指令集，以便将指令忠实地映射到约束，即位级精度。以太坊全局状态提供契约变量的初始化（或当前）值，从而实现更精确的分析。包括值、消息调用数据在内的所有其他变量都被视为输入符号值。
Oyente采用模块化设计。 它由四个主要组件组成，即CFG Builder，Explorer，Core Analysis和Validator。 CFG Builder构造契约的控制流图，其中节点是基本执行块，边表示块之间的执行跳转。 Explorer是我们的主要模块，象征性地执行合同。 然后将Explorer的输出提供给Core Analysis，我们在其中实现我们的逻辑以针对第3节中确定的漏洞。最后，Validator在向用户报告之前过滤掉一些误报.
本文作出以下贡献：我们在以太坊智能合约中记录了几类新的安全漏洞。我们将以太坊智能合约的语义形式化，并提出建议作为记录错误的解决方案。我们提供Oyente，一种象征性执行工具，用于分析以太坊智能合约以检测错误。我们在真正的以太坊智能合约上运行Oyente并确认真实以太坊网络中的攻击。
参考文献：
[1] Kevin Delmolino, Mitchell Arnett, Ahmed Kosba,Andrew Miller, and Elaine Shi. Step by step towards creating a safe smart contract: Lessons and insights from a cryptocurrency lab. Cryptology ePrint Archive,Report 2015/460, 2015. http://eprint.iacr.org/.
[2] Gavin Wood. Ethereum: A secure decentralized generalised transaction ledger.
http://gavwood.com/paper.pdf, 2014.
[3] Ethereum Foundation. The solidity contract-oriented programming language.
https://github.com/ethereum/solidity
[4] Ethereum Foundation. The serpent contract-oriented programming language.
https://github.com/ethereum/serpent
[5] Oyente project page.https://www.comp.nus.edu.sg/˜loiluu/oyente.html.
[6] James C. King. Symbolic execution and program testing. Commun. ACM, 19(7):385–394.
致谢
本文由南京大学软件学院2019级硕士生刘芳潇翻译转述
添加新手交流群：币种分析、每日早晚盘分析
添加助理微信，一对一亲自指导：YoYo8abc
