如何审计复杂的DeFi协议：分而治之方法论

保护一个单体智能合约代码库不仅仅是一个代码审查任务；它是一个系统性的工程挑战。随着 DeFi 协议演变成借贷市场、收益聚合器和跨链桥的网状结构，线性地阅读代码不足以保证安全性。

对于企业级的安全性，线性扫描是一种负担。为了确保协议的偿付能力，Zealynx 采用分而治之的方法。这是一种将系统分解为隔离的组件、验证它们的局部不变性并将它们重新组装以进行接缝压力测试的工程实践。

我们将以 Uniswap V2 为案例来演示这种方法。通过剥离它并隔离 Pair 逻辑，我们揭示了严格的组件分析如何保护数十亿美元的价值。

理论：系统复杂性 vs 线性审查

人类处理复杂状态转换的能力是有限的。对认知负荷的研究表明，审查人员可以同时跟踪的活动变量的数量存在硬性限制。

一个复杂的 DeFi 协议涉及数百个状态变量和交互。尝试线性审计会迫使工程师将每个变量加载到他们的心理堆栈中，导致认知溢出，并且不可避免地会忽略漏洞。

在具有高价值的系统中，分而治之是正确性的必要条件。它正式分解了问题：

1. 分解：将系统切分为具有清晰边界的隔离模块。
2. 不变量定义：定义每个模块的“物理定律”。
3. 本地验证：证明该模块在隔离状态下遵守其定律。
4. 组合分析：验证模块是否安全地交互。

通过隔离地验证组件，我们确保安全保证建立在经过验证的局部真理的基础上，而不是概率性的概述。

阶段 1：划分（架构映射）

在分析语法之前，我们先绘制地图。有效的风险管理需要清楚地了解跨交互合约的状态转换。

我们将代码分为四个不同的集群，以消除上下文切换并专注于特定的风险向量：

1. 金库/资产集群：资金在哪里？（ERC20，ETH 余额）。
2. 逻辑集群：“大脑”。（定价、交换、利率计算）。
3. 数据/预言机集群：外部真理来源。
4. 治理集群：管理权限和时间锁。

通用应用：这适用于任何系统。在借贷协议中，我们将 Comptroller（逻辑）与 cToken（金库）分开。在桥接中，我们将 Relayer（治理）与 Custody（金库）分开。目标始终是识别信任边界——数据在哪里进入，资金从哪里离开？

可视化 Uniswap V2

映射 Uniswap V2 揭示了两个主要的不同组件：

• 工厂：治理/管理集群。它部署交易对并管理 feeTo 地址。
• 交易对：逻辑和金库集群。这是协议的“上帝类”。

策略：我们降低了工厂的优先级，因为它主要是管理性的。关键的偿付能力风险在于交易对合约。我们隔离 UniswapV2Pair.sol，将其视为具有严格输入和输出的黑盒。

阶段 2：不变量（定义偿付能力）

安全性需要定义协议不变量——无论用户输入或市场状况如何，都绝不能被打破的数学真理。

对于 Uniswap V2，文档 提供了“恒定乘积公式”：$x \cdot y = k$。

翻译成安全不变量：

偿付能力不变量：在任何交换操作之后，储备金的乘积必须大于或等于交换之前的乘积（调整费用后）。

注意： 我们指定“交换”，因为 mint 和 burn 操作旨在更改 k。

如果这个不变量被打破，则池子无力偿债。我们的目标不仅仅是寻找错误；而是试图违反 $k$。

阶段 3：征服（案例研究：UniswapV2Pair.sol）

检查 UniswapV2Pair.sol 中的 swap 函数揭示了标准审查和架构分析之间的区别。一位高级工程师专注于资产层和逻辑层之间的交互。

1. 资产层检查（乐观转移）

Uniswap V2 采用“乐观转移”模式：它在验证收到付款之前先转移代币出去。

1// UniswapV2Pair.sol
2function swap(uint amount0Out, uint amount1Out, address to, bytes calldata data) external lock {
3    require(amount0Out > 0 || amount1Out > 0, 'UniswapV2: INSUFFICIENT_OUTPUT_AMOUNT');
4    (uint112 _reserve0, uint112 _reserve1,) = getReserves();
5
6    // ... logic ...
7

8    // OPTIMISTIC TRANSFER
9    if (amount0Out > 0) _token0.safeTransfer(to, amount0Out);
10    if (amount1Out > 0) _token1.safeTransfer(to, amount1Out);
11
12    // FLASH LOAN HOOK
13    if (data.length > 0) IUniswapV2Callee(to).uniswapV2Call(msg.sender, amount0Out, amount1Out, data);
14
15    // ... check invariants ...
16}

工程问题：如果合约首先释放资金，如何保证偿付能力？

