(论文阅读)WANA: Symbolic Execution of Wasm Bytecode for Extensible Smart Contract Vulnerability Detection
时间： 2021
作者： B Jiang, Y Chen, D Wang（北航）
会议： QRS‘2021 （软工CCF-C）
Abstract
许多流行的区块链平台支持智能合约，以建立去中心化的应用程序。然而，智能合约内的漏洞已经证明导致其终端用户的严重经济损失。特别是EOSIO智能合约平台上的智能合约导致了大约38万个EOS代币的损失，在攻击发生时，价值约为190万美元。EOSIO智能合约平台是基于Wasm虚拟机的，它也是支持其他智能合约平台以及网络应用的底层系统。在这项工作中，我们提出了WANA，一个基于Wasm字节码符号执行的可扩展智能合约漏洞检测工具。WANA提出了一套基于Wasm字节码分析的算法来检测EOSIO智能合约的漏洞。我们的实验分析表明，WANA可以有效地、高效地检测EOSIO智能合约中的漏洞。此外，我们的案例研究还表明，WANA可以扩展到有效检测Ethereum智能合约的漏洞。
问题背景
EOSIO是一个流行的公共区块链平台，支持智能合约技术。然而，EOSIO智能合约中的漏洞导致了其终端用户的经济损失。对于EOSIO智能合约来说，区块信息依赖漏洞、假的EOS转移漏洞和伪造的转移通知漏洞总共导致了大约38万个EOS代币的损失 。在攻击发生时，这些漏洞的累计损失金额约为价值190万美元。因此，需要有效的漏洞检测工具来保护EOSIO区块链平台的生态系统。
Wasm不仅被EOSIO公共区块链平台采用作为智能合约执行引擎[35]，也被其他区块链平台的议程项目采用。例如，以太坊区块链平台已经计划为以太坊2.0采用Ethereum Wasm（EWasm）虚拟机。Polkadot平台[40]进一步采用Wasm作为其parachain运行时和智能合约执行的编译目标。Wasm在构建Web应用程序中也很受欢迎，因为Wasm模块可以调用到JavaScript上下文，并通过从JavaScript访问的相同Web API访问浏览器的功能。Wasm的综合符号执行引擎有希望为任何以Wasm为目标的应用程序提供一个可扩展的安全分析框架。
贡献
- 它为Wasm提出了一个通用的符号执行框架WANA；
- 它提出了一个基于符号执行引擎的智能合约漏洞检测工具的新的可扩展架构；
- 它提出了一个全面的实验研究，以评估WANA对EOSIO智能合约的漏洞检测效果；
- 它提出了一个案例研究，以评估WANA在Ethereum平台上漏洞检测方面的可扩展性。
模型
如上图所示，Wasm字节码被解析、加载，并在Wasm符号执行引擎中被初始化。WANA的符号执行引擎是作为一个新的虚拟机实现的，它可以根据WASM规范评估具体和符号输入。它已经实现了Wasm规范1.0版中的所有指令。当一个模块被加载到WANA Wasm虚拟机中时（在加载和初始化阶段），WANA的符号执行引擎会准备一个执行环境，其中包括存储器、各种表（包括函数表和符号表）、全局变量和一个执行堆栈，以保持模块的执行上下文。
1. 符号执行引擎
WANA会在所有exported函数上进行符号执行，对于每个导出的函数正文中的指令所调用的每个Wasm函数，WANA首先准备一个框架作为其执行环境，其中包括参数、局部变量、返回值和对其模块的引用。然后，它开始依次符号执行被调用函数的code section的指令。
在所有的Wasm指令中，主要有四种指令，包括数字、内存、控制和函数调用指令,下面介绍WANA如何处理:
Numeric instructions:
WANA实现了基于堆栈的执行逻辑。WANA的符号执行引擎首先弹出操作数，进行符号计算，并将结果推回堆栈。所有关于整数和浮点值类型的数字指令都支持。
Control instructions:
有两种分支指令：无条件分支（如br）和条件分支（如br_if）。
(a) 非条件性分支： 在Wasm中，执行无条件分支将直接跳到指令参数指定的标签上继续执行，这对实现循环很有用。然而，当循环的深度增加时，符号执行引擎将变得缓慢或由于状态爆炸而被困住。因此，WANA在路径探索过程中对每个标签的最大嵌套循环深度设置了一个上限。
(b) 条件性分支： 对于指令br_if，其执行将取决于该指令表达式的评估结果。WANA将记录每个分支的执行环境，并遍历各个分支以实现路径覆盖。对于每个分支，在遍历之前，相应的路径约束将被输入到z3[15]进行约束解算，这可以通过修剪那些不可行的路径来提高执行效率。和上面一样，WANA在路径探索过程中也对每个标签的最大嵌套循环深度设置了一个上限。
Memory and Memory instructions:
在Wasm中，有三种类型的内存操作指令：load、store和增加内存的大小。一个Wasm模块可以在任何字节地址上从/向线性存储器加载和存储值。由于Wasm中对整数和浮点数据类型有许多位操作指令，WANA被设计为用z3中的位向量数据类型来表示整数和浮点数据类型。WANA使用32位（64位）位向量数据类型来表示32位（64位）整数和浮点符号数据类型。由于字节数组不能存储位向量或其表达式，WANA使用线性列表来存储位向量的具体值和符号值的引用，以模拟模块的内存。
在符号执行过程中，WANA在执行存储操作时，将把键值对（address, value）插入字典中。在load操作中，如果符号内存地址存在于字典中，WANA将直接从字典中获取相应的值。否则，WANA将从线性列表中随机选择一个内存地址并返回其值。此后，符号内存地址将被绑定到一个随机选择的内存地址。
Function call:
在Wasm中，有两种类型的函数调用：直接和间接。
对于间接函数调用，WANA的符号执行引擎首先从执行堆栈的顶部框架获得一个索引。然后，符号执行引擎使用该索引从函数表中获得具体的函数地址。对于当前Wasm模块中的函数，WANA直接进入函数，继续进行符号执行。
2. 对库函数建模
一个智能合约可能会调用底层区块链平台提供的各种库函数。WANA根据这些库函数的效果来处理这些库函数的调用，并相应地模拟其行为。由于库函数与平台有关，WANA为不同的平台模拟了不同的库函数行为。当把WANA扩展到一个新的平台时，其相应的库函数也应被模拟。
