costa-group/EthIR
GitHub: costa-group/EthIR
这是一个用于 Ethereum 字节码高级分析的框架，通过构建控制流图和生成基于规则的表示，支持对智能合约进行静态属性推断。
Stars: 22 | Forks: 3
# EthIR
[][license-badge-url]
一个用于 Ethereum 字节码高级分析的框架。
EthIR 为 Ethereum 字节码构建完整且合理的控制流图（CFG），并生成程序的*基于规则的表示*（RBR）。这种高级表示使得应用现有高级分析来推断 EVM 代码的属性成为可能。
## 安装 (Ubuntu)
### 1. 安装 Solidity 编译器
下载包含 Solidity 编译器静态可执行文件的源文件夹。
将其添加到 PATH 并测试是否已安装。
```
sudo cp source/solc* /usr/bin/
sudo chmod 755 /usr/bin/solc*
solc --version
solcv5 --version
solcv6 --version
```
如果您想安装最新版本：
```
sudo add-apt-repository ppa:ethereum/ethereum
sudo apt-get update
sudo apt-get install solc
```
此外，它还支持 `solc-select`。要安装它，请运行：
```
pip3 install solc-select
solc-select install all
```
### 2. 安装 Ethereum
源文件夹中提供了一个静态可执行文件。
将其添加到 PATH 并测试是否已安装。
```
sudo cp source/evm* /usr/bin/
sudo chmod 755 /usr/bin/evm*
evm --version
```
如果您想安装最新版本：
```
sudo apt-get install software-properties-common
sudo add-apt-repository -y ppa:ethereum/ethereum
sudo apt-get update
sudo apt-get install ethereum
```
### 3. 安装 [Z3](https://github.com/Z3Prover/z3/releases)（最后测试的版本为 4.5.0）
下载 [源代码文件夹](https://github.com/Z3Prover/z3/archive/z3-4.5.0.zip)。
解压文件夹并进行安装。
```
unzip z3-z3-4.5.0.zip
cd z3-z3-4.5.0
python scripts/mk_make.py --python
cd build
make
sudo make install
```
### 4. 安装依赖项（最后测试的 pip 版本为 8.1.1）
使用 `pip install` 命令安装 six、requests python 库。
```
pip3 install six
pip3 install requests
pip3 install semantic_version
```
根据 pip 版本的不同，上述命令可能会失败。如果是这种情况，请运行以下命令代替之前的命令。
```
python3 -m pip install six
python3 -m pip install requests
python3 -m pip install semantic_version
```
要检查版本，请运行命令 `pip -V`。
## 运行 EthIR
要执行 EthIR，请在文件夹 *ethir* 内运行以下命令之一：
1. 从 solidity 文件运行 EthIR：
```
./ethir.py -s file_name.sol
```
2. 从 EVM 文件运行 EthIR：
```
./ethir.py -s file_name.evm -b
```
3. 从反汇编的 EVM 文件运行 EthIR：
```
./ethir.py -s file_name.disasm -disasm
```
### 选项
命令 `./ethir.py -h` 显示包含 EthIR 所有可用选项的列表。其中一些最相关的选项如下：
1. 以文本模式存储控制流图，并以图形方式存储在 dot 文件中：
```
./ethir.py -s filename -cfg normal
```
2. 生成 SACO RBR
```
./ethir.py -s filename -saco
```
3. 显示调试信息：
```
./ethir.py -s filename -d
```
EthIR 在执行期间生成的所有文件都存储在目录 /tmp/costabs/ 中。
### 运行示例
安装 EthIR 后，假设我们要为文件夹 *[examples](https://github.com/costa-group/EthIR/tree/master/examples)* 中可用的反汇编文件 *blockking.evm.disasm* 生成 RBR。首先，我们必须进入 *ethir* 目录并在那里执行命令 `./ethir.py -s ../examples/blockking.evm.disasm -disasm`。
在执行期间，EthIR 创建了目录 */tmp/costabs/*，用于存储与 *blockking.evm.disasm* 文件关联的 RBR。如果我们检查此目录，会发现一个名为 *rbr.rbr* 的文件，其中包含 RBR。如果我们使用任何通用编辑器（gedit、emacs）打开该文件，我们可以看到生成的 rbr。下面是为 *blockking.evm.disasm* 文件生成的 RBR 的草图：
```
block0(g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(8), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), calldatasize, calldataload, gas, caller, callvalue, number, gasprice, balance)=>
s(0) = 96
s(1) = 64
l(0) = s(0)
s(0) = calldatasize
call(jump0(s(0),g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(8), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), calldatasize, calldataload, gas, caller, callvalue, number, gasprice, balance))
jump0(s(0), g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), balance, calldataload, calldatasize, caller, callvalue, gas, gasprice, number)=>
eq(s(0), 0)
call(block174(g(11), g(8), g(4), g(1), g(0), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), caller, callvalue, gas, gasprice, number))
jump0(s(0), g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), balance, calldataload, calldatasize, caller, callvalue, gas, gasprice, number)=>
neq(s(0), 0)
call(block11(g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), balance, calldataload, caller, callvalue, gas, gasprice, number))
block11(g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), balance, calldataload, caller, callvalue, gas, gasprice, number)=>
s(0) = 224
s(1) = 2
s(0) = s(1)^s(0)
s(1) = 0
s(1) = calldataload
s(0) = s(1)/s(0)
s(1) = 607252836
s(2) = s(0)
call(jump11(s(2),s(1),s(0),g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), balance, calldataload, caller, callvalue, gas, gasprice, number))
```
如果我们执行命令 `./ethir.py -s ../examples/blockking.evm.disasm -disasm -eop` 而不是上述命令，EthIR 生成的 RBR 将带有 nops 注释，并且 EVM 字节码会交错在文本中。下面是为 *blockking.evm.disasm* 生成的带有 nops 注释的 RBR 的草图：
```
block0(g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(8), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), calldatasize, calldataload, gas, caller, callvalue, number, gasprice, balance)=>
s(0) = 96
nop(PUSH1)
s(1) = 64
nop(PUSH1)
l(0) = s(0)
nop(MSTORE)
s(0) = calldatasize
nop(CALLDATASIZE)
call(jump0(s(0),g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(8), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), calldatasize, calldataload, gas, caller, callvalue, number, gasprice, balance))
nop(ISZERO)
nop(PUSH2)
nop(JUMPI)
jump0(s(0), g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), balance, calldataload, calldatasize, caller, callvalue, gas, gasprice, number)=>
eq(s(0), 0)
call(block174(g(11), g(8), g(4), g(1), g(0), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), caller, callvalue, gas, gasprice, number))
jump0(s(0), g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), balance, calldataload, calldatasize, caller, callvalue, gas, gasprice, number)=>
neq(s(0), 0)
call(block11(g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), balance, calldataload, caller, callvalue, gas, gasprice, number))
block11(g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), balance, calldataload, caller, callvalue, gas, gasprice, number)=>
s(0) = 224
nop(PUSH1)
s(1) = 2
nop(PUSH1)
s(0) = s(1)^s(0)
nop(EXP)
s(1) = 0
nop(PUSH1)
s(1) = calldataload
nop(CALLDATALOAD)
s(0) = s(1)/s(0)
nop(DIV)
s(1) = 607252836
nop(PUSH4)
s(2) = s(0)
nop(DUP2)
call(jump11(s(2),s(1),s(0),g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), balance, calldataload, caller, callvalue, gas, gasprice, number))
nop(EQ)
nop(PUSH2)
nop(JUMPI)
```
EthIR 还允许我们存储被分析文件的 CFG。在这种情况下，我们必须执行命令 `./ethir.py -s ../examples/blockking.evm.disasm -disasm -cfg`。EthIR 将 cfg 存储在目录 */tmp/costabs/* 中扩展名为 *.cfg* 的文件中。
请注意，一个文件可能包含多个智能合约。在这种情况下，EthIR 会为每个合约生成一个文件 rbr0.rbr、rbr1.rbr、...rbrn.rbr。
## 智能合约示例
文件夹 *[examples](https://github.com/costa-group/EthIR/tree/master/examples)* 包含用于测试该工具的运行示例。其中既有 solidity、evm 也有反汇编文件。
大多数示例（如 bloccking.evm.disasm、advertisement.sol、validToken.sol 或 cryptoPhoenix.sol）都是从区块链获取的真实合约，而其他示例（如 loop1.sol 和 sum.sol）则是临时示例，更容易理解反编译过程。
## 使用 SACO 限制循环
[SACO](http://costa.fdi.ucm.es/saco/web/) 是一个用于并发对象的静态分析器，能够推断循环迭代次数的*上界*以及其他属性。请注意，这是推断智能合约 gas 消耗的关键的第一步。
[SACO](http://costa.fdi.ucm.es/saco/web/) 的内部表示与 EthIR 生成的 RBR 的语法在经过轻微的语法转换后相匹配。得益于此，它能够证明某些示例中包含的循环的终止性，并为这些循环产生线性界限。以下是 [SACO](http://costa.fdi.ucm.es/saco/web/) 为文件夹 [*examples*](https://github.com/costa-group/EthIR/tree/master/examples) 中包含的某些智能合约推断出的一些循环界限：
|智能合约|界限|智能合约|界限|
|--|--|--|--|
| BlockKing | nat(g8/10)*36+8934493 | CryptoPhoenix | nat(g3)*228409344+4113285485 |
| Loop1 | nat(a)*25+234 | Eligma | nat(_numberOfReturns)*2628+134 |
| Lottery | 159 | BlockSquareSerieA | 286 |
| Enclaves | 268 | AuctusEther | 264 |
| Advertisement | inf | validToken | inf |
[SACO](http://costa.fdi.ucm.es/saco/web/) 为上表中显示的前四个智能合约推断出了线性界限。智能合约 BlockKing 和 CryptoPhoenix 的界限取决于其字段之一的值（分别为第八个和第三个字段）。对于智能合约 Loop1 和 Eligma，获得的界限依赖于其某些函数的参数（a 和 _numberOfReturns）。如果智能合约不包含任何循环（如 Lottery、BlockSquareSerieA、Enclaves 或 AuctusEther），[SACO](http://costa.fdi.ucm.es/saco/web/) 会推断出一个常数界限。
请注意，由于 [SACO](http://costa.fdi.ucm.es/saco/web/) 的精度限制（它没有位运算和函数 sha3 的模型），分析器会忽略位变量的信息。由于这个因素，[SACO](http://costa.fdi.ucm.es/saco/web/) 无法为某些智能合约（如 ValidToken 或 Advertisement）推断界限，并返回 *inf*。
其他在中间形式（如整数转换系统或 Horn 子句）上工作的高级分析器（例如 AproVe、T2、VeryMax、CoFloCo）也可以很容易地适配以在 EthIR 生成的 RBR 转换程序上工作。
如果您有兴趣将 EthIR 与 [SACO](http://costa.fdi.ucm.es/saco/web/) 结合使用，请通过 pull-request 或新 issue 联系 [SACO](http://costa.fdi.ucm.es/saco/web/) 开发人员。
您可以 [在此处](http://costa.fdi.ucm.es/gastap) 尝试第一个原型。GASTAP 推断每笔交易中涉及的 gas 的上界。
标签：CFG, EVM, Python, RBR, Solidity, URL提取, Z3, 中间表示, 二进制发布, 云安全监控, 云资产清单, 以太坊, 区块链, 反编译, 可配置连接, 字节码, 开源工具, 形式化验证, 控制流图, 无后门, 智能合约, 智能合约安全, 程序分析, 符号执行, 逆向工具, 逆向工程, 静态分析