动态分析与模糊测试 - Alpha Book
跳转至

动态分析与模糊测试

静态分析找"看起来像漏洞"的代码，动态测试找"真的会执行的漏洞"。两个互补，缺一不可。

Echidna

  • 作者：Trail of Bits
  • 类型：基于属性的模糊测试（property-based fuzzer）
  • 特色：用 Solidity 写不变量，然后对抗式生成交易序列
Solidity
// 定义不变量：合约余额总和 == 所有用户存款总和
function test_balance_sum() public view {
    uint256 contractBal = address(this).balance;
    uint256 sum;
    for (uint i = 0; i < users.length; i++) {
        sum += balances[users[i]];
    }
    assert(contractBal >= sum);
}
Bash
echidna test.sol --contract Test

优点：直接写 Solidity 不变量、自动生成攻击序列 缺点：需要人工定义不变量，覆盖率依赖种子多样性

Source | 教程

Medusa

  • 作者：Trail of Bits
  • 类型：变异式模糊测试，基于 go-ethereum
  • 特色：Echidna 的 Go 重写版，性能更好
Bash
medusa fuzz --target contract.bin

优点：纯 Go 实现运行快、内置覆盖率引导

Source

Manticore

  • 作者：Trail of Bits
  • 类型：动态符号执行
  • 特色：分析 EVM 字节码，穷举所有可能执行路径
Bash
manticore contract.bin

优点：能找出"理论上可达"的任何执行路径 缺点：路径爆炸，大规模合约不可用

Source

Harvey

  • 作者：ConsenSys Diligence
  • 类型：灰盒模糊测试
  • 特色：结合静态分析的模糊测试

Source

Foundry 模糊测试

Solidity
// 通过 Foundry 的 vm 对象做模糊测试
function testFuzz_Withdraw(uint256 amount) public {
    vm.assume(amount > 0 && amount <= balances[msg.sender]);
    vm.prank(msg.sender);
    vault.withdraw(amount);
    assertEq(balances[msg.sender], 0);
}
Bash
forge test --match-test testFuzz_Withdraw -vvvv

优点：不需要额外工具链，直接用 Foundry Source

工具选择

场景 推荐工具
快速扫描 → 漏洞 Slither
深度穷举所有可能 Manticore
对抗式属性检查 Echidna / Medusa
闭源合约 Echidna + Rattle
自定义不变量测试 Foundry fuzz + invariant
CI 集成 Slither + Foundry fuzz

Foundry 的两种测试：模糊与不变式

Foundry 把动态测试做成一等公民，关键是两套机制：

模糊测试（fuzz）——对带参数的函数喂随机输入，断言不崩、不 revert、不越界。它验证「采样到的输入」都安全，但采样不到的边界仍可能漏。

不变式测试（invariant）——以 invariant 前缀命名函数，Forge 先跑 setUp，再对合约做成千上万次随机调用序列，每次之后都重新校验你声明的不变量：

Solidity
contract VaultInvariant is Test {
    Vault v;
    function setUp() public { v = new Vault(); targetContract(address(v)); }

    function invariant_totalSupplyGeDeposits() public {
        assertGe(v.totalSupply(), v.totalDeposited());
    }
}

targetContract / targetSelector 决定「随机序列能调哪些函数」；如果某些函数必须由特定角色调用，要写 handler 合约把权限、时序约束包进去，否则 Forge 生成的序列会大量 revert，覆盖率上不去。

Fork 测试：在主网状态上跑

模糊测试在空白状态里跑，发现不了「和真实协议交互时才出的问题」。Fork 测试用 vm.createFork 把主网（或某条测试网）的存储快照拉下来，你的合约直接在 Aave、Uniswap 那种真实状态上跑：

Solidity
function testBorrowOnFork() public {
    vm.createFork(vm.envString("RPC_URL"));
    vm.selectFork(0);
    vm.prank(0xSomeWhale);            // 冒充一个大户
    // ... 在真实主网状态上借出资产
}

这能抓到「预言机读取、授权模型、跨协议组合」这类只在真实部署后才暴露的漏洞，代价是测试变慢、依赖 RPC 可用性。

两种模糊测试哲学

  • 基于属性（property-based）：Echidna / Medusa 让你写 Solidity 不变量，工具对抗式生成交易序列去打破它。长处是「你要先想清楚什么不能变」。
  • 覆盖率引导（coverage-guided）：Medusa 内置覆盖率引导，优先探索没走过的分支。长处是「不用手写那么多不变量也能挖深」。

两者互补：先用覆盖率引导广撒网，再对你最在意的会计 / 权限不变量写属性测试收口。

差分与编排

  • Etheno（Trail of Bits）：把同一个合约同时丢给多个分析器（Manticore、Echidna、符号执行），对结果做差分，专门找「某个工具说安全、另一个说危险」的分歧点——分歧往往是边界 bug 的藏身处。
  • 差分测试：对同一个逻辑跑两套实现（参考实现 vs 被测实现），看输出是否一致，适合数值密集的合约。

局限与误用

  • 不变量是人工负担：写得松（永远为真的废话）等于没测；写得紧（依赖具体初始状态）又会大量误报。这条线要靠经验调。
  • 覆盖率有天花板：模糊测试再久也只采样输入空间，理论上可达但概率极低的路径可能永远不被命中。
  • 确定性陷阱：种子 / corpus 固定才能复现 bug；CI 里随机种子会让偶发失败难以定位。
  • 不是证明：动态测试证伪「存在坏输入」，但永远不能证明「没有坏输入」——那是形式化验证的活。

在流水线里的位置

静态分析扫显患 → 对核心不变量上模糊 / fork 测试 → 对最值钱的那 5–10% 代码上形式化验证。动态测试填静态分析「看不见逻辑」的坑，但要把它当成「穷举采样」而不是「穷举证明」来用。

参考资料