答案不在于转移逻辑，而在于执行后的状态验证。

2. 逻辑层检查（强制执行 k）

协议不依赖于 msg.value 或用户参数来确定收到的资金。它在执行结束时验证自己的余额。

1    uint balance0 = IERC20(_token0).balanceOf(address(this));
2    uint balance1 = IERC20(_token1).balanceOf(address(this));
3

4    uint amount0In = balance0 > _reserve0 - amount0Out ? balance0 - (_reserve0 - amount0Out) : 0;
5    uint amount1In = balance1 > _reserve1 - amount1Out ? balance1 - (_reserve1 - amount1Out) : 0;

分而治之策略的实际应用： 这证明了关注点的清晰分离：

• 状态：合约信任 balanceOf(address(this))。
• 逻辑：它基于_当前余额_和_缓存的储备金_之间的差额来计算 amountIn。

3. 漏洞搜寻：带手续费的代币转账

通过隔离资产层，一个关键的差异变得显而易见。

• 期望：逻辑层假定用户转移 100 个代币会导致 balanceOf 增加 100。
• 现实：某些代币（USDT、PAXG）在转移时征收费用。用户发送 100，合约收到 99。

如果 Uniswap 信任输入参数，数学运算就会中断。但是，由于 Uniswap 依赖于 balanceOf（实际状态），因此它可以正确处理这些非标准代币。

关键见解：这高亮显示了分叉的主要风险向量。如果协议分叉用 amount 输入参数替换 balanceOf 检查以优化 gas，它们会引入致命的偿付能力错误。

阶段 4：重组（交互风险）

在组件验证之后，我们重新组装系统以分析其与外部环境的交互。

重入向量

Uniswap V2 采用 lock 修饰符（互斥锁）。

1modifier lock() {
2    require(unlocked == 1, 'UniswapV2: LOCKED');
3    unlocked = 0;
4    _;
5    unlocked = 1;
6}

虽然标准的重入性得到了缓解，但只读重入性仍然是一个风险。

在 uniswapV2Call（闪电贷Hook）期间，reserves 状态变量仍然过时，而代币余额已经更改。如果外部合约在此回调期间读取 getReserves()，它会收到过时的定价数据。如果它读取 balanceOf()，它会看到新的余额。

风险评估： 虽然 UniswapV2Pair 受到自我保护，但如果集成协议在闪电兑换期间基于 getReserves() 和 balanceOf() 的混合计算价格，则它们很容易受到攻击。

受害者情景： 一个使用 Pair.getReserves() 在闪电贷期间计算抵押品价值的借贷协议将看到旧的（高的）价格，即使资产已离开池子。“分而治之”的方法揭示了风险存在于接口边界。

阶段 5：验证（证明）

安全不是猜测；而是一种证明。一旦组件和不变量（$k$ 不得减少）被识别，我们就会使用工具来强制执行它。

这种方法为 形式验证 奠定了基础。像 Halmos、Certora 或 Hevm 这样的工具无法一次性“解决”整个协议——状态空间太大了。它们需要为特定组件定义不变量。

基于属性的测试（Foundry）

我们不为简单的算术编写单元测试。我们编写 模糊测试，试图打破协议的规则。

1// Foundry Invariant Test
2contract UniswapInvariant is Test {
3    UniswapV2Pair pair;
4

5    function invariant_k_never_decreases() public {
6        (uint112 reserve0, uint112 reserve1,) = pair.getReserves();
7        uint k = uint(reserve0) * uint(reserve1);
8
9        // Assert that K is always maintained (allowing for small fee growth)
10        assert(k >= initial_k);
11    }
12}

通过针对一个使用随机输入执行 swap、mint 和 burn 的处理程序运行此代码，我们可以确认没有边缘情况（溢出、舍入误差）违反核心逻辑。

结论

“分而治之”的方法将安全性从手动审查转变为严格的工程过程。它是识别 “深层错误”——linter 和 AI 工具错过的逻辑缺陷——的唯一一致方法。

1. 分割：将资金（金库）与数学（逻辑）分开。
2. 定义：建立不变量（例如，$x \cdot y = k$）。
3. 征服：隔离验证这些不变量的实现。
4. 验证：检查接缝（重入、互操作性）。

当通过这个视角分析 Uniswap V2 时，我们看到了一种旨在在对抗环境中强制执行数学真理的机制。这是 Zealynx 为每个项目带来的安全标准。

将此应用于你自己的审计

要在实践中实施这种方法：

1. 从文档开始：在阅读代码之前，使用文档和部署图映射协议架构。
2. 首先定义不变量：写下必须保持的数学真理（例如，总份额 = 个人份额之和）。
3. 隔离组件：将金库逻辑与定价逻辑分开审计，将治理与执行分开审计。
4. 测试边界：专注于组件之间的交互点——这是大多数关键错误隐藏的地方。
5. 自动化验证：使用 Foundry 不变量测试来持续验证你识别的不变量。

