18.1引用
Kalra, Sukrit & Goel, Seep & Dhawan, Mohan & Sharma, Subodh. (2018). ZEUS: Analyzing Safety of Smart Contracts. 10.14722/ndss.2018.23092.
18.2摘要
一旦部署了智能合约，无论其拥有多少资金，都很难对其进行修补。我们提出了ZEUS，这是一个验证智能合约的正确性和公平性的框架。我们认为正确性是对安全编程实践的坚持，而公平则是对商定的高级业务逻辑的坚持。ZEUS利用抽象解释和符号模型检查以及受约束的horn条款的功能来快速验证合同的安全性。我们为以太坊和Fabric区块链平台构建了ZEUS原型，并通过超过22.4万个智能合约对其进行了评估。我们的评估表明，约94.6％的合同易受攻击。与现有技术相比，ZEUS评估错误率低，分析时间缩短了一个数量级。
18.3介绍
区块链是支撑比特币加密货币的设计模式。但是，使用共识来验证参与者节点之间的交互是需要相互不信任的对等方进行业务而无需受信任的中介的应用的关键推动力。一种这样的用途是启用智能合约，该合约以编程方式编码规则以反映任何类型的多方交互。
尽管智能合约的忠实执行是由区块链的共识协议强制执行的，但参与实体仍具有以下特权：（i）验证智能合约的正确性，即语法实现遵循最佳实践，以及（ii）验证其合法性。公平性，即代码遵循商定的高层业务逻辑进行交互。尽管可以在一定程度上手动审核合同的正确性，但仍然很费力且容易出错。另一方面，自动正式审核需要专用工具和逻辑。与其他分布式系统代码不同，智能合约是不可变的，并且在存在错误的情况下很难修补，而无论持有多少金钱，这一事实使问题更加严重。
我们介绍了ZEUS的设计和实现-ZEUS的实用框架，该框架使用抽象解释和符号模型检查对智能合约进行自动正式验证。ZEUS接受以高级语言编写的智能合约作为输入，并利用用户协助来帮助在XACML样式的模板中生成正确性和/或公平性标准。它将这些合同和策略规范转换为低级中间表示（IR），例如LLVM位代码，对执行语义进行编码以正确地推断出合同行为。然后，它在IR上执行静态分析，以确定必须断言验证谓词（在策略中指定）的点。最后，ZEUS将修改后的IR馈送到验证引擎，该引擎利用受约束的horn条款（CHC）快速确定智能合约的安全性。
18.4ZEUS
ZEUS的智能合同验证工具链包括（a）策略构建器，（b）源代码翻译器和（c）验证器。 具体来说，ZEUS将智能合约和必须对照智能合约进行验证的策略（以规范语言编写）作为输入。它在智能合约代码之上执行静态分析，并将策略谓词作为断言语句插入正确的程序点。 然后，ZEUS利用其源代码转换器将忠实嵌入策略声明的智能合约转换为LLVM位码。 最后，ZEUS调用其验证程序来确定断言冲突，这表明策略冲突。
现在，我们提供ZEUS工作流程的正式概述，并提供其健全性的证明。尽管我们专注于基于Solidity的智能合约，但ZEUS的设计是通用的，适用于以任何源语言编写的合约。
18.4.1规范化Solidity语法
我们定义了一种抽象语言，它捕获了Solidity程序的相关构造。一个程序由一系列合同声明组成。除了对合同专用的持久性存储的声明和初始化之外，每个合同抽象地视为一个或多个方法定义的序列。合同由ID唯一标识，其中ID属于一组标识符。合同的公开方法的调用被视为交易。
18.4.2规范政策语言
将政策翻译为断言。我们的抽象语言包括用于定义智能合约上的状态可达性属性的断言。 ZEUS利用策略元组提取：（a）要断言的谓词（即Cond），以及（b）在程序源中插入断言语句的正确控制位置。
18.4.3正确性
要证明从Solidity合同到具有声明（对应于策略谓词）的抽象语言的转换的正确性，最后到LLVM位代码，则需要执行以下步骤。首先，我们讨论将Solidity代码转换为抽象语言不会影响语义行为。其次，我们认为保守的断言位置不会影响方法的正确性。第三，我们将策略确认问题简化为状态可达性问题。第四，我们在Solidity程序的上下文中提供了状态可达性的定义。第五，我们证明了通过确保程序的近似版本上的状态可访问性，我们不会错过任何程序行为。最后，我们认为，由于我们从这种过分逼近的Solidity程序到LLVM位代码的转换是忠实的从表达式到表达式的转换，因此我们保留了决策程序的整体模数完整性。
18.4.4通过CHC进行符号模型检查
ZEUS使用现有技术发出验证条件作为已翻译程序的CHC。 CHC表示法的优势使其能够与各种基于SMT的求解器和现成的模型检查器进行交互。
18.4.5端到端示例
图1 端到端示例
图1展示了一个端对端示例，其中包含所有程序转换。Solidity代码段将msg.value发送到地址msg.sender并通过从bal [msg.sender]中减去本地余额来更新其本地余额。该示例策略检查发送调用必须满足以下条件：用户的余额必须大于要发送的值。ZEUS从策略条件中提取谓词，并将其作为断言放置在Solidity代码中。随后，它将其转换为抽象语言。最后，ZEUS将该程序转换为LLVM位代码。
18.5实现
如上一节所述，我们实现了ZEUS的原型。我们使用源自Solidity编译器solc的智能合约的AST在C ++中实现策略构建器和Solidity到LLVM位代码转换器。
为了易于实施，我们利用Seahorn作为我们检查策略验证后端的符号模型。我们没有从头开始构建验证器，而是确定Seahorn为我们提供了一种现成的实现，即通过LLVM位代码使用CHC生成验证条件。此外，使用经过测试的bug和性能进行了微调的现有工具，有助于减少ZEUS的错误警报并缩短验证时间。但是，如稍后在小节中所示，ZEUS与Seahorn无关，它可以与对LLVM位码进行操作的任何其他验证程序一起使用。
18.7.1政策制定者
ZEUS从solc解析器中的相应AST节点提取标识符信息（针对主题和对象），以构建策略。该操作是从AST中的函数调用节点提取的，而谓词是从表示二进制操作的节点中的条件提取的。
具体来说，ZEUS在源代码（S）作为Solidity 中合同和运行时定义的全局变量的合同代码上运行污染分析。接收器（F）是对外部API调用的调用，例如发送或可公开调用的函数。ZEUS还捕获源于源并终止于汇的所有流的控制流条件或路径谓词。污点分析过程的输出是一组元组，由源，对象，接收器及其相应的路径谓词组成。ZEUS然后列出所有可用的污染源的集合，即全局变量和环境变量，用户从中选择要跟踪的对象。然后，它会筛选来自异味通过的结果，这些结果会将搜索空间缩小为包含用户选择的至少一个主题的元组。然后，ZEUS提示用户选择对象，然后进一步修剪元组列表。然后，它显示涉及至少一个或多个主题或对象的潜在调用的列表。经过进一步选择，ZEUS列出了从源到接收器遇到的可用谓词。用户可以使用布尔运算符组合这些谓词（或指定自己的谓词）以在策略中形成条件，并指示是否将它们作为前提条件或条件前提进行检查。最后，用户在结果标签中指示规范是确定违规还是接受的行为。
18.7.2Solidity到LLVM的位码转换器
ZEUS接收一个智能合约，并将其通过翻译器，以生成其LLVM位码以及调试符号信息。随后，为了易于实现，它读取策略规范并重写位码（而不是Solidity源代码）以根据规范中的触发属性为谓词注入断言条件。大多数Solidity语句和表达式的语义与C / C ++相同。我们使用丰富的LLVM API在代码编译期间遍历AST时生成语义正确的位码。我们使用标准的LLVM API处理表达式翻译。
保证正确性。在Solidity中，公共功能的执行构成交易，可以在矿工处重新排序。为了听起来不错，ZEUS必须正确推断出程序中所有可能的执行顺序和控制路径。
建模实体语法。ZEUS支持复杂的Solidity语法，包括继承，外部函数，元组表达式，修饰符，对嵌套结构定义的操作，对映射和数组的迭代以及内存分配/取消分配。
LLVM优化。LLVM的优化程序可以执行积极的遍历，从而消除了任何对变量没有影响的非副作用。但是，这可能会对验证结果产生不利影响。此外，验证者可能会调用自己的优化过程，从而可能与Solidity代码中的LLVM位代码转换混淆。为了忠实于合同编写者所设想的语义，ZEUS为每个外部函数返回值创建一个全局变量，并且不对所有函数进行优化。
限制。我们的ZEUS原型在策略规范，翻译和验证方面存在一些限制。
（1）涉及数学公式的公平性较难检查。ZEUS依靠用户来准确定义涉及此类数学表示的策略。
（2）ZEUS忠于大多数Solidity语法。但是，诸如throw和selfdestruct之类的结构没有精确的LLVM位代码转换，则将其建模为程序出口。
（3）ZEUS不支持协定层次结构中的虚函数，即使用super关键字，该关键字根据最终继承图在运行时解析函数调用。
（4）Solidity的汇编块允许将EVM字节码与常规的Solidity语句一起使用。即使现实世界中的合同很少使用组装，ZEUS还是比较保守，不使用组装块来分析合同。
（5）ZEUS支持安全特性的验证，即状态可达性可通过具有整数线性算法的无量词逻辑表示。验证活动性需要支持线性时间逻辑，而ZEUS目前不支持，扩展ZEUS以支持其他类型的属性，例如跟踪或超属性，不需要更改核心设计，我们将其留作将来的工作
18.6评估
所有实验都是在IBM System x3850 X5机器上执行的，该机器具有4.27个Intel Xeon E7-4860 CPU（2.27 GHz），每个CPU10个内核，每个线程2个线程，以及512 GB RAM，运行64位Ubuntu v14.04。 我们基于solc构建了与LLVM 3.6兼容的Solidity到LLVM位代码转换器。 我们使用稳定的Seahorn版本（3月31日的快照）作为验证程序，并将超时阈值设置为1分钟。 为了与Oyente进行比较，我们使用其4月15日可用的快照，并将超时时间保持为30分钟。
基于Solidity的智能合约从以下几个方面进行评估：（1）再入；（2）未经检查的发送；（3）发送失败；（4）整数上溢/下溢；（5）交易状态依赖性；（6）对区块状态的依赖性；（7）交易订单依赖性。
在性能层面，从以下几个角度进行评估：（1）指导费用；（2）分析的复杂性；（3）分析时间。
具体实验数据可以阅读原文获取。通过实验，我们得出结论：ZEUS表现结果优异，大大优于Oyente，验证时间缩短了一个数量级。
18.7结论
我们介绍了ZEUS的设计和实现，ZEUS是一个用于分析智能合约安全特性的框架。 ZEUS利用抽象解释和符号模型检查以及CHC的功能来快速确定验证条件。我们构建了第一个从Solidity到LLVM的位码转换器，以根据策略规范自动插入验证条件。我们对超过22.4万个Solidity智能合约的评估表明，其中约94.6％（资产净值超过5亿美元）易受攻击。 在我们的数据集中，ZEUS表现结果优异，大大优于Oyente，验证时间缩短了一个数量级。
本文由南京大学软件学院2016级本科生曹佳玮转述。
添加新手交流群：币种分析、每日早晚盘分析
添加助理微信，一对一亲自指导：YoYo8abc
