以太坊智能合约静态分析技术详解

概述

以太坊智能合约安全事件频发，从The DAO事件到Fomo3D奖池被盗，每次安全问题的破坏力都十分巨大。由于智能合约部署后更新和升级非常困难，因此在部署前进行静态分析，检测并发现合约中的漏洞至关重要。本文将从五个方面详细讲解智能合约静态分析技术：

1. 智能合约的编译
2. 智能合约汇编指令分析
3. 从反编译代码构建控制流图
4. 从控制流图开始约束求解
5. 常见的智能合约漏洞及检测方法

第一章 智能合约的编译

1.1 编译环境搭建

1.1.1 安装go-ethereum

在Ubuntu系统中通过apt-get安装：

sudo apt-get install software-properties-common
sudo add-apt-repository -y ppa:ethereum/ethereum
sudo apt-get update
sudo apt-get install ethereum

安装成功后可使用geth、evm、swarm等命令。

1.1.2 安装solidity编译器

sudo add-apt-repository ppa:ethereum/ethereum
sudo apt-get update
sudo apt-get install solc

1.2 solidity编译器使用

1.2.1 基本用法

示例合约test.sol：

pragma solidity ^0.4.25;
contract Test {}

生成字节码：

solc --bin test.sol

输出包含部署代码、runtime代码和auxdata三部分。

生成runtime代码：

solc --bin-runtime test.sol

1.2.2 智能合约字节码结构

1. 部署代码：创建合约时运行，完成后将runtime代码+auxdata存储到区块链
2. runtime代码：合约实际执行的代码
3. auxdata：每个合约最后43字节的辅助数据

1.2.3 生成汇编代码

solc --bin --asm test.sol

输出分为三部分：

• EVM assembly标签：部署代码
• sub_0标签：runtime代码
• auxdata：与字节码中相同

1.2.4 生成ABI

solc --abi test.sol

第二章 智能合约汇编指令分析

2.1 以太坊汇编指令

2.1.1 EVM虚拟机

• 基于栈的虚拟机
• 32字节(256比特)字长
• 栈最多容纳1024个字

2.1.2 常用汇编指令

2.2 智能合约汇编分析

示例合约：

pragma solidity ^0.4.25;
contract Overflow {
    uint private sellerBalance=0;
    function add(uint value) returns (bool, uint){
        sellerBalance += value;
        assert(sellerBalance >= value);
    }
}

反编译后关键流程：

1. 检查calldata长度
2. 验证函数签名(0x1003e2d2)
3. 检查转账金额(必须为0)
4. 执行add函数逻辑
5. 检查sellerBalance >= value条件

2.3 字节码反编译

使用evm工具反编译runtime代码：

evm disasm test.bytecode

反编译结果与控制流对应关系：

• 00000-0003d：函数签名检查
• 00043-0004d：转账金额验证
• 00073-00085：add函数核心逻辑

第三章 构建控制流图

3.1 控制流图概念

3.1.1 基本块(basic block)

构建原则：

1. 遇到程序第一条指令开始新块
2. 遇到跳转/分支指令结束当前块
3. 其他指令加入当前块

3.1.2 控制流图(CFG)

有向图G=(N,E)：

• N：基本块集合
• E：基本块间的跳转关系

3.2 构建基本块

示例反编译代码可划分为11个基本块，每个块包含：

• 起始和结束地址
• 指令序列

3.3 构建边

跳转关系示例：

• 基本块1 → 基本块2(条件不满足)
• 基本块1 → 基本块3(条件满足)
• 基本块6 → 基本块8(无条件)

3.4 完整控制流图

• 条件分支(菱形节点)
• 结束块(基本块11)

第四章 约束求解

4.1 z3基础

4.1.1 基本用法

from z3 import *
x = Int('x')
y = Int('y')
solve(x > 2, y < 10, x + 2*y == 7)

4.1.2 布尔运算

p = Bool('p')
q = Bool('q')
solve(Implies(p, q), r == Not(q))

4.1.3 位向量

x = BitVec('x', 16)
y = BitVecVal(65535, 16)

4.2 智能合约约束求解

4.2.1 表达式转换

基本块1指令：

CALLDATASIZE
LT(4, Id_size)
JUMPI(0x3e)

转换为z3表达式：

If(ULE(4, Id_size), 0, 1) != 0

4.2.2 执行求解

solver.add(exp)
if solver.check() == sat:
    print("跳转到基本块3")
else:
    print("跳转到基本块2")

第五章 常见漏洞检测

5.1 整数溢出

5.1.1 漏洞原理

uint256最大值为2²⁵⁶-1，加1会变为0

5.1.2 检测方法

first = BitVecVal(stack.pop(), 256)
second = BitVecVal(stack.pop(), 256)
solver.add(UGT(first, first + second))
if check_sat() == sat:
    print("整数溢出")

5.2 重入漏洞

5.2.1 漏洞原理

转账方法对比：

• transfer/send：限制2300gas，安全
• call：默认无gas限制，危险

5.2.2 检测方法

1. 检查call指令是否设置gas限制
2. 检查call后是否有其他操作

危险模式：

receiver.call.value(amount)();
balances[msg.sender] -= amount;  // 先转账后修改状态

安全模式：

balances[msg.sender] -= amount;  // 先修改状态
receiver.call.value(amount)();   // 后转账

总结

本文系统介绍了智能合约静态分析技术：

1. 从编译环境搭建到字节码生成
2. 通过反汇编理解EVM指令
3. 构建控制流图分析执行路径
4. 使用z3进行约束求解
5. 检测整数溢出和重入等常见漏洞

掌握这些技术可有效提高智能合约安全性，在部署前发现潜在漏洞。