与 Zealynx 合作

在 Zealynx，我们专注于 DeFi 格局的基础 AMM 设计、架构权衡和安全漏洞。如果你正在构建与 AMM 集成的协议，或者需要对复杂的 DeFi 系统进行严格的审计，我们的团队可以提供必要的专家指导，以确保偿付能力和安全性。

保护你的协议

常见问题解答：分而治之方法

1. 智能合约安全中的协议不变量是什么？

协议不变量是数学或逻辑规则，无论用户操作或市场状况如何，都必须在智能合约的整个执行过程中保持为真。例如，在流动性池中，不变量可能是 LP 代币的 totalSupply 始终等于所有个人余额之和，或者在 Uniswap V2 中，储备金的乘积 ($x \cdot y = k$) 在交换后永远不会减少。违反这些不变量通常表明存在可能导致资金损失的关键漏洞。与缺少访问控制等表面错误不同，违反不变量代表了协议经济或数学逻辑中的根本缺陷。

2. 什么是只读重入，为什么它对 DeFi 协议是危险的？

只读重入发生在合约的 view 函数在外部调用期间返回过时或不一致的状态时（即使无法重新进入合约以进行状态更改）。在 Uniswap V2 示例中，在闪电兑换期间，getReserves() 返回旧值，而代币余额已经更改。这是危险的，因为与你的合约集成的外部协议可能会基于此过时数据计算价格或抵押品价值，从而导致漏洞利用。与传统的重入不同，没有互斥锁可以阻止这种情况——漏洞存在于集成边界。DeFi 协议绝不能混合来自不同来源的链上状态读取（如 getReserves() 和 balanceOf()），而不了解它们的同步保证。

3. 为什么智能合约审计专注于组件之间的“信任边界”？

信任边界是数据从外部源进入你的协议或资产在隔离组件之间移动的接口。这些边界是风险最高的区域，因为它们代表了一个组件的假设与另一个组件的现实相遇的点。例如，当你的金库接受来自用户的代币（外部 → 内部）时，或者当你的定价逻辑查询预言机（内部 → 外部）时。大多数关键漏洞（如带手续费的代币转账问题、预言机操纵或跨合约重入）都发生在这些边界。在单独验证每个组件后，分而治之的方法专门隔离并压力测试这些接缝。

4. 智能合约中的深层错误和表面错误有什么区别？

表面错误是违反已知模式的行为，自动化工具可以捕获这些行为：缺少访问控制、整数溢出（pre-0.8.0）、未检查的外部调用或标准重入。深层错误是违反系统唯一不变量的协议特定逻辑缺陷——例如允许 AMM 中恒定乘积公式 $k$ 减少，或允许总份额超过金库中存入的资产。自动扫描器会错过这些错误，因为它们不了解你的协议的预期行为。深层错误需要了解架构，定义特定系统的“正确”含义，并系统地测试这些定义。这就是为什么协议特定的不变量测试和形式验证对于处理大量 TVL 的高价值 DeFi 系统至关重要。

5. Uniswap V2 中的乐观转移模式如何保持偿付能力？

乐观转移模式在验证收到付款之前将代币发送给用户——这似乎是一种危险的设计。偿付能力通过执行后的余额验证来维护：合约不信任用户提供的金额，而是在转移后通过 balanceOf(address(this)) 读取其实际代币余额，并将它们与缓存的储备金进行比较。该协议计算收到的金额为 actualBalance - (oldReserve - amountSent)，并对这些实际金额强制执行不变量 $k$。这种设计对于正确处理带手续费的代币转账至关重要。但是，取代它并使用输入参数验证来节省 gas 的分叉会引入致命的偿付能力错误——这是 AMM 衍生品中的一个常见漏洞。

6. DeFi 创始人评估智能合约审计时应该注意什么？

寻找审计员识别并测试了你的协议特定不变量的证据，而不仅仅是通用漏洞清单。一个高质量的审计应该记录：（1）架构分解，显示组件是如何隔离的，（2）为每个组件定义的数学或逻辑不变量（例如，“总质押必须等于用户质押之和”），（3）使用 Foundry、Echidna 或 Certora 等工具进行基于属性或不变量测试的证据，以及（4）在信任边界的集成风险分析。询问潜在的审计员：“你会为我们的协议定义哪些不变量？” 如果他们在阅读代码之前无法回答协议特定问题，他们很可能正在运行自动化扫描器和手动检查表审查——这对于处理大量 TVL 的复杂 DeFi 系统来说是不够的。

• 原文链接： zealynx.io/blogs/divide-...
• 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～