11.1引用
Brent L, Jurisevic A, Kong M, et al. Vandal: A Scalable Security Analysis Framework for Smart Contracts[J]. 2018.
11.2摘要
现代区块链的兴起促进了智能合约的出现:在区块链上运行的自主程序。随着法律、商业、商业和治理领域的应用程序的预测，智能合约已经迅速崛起。
智能契约通常用高级语言(如solid)编写，并转换为紧凑的低级字节码，以便在区块链上部署。一旦部署完毕，字节码就会自动执行，通常由虚拟机执行。与所有程序一样，由于缺乏编程方法、语言和工具链(包括有bug的编译器)，智能合约很容易受到恶意攻击。与此同时，智能合约也是高价值的目标，通常需要大量加密货币。因此，开发人员和审计人员需要能够分析底层字节码以检测潜在安全漏洞的安全框架。
在本文中，我们提出了Vandal:Ethereum智能契约的安全分析框架。Vandal由一个分析管道组成，该管道将低级Ethereum虚拟机(EVM)字节码转换为语义逻辑关系。框架的用户可以用声明式的方式表示安全性分析:安全性分析用用Souffle语言编写的逻辑规范表示。我们对一组常见的智能合约安全漏洞进行了大规模的实证研究，证明了Vandal的有效性和高效性。Vandal既快速又健壮，平均运行时间为4.15秒，性能优于当前最先进的工具Oyente、EthIR、Mythril和Rattle。
11.3介绍
自从2008年推出比特币加密货币以来，区块链技术已经引起了经济学家、律师、技术行业和政府越来越大的兴趣。区块链是分散的分布式公共账本，最近被用作图灵完备的计算设备，用于存储和执行称为智能契约的自主程序。Ethereum和Cardano是具有智能合约功能的区块链的两个例子。Ethereum已经成为智能合约开发事实上的标准平台，我们在这儿专注于Ethereum智能合约。
智能合约通常用高级语言编写，如solbility，编译为低级字节码，部署在区块链上。智能合约有唯一的地址，用于在区块链上识别它们。然后，网络用户可以调用智能合约，并由Ethereum虚拟机(EVM)执行。每个智能合约都有自己的以太余额，以太是以太坊使用的加密货币。
一旦部署到区块链上，契约的字节码就变得不可变。这是一个高风险、高风险的范例:部署的代码是不可能打补丁的，而合约共同控制着价值数十亿美元的Ether。因此，智能合约中的安全漏洞可能会带来灾难性的后果。
已经描述了广泛的已知安全漏洞。当消息调用操作的成功/失败返回值未被检查时，即出现所谓的未检查的发送漏洞。，总是假设成功。这个漏洞是由错误处理的异常引起的更大类型的漏洞的一个例子，并且意外地频繁地发生。可重入性漏洞的出现是由于在编写合约时没有考虑到可重入性，从而允许攻击者利用中间状态进行可重入消息调用。当合同余额被任意调用者窃取时，就会出现不安全的余额漏洞。可销毁的契约是那些在暴露的程序路径上包含自毁指令的契约。如果没有足够的身份验证，则允许任意调用方永久地销毁契约。当契约通过检查起源的返回值而不是调用者来执行身份验证时，起源漏洞就会发生。在EVM中，origin返回发起事务的帐户的地址，而caller返回发起当前执行消息调用的帐户或契约的地址。
为了分析和缓解当前智能契约编程方法、语言设计和工具链方面的缺陷，我们提出了一个新的安全分析框架Vandal:该框架能够直接分析智能契约字节码。Vandal促进了一种逻辑驱动的静态程序分析方法。在这种方法中，Datalog被用作一种特定于域的语言，以弥补安全漏洞的程序语义与相应分析的实现之间的差距。
在Vandal中，安全性分析问题是使用逻辑规则以声明方式指定的。然后，一个现成的Datalog引擎执行一组编码契约的输入关系(也称为扩展数据库)的规范，并生成一个输出关系，其中包含已检测到的安全漏洞列表及其在字节码中的位置。我们的逻辑驱动方法使得安全分析程序易于编写、维护，并且与低级的手工实现相比，出错的可能性更小。
Vandal由两部分组成。首先，分析管道将低级字节码转换为逻辑驱动的安全分析的逻辑关系。在Vandal中，逻辑关系公开字节码的数据流和控制流依赖项。第二个组件是一组用于安全分析问题的逻辑规范。Vandal使用Souffle作为Datalog引擎，它从逻辑规范中综合了高性能的c++代码。
11.4Vandal框架介绍
Vandal被设计成用一种称为Souffle的声明性语言来描述安全漏洞分析。用声明性语言表示漏洞分析可以使安全专家快速构建新分析的原型，并轻松地组合现有分析。逻辑规范驱动方法有几个优点，包括用于设计和实现安全分析的敏捷能力。安全分析的设计空间可以在精度和时间之间进行权衡。安全分析的传统实现需要数十万行代码，实现、测试和维护的成本非常高。使用逻辑语言来表达安全分析所带来的性能损失可以通过现代逻辑合成器的出现而得到缓解，例如Souffle，它可以从逻辑规范生成高性能的c++代码。生成的c++代码在性能上与手工编写的程序分析代码相当，甚至更好。
Vandal设计面临的挑战是如何将智能契约转化为逻辑关系。Vandal框架利用分析管道将存储在区块链上的Ethereum字节码转换为反映智能契约语义的逻辑关系。这很有挑战性:EVM字节码是由一个非常底层的基于堆栈的抽象机器执行的。与Java虚拟机字节码相比，低级EVM字节码没有类和方法的抽象、没有内存管理、没有类型检查、没有类装入，也没有函数调用的堆栈帧概念。EVM是一个非常简单的计算设备，用于在区块链上有效地存储智能契约。智能契约的控制流和数据流被虚拟机栈混淆，使得静态程序分析的任务异常困难。要应用逻辑驱动的方法来分析智能契约，必须将EVM字节码转换为新的程序表示，以重新构造原始高级语言的数据流和控制流依赖关系。
为了从Ethereum的低级字节码重建程序语义，我们引入了一个分析管道。该管道将字节码转换为可分析形式的任务分成几个阶段，如下所示:由Scraper从区块链中提取Ethereum字节码，由反汇编程序进行反汇编，然后由反编译程序将其反编译为寄存器传输语言。该反编译器重构了智能契约高级语言的控制域数据流。反编译后，字节码程序表示为寄存器传输语言。提取器将寄存器转换语言的中间表示形式转换为逻辑关系。这些逻辑关系捕获智能契约的语义，并以简单的制表符分隔值格式存储。Souffle将安全分析合成为可执行程序，这些程序读取提取器生成的逻辑关系，并执行安全分析以检测漏洞。潜在的安全漏洞是在执行安全分析之后报告的。
11.4.1 Scraper
我们分析管道的第一个阶段是scraper，它从活动的Ethereum区块链中提取智能契约的字节码表示。
我们使用奇偶校验Ethereum客户端的JSON-RPC API实现scraper。对于抓取所有事务，包括内部事务，奇偶校验客户端必须与命令行标志同步，命令行标志启用跟踪并禁用修剪，如清单1所示。
清单1:算法1中列出了奇偶校验命令行标志，用于启用跟踪和禁用修剪。该过程遍历所有块中的所有事务，搜索契约创建。
对于区块链上的每个契约，我们的scraper在本地文件系统上生成一个文件，其中包含smart契约的机器码，即，这是一个字节序列，在管道的后面阶段需要反汇编和反编译。
11.4.2Disassembler
分析管道的第二阶段是反汇编程序，它将EVM字节码转换为一系列可读的、用程序计数器地址注释的低级助记符。这种转换是通过对字节码进行一次线性扫描来执行的，将每条指令转换为对应的助记符，并为每条指令和每一个内联操作数增加一个程序计数器。结果是一系列的程序地址、助记符和它们的参数。
图11-1
图11-2
假设程序员在区块链上部署了如图11-1所示的可靠智能契约。Vandal Scraper将以EVM字节码的形式捕获此智能契约的机器码表示形式，生成如图11-2(a)所示的文件。反汇编器将机器码转换为可读的EVM字节码，如图11-2(b)所示。
Vandal反汇编器生成与Ethereum基金会的官方反汇编器类似的输出格式，但支持基本的块边界描绘。反汇编程序和反编译程序共享一个公共的字节码解析实现。如果EVM规范发生更改，则提供用于声明新指令的接口。
11.4.3Decompiler
分析管道的下一阶段是反编译器，它将低级EVM字节码转换为寄存器传输语言。这种寄存器传输语言公开字节码的数据流和控制流结构。从概念上讲，新定义语言的语义与EVM的语义有很强的重叠，即，EVM的指令仍然反映在反编译器的寄存器传输语言中。下面的Listing1给出了该语言的抽象语法。
Listing 1
这种语言有两种类型的操作:没有副作用的操作和有副作用的操作。操作可以操作寄存器、内存或存储器中的值。操作的右边可以是一个常量、另一个寄存器，也可以是一个需要0个或多个参数的操作。左边是一个寄存器，如果操作有副作用，它就是一个内存/存储位置。EVM的所有基于堆栈的操作都可以用这种寄存器语言表示。注意，存储结构在区块链上持久存在，而内存仅在运行时临时存在。
11.4.4Extractor
分析管道中的下一步是将寄存器传输语言转换为逻辑关系的提取器。逻辑关系是逗号分隔的文件，稍后可以通过在Souffl e中表示的安全分析读取这些文件。逻辑关系表示EVM字节码程序的寄存器传输语言。
Listing 2
在Datalog之外，我们还有其他的关系，即计算前支配关系和后支配关系，例如智能契约中的控制依赖关系可以用几行逻辑来表达。我们为内存、存储和跳转操作提供了特定的逻辑关系，以更详细地反映智能契约的语义。
11.5主要贡献
提出了一种检测智能协议字节码安全漏洞的静态分析框架Vandal。Vandal由一个分析管道组成，其中包括一个反编译器，它执行抽象解释，将字节码转换为逻辑关系形式的高级中间表示。Vandal使用一种新颖的逻辑驱动方法来定义安全漏洞分析，并包含一个静态分析库来简化新分析规范的开发。
本文由南京大学软件学院2016级本科生徐介辉转述。
添加新手交流群：币种分析、每日早晚盘分析
添加助理微信，一对一亲自指导：YoYo8abc
