介绍
自动化市场中小的舍入误差可能会导致价格变动、资金池耗尽或产生可利用的条件。Balancer 的 StableSwap 漏洞就是一个例子，说明一个小的数学不一致如何产生有意义的风险。本文解释了如何使用 Python 进行差分模糊测试，以揭示高精度计算与 Solidity 实现之间的差异。
Balancer 官方报告
根本原因
资金池接收一个交换量并返回另一种 token 的数量。当合约乘以一个因子时，会发生精度问题。乘法会降低分辨率，并产生一个小于数学上正确值的输出。
如何修复舍入
有两种方法可以解决这个问题：
- 以正确的方向舍入输入 token
- 对计算和转移始终使用相同的值
交换中的数学
StableSwap 不变量
StableSwap 不变量定义为：
A * n^n * S + D = A * D * n^n + D^(n+1) / (n^n * P)
其中：
$A$ 是放大系数，它将曲线塑造成恒定总和行为$n$ 是池中 token 的数量$S$ 是余额的总和：Σ($x_i$)$D$ 是不变量，类似于总流动性$P$ 是余额的乘积：Π($x_i$)
当一个余额发生变化时，合约使用这种关系来计算输出 token 的数量。
有关数学的更多详细信息，请参阅此 Cyfrin Updraft Curve 课程。
注意：在 Balancer 代码中，amplificationParameter 表示 A 乘以 n^(n−1)，而不是单独的 A。测试必须使用这个扩展值，以避免错误的失配。
本文重点在于测试数学的正确性与差分模糊测试，而不是解释数学结构本身。一些代码摘要可能包括 AI 生成的描述，应仔细审查。
附录提供了一个 Balancer 池的 Python 测试示例。
该测试包括：
- 手动引导模糊测试 (MGF) 逻辑
- 合约调用及其 Python 等价物
- 名为
*pure_math_quiet 的函数，它使用 Python 的 Decimal 类型进行精确计算
差分测试的工作原理：
- Python 使用
Decimal 以高精度计算值
- Solidity 计算相同的值
- 测试比较这两个结果，并检查偏差是否可以接受
函数 get_token_balance_pure_math_quiet 使用 Python 的 sqrt()，比 Solidity 中使用的牛顿迭代法更直接和准确地求解。
模糊测试的要点
标准模糊测试探索定义范围内的随机值。如果该范围不包括边缘情况，则模糊测试活动将不会暴露它们。高质量的模糊测试需要达到极端状态的值，尽管花费在测试这些值上的时间可能并不总是有效地揭示问题。
测试边缘情况
两种模糊测试方法很有用。首先，使用典型值测试正常条件。其次，使用极端值测试边缘情况，以查看系统在哪里崩溃。
边缘情况测试回答了基本问题。如果发生溢出，用户是否仍然可以提款？协议可以暂停然后正确恢复吗？系统必须处理故障并恢复，而不会造成进一步的损失。
一个常见的错误是在边缘情况失败时停止测试。相反，继续探索以了解哪些组件继续工作，哪些组件不工作。
正常和边缘情况测试可以结合使用，尽管这会产生不必要的复杂性。清晰的测试通常比复杂的测试更好。
测试环境
集成测试使用真实的外部协议。这些测试运行缓慢，但揭示了实际行为。Fork 测试创建了主网状态的本地副本。Fork 测试速度更快，并且允许修改永远不会在主网上发生的条件。
主网状态很少包含极端值。在 fork 上测试边缘情况时，你必须自己创建极端条件。
手动引导模糊测试 (MGF) 有助于实现这一结果。使用 MGF，测试人员将模糊测试引导到需要探索的特定场景。
题外话：关于 ERC-4626 的模糊测试
ERC-4626 vault 标准包含对存款、取款和份额发行的精度敏感的会计处理。大量取款会影响舍入，并可能导致资金损失。对这些 vault 进行模糊测试需要监控余额、供应和份额行为的逻辑。这使得 ERC-4626 测试比标准模糊测试更具挑战性。
结论
测试交换函数需要两次确认。数学必须产生正确的输出，并且合约必须转移完全相同的数量。差分模糊测试有助于验证这两点。
良好的模糊测试必须反映定义系统的数学公式。Python 非常适合这项工作，因为它提供了高精度工具。差分测试将理论结果与合约的行为进行比较。
必须验证几个方面。不变量必须保持正确。从不同方向计算时，输出计算必须匹配。所有中间值都必须干净地验证。这是确保数学和实现对齐的唯一可靠方法。
手动引导模糊测试 (MGF) 将人类洞察力与自动化探索相结合。这种方法可以发现随机模糊测试经常遗漏的微妙错误。
附录
https://gist.github.com/meditationduck/5b51b49b23cda2220672bdd004f131b9
