译文出自:登链翻译计划 [1]
译者:翻译小组 [2]
校对:Tiny 熊 [3]
理论:什么是 SMTChecker?
你是否敢打赌保证,你刚刚部署的合约没有严重的漏洞吗?如果你像我一样,想必答案是一个响亮的
不
。
我在传统的软件工程中见过足够多的黑客,知道你永远不可能 100% 确定。这很可怕,但不同技术的组合使用可以让我们相当接近到所需要的信心。
SMTChecker[4] 就是这样给我信心的技术之一。
SMTChecker 是一个对合约进行形式化验证的工具:你定义一个规范(你的合约应该做什么),SMTChecker 以证明该合约符合该规范。如果不符合,SMTChecker 通常会给你一个具体的反例:一个破坏规范的交易序列。
最重要的是什么?如果你使用 Solidity,你已经有了 SMTChecker - 它是 Solidity 编译器的一部分。
不过它决不是一个无懈可击的解决方案 -- 验证错误是慢的。最重要的是,要定义一个完整的规范是非常困难的。但即使如此,SMTChecker 仍然值得一试。
以跳棋合约为例
该合约实现了一个计数器 -- 一个在 8x8 棋盘上玩的跳棋(或 draughts)游戏的棋子。
我们将设计一个
LazyCounter
:它不能移动,但可以通过捕获 (capture) 相邻的“支点”棋子,
跳到
对角线格子:如果当前在(0,0),想要支点棋子是(1,1),我最终会跳在(2,2),很简单吧。
// SPDX-License-Identifier: MIT pragma solidity >=0.8.7; contract LazyCounter { int8 private x; int8 private y; constructor(int8_x, int8_y) { // check that we're within the board boundaries require(_x >= 0 &&_x < 8 &&_y >= 0 &&_y < 8); x =_x; y =_y; } /// @dev capture a piece at (_x,_y) function capture(int8_x, int8_y) public { require(_x >= 0 &&_x < 8 &&_y >= 0 &&_y < 8); int8 deltaX =_x - x; int8 deltaY =_y - y; // check that we're capturing a diagonally adjacent piece require((deltaX == 1 || deltaX == -1) && (deltaY == 1 || deltaY == -1)); // jump over x =_x + deltaX; y =_y + deltaY; } /// @dev can't leave the board under any conditions function invariant() public view { assert(x >= 0 && x < 8 && y >= 0 && y < 8); } }
代码很简单:我们在一个给定的位置创建一个计数器。然后它可以捕捉其他棋子。
有趣的是最后一个函数 (invariant),它定义了一个在任何时候都必须保持的不变性。这个不变性很简单--计数器不能离开棋盘。让我们编译合约,看看我们的不变性是否被破坏(注意额外的
solc
参数--它们开启了 SMTChecker 的积极 (aggressive)[5] 但非准确 (accurate)[6] 模式)。
~/hide/smtchecker_demo ❯❯❯ solc 1.sol --model-checker-engine chc --model-checker-show-unproved --model-checker-timeout 0 Warning: CHC: Assertion violation happens here. Counterexample: x = 0, y = 8Transaction trace: LazyCounter.constructor(2, 6) State: x = 2, y = 6 LazyCounter.capture(1, 7) State: x = 0, y = 8 LazyCounter.invariant() --> 1.sol:32:9: | 32 | assert(x >= 0 && x < 8 && y >= 0 && y < 8); | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
哎呀,我们的不变性被破坏了。SMTChecker 甚至给了我们一个反例 ! 如果我们的棋子在 (2, 6),而它捕获了 (1, 7) 的棋子,那么它最终会在 (0, 8),也就是棋盘外。我们忘记了在捕获棋子后检查落点位置的有效性。
重要的是要理解 SMTChecker 刚刚做了什么:我们给了它一个合约,其中有一组操作边界 (定义有效输入的
require
语句) 和一个不变性。SMTChecker 做了一个 详尽的分析 :在一个循环中调用了 所有的公共函数 ,其中有 所有可能的输入 ,有 所有可能的组合 。实际上,它并没有采用蛮力方法 (那样太昂贵了),而是依靠 数学来实现 (我不会假装完全理解了,有一些细节在这里 [7])。
下面是另一个例子,说明 SMTChecker 在尝试长的交易序列来测试不变性:一个实现国际象棋 " 马 " 的合约。我们将添加一个已知是无效的不变式,只是为了让 SMTChecker 找出:马不能到达(7,7)的位置的反例 :
// SPDX-License-Identifier: MIT pragma solidity >=0.8.7; contract Knight { int8 private x; int8 private y; function isValidPosition() internal view returns (bool) { return x >= 0 && x < 8 && y >= 0 && y < 8; } function move1() public { x += 1; y += 2; require(isValidPosition()); } function move2() public { x += 2; y += 1; require(isValidPosition()); } function move3() public { x += 2; y -= 1; require(isValidPosition()); } function move4() public { x -= 1; y -= 2; require(isValidPosition()); } function move5() public { x -= 1; y += 2; require(isValidPosition()); } function move6() public { x -= 2; y += 1; require(isValidPosition()); } function move7() public { x -= 2; y -= 1; require(isValidPosition()); } function move8() public { x -= 1; y -= 2; require(isValidPosition()); } function get_to_7_7() public view { assert(!(x == 7 && y == 7)); } }
~/hide/smtchecker_demo ❯❯❯ solc 2.sol --model-checker-engine chc --model-checker-show-unproved --model-checker-timeout 0 Warning: CHC: Assertion violation happens here. Counterexample: x = 7, y = 7Transaction trace: Knight.constructor() State: x = 0, y = 0 Knight.move2() Knight.isValidPosition() -- internal call State: x = 2, y = 1 Knight.move2() Knight.isValidPosition() -- internal call State: x = 4, y = 2 Knight.move5() Knight.isValidPosition() -- internal call State: x = 3, y = 4 Knight.move1() Knight.isValidPosition() -- internal call State: x = 4, y = 6 Knight.move3() Knight.isValidPosition() -- internal call State: x = 6, y = 5 Knight.move1() Knight.isValidPosition() -- internal call State: x = 7, y = 7 Knight.get_to_7_7() --> 2.sol:61:9: | 61 | assert(!(x == 7 && y == 7)); | ^^^^^^^^^^^^^^^^^^^^^^^^^^^
太棒了, SMTChecker 给了我们将马从(0,0)移到(7,7)的步骤序列。
实践一下
免责声明:其他一切都只是一个大实验,看看它如何在
生产环境
中发挥作用。可能还有其他方法,我不会声称我已经找到了“最正确”方法。
让我们做一些更实际的事情,这也是 AMM 的一部分:流动性提供者为交易对增加流动性(这里不进行实际交易)。
-
构造时,所有者存入一些(
x
) X 代币和一些(y
) Y 代币,AMM 则产生x * y
LP 代币; -
任何人可以再次存入
x1
X 和y1
Y 代币,只要这不改变 X/Y 余额的比例(x1/y1 == xReserves / yReserves
),AMM 生成totalSupply(LP) * (x1 / xReserves)
LP 代币; -
只支持精度为 18 ERC20 代币
功能只有这些,甚至连 LP 代币分发都没有,代码如下:
// SPDX-License-Identifier: MIT pragma solidity >=0.8.7; /// @dev bare minimum of IERC20 and IERC20Metadata that we'll use interface IERC20Metadata { function decimals() external view returns (uint8); function transferFrom(address sender, address recipient, uint256 amount) external returns (bool); } contract AMMPair { IERC20Metadata x; IERC20Metadata y; uint256 xReserves; uint256 yReserves; uint256 totalSupply; constructor(IERC20Metadata_x, IERC20Metadata_y, uint256 depositX, uint256 depositY) { require(_x.decimals() == 18); require(_y.decimals() == 18); require(depositX != 0); require(depositY != 0); x =_x; y =_y; xReserves = depositX; yReserves = depositY; totalSupply = depositX * depositY / 1e18; x.transferFrom(msg.sender, address(this), depositX); y.transferFrom(msg.sender, address(this), depositY); } function addLiquidity(uint256 depositX, uint256 depositY) public returns (uint256) { require(depositX != 0, "depositX != 0"); require(depositY != 0, "depositY != 0"); require(depositX * 1e18 / depositY == xReserves * 1e18 / yReserves, "unbalancing"); uint256 extraSupply = depositX * totalSupply / xReserves; xReserves += depositX; yReserves += depositY; totalSupply += extraSupply; x.transferFrom(msg.sender, address(this), depositX); y.transferFrom(msg.sender, address(this), depositY); return extraSupply; } }
我们可以添加什么样不变性?不多 -- 也许储备不为空(
xReserves != 0 && yReserves != 0
),仅此而已。
让我们把不变性的定义扩展,称之为
动态不变性
:知道执行
addLiquidity
之前和之后的状态,我们可以断言什么?
contract AMMPair { // ... function invariantAddLiquidity(uint256 depositX, uint256 depositY) public { uint256 oldSupply = totalSupply; uint256 oldXReserves = xReserves; uint256 supplyAdded = addLiquidity(depositX, depositY); assert(depositX / oldXReserves == supplyAdded / oldSupply); revert("all done"); } }
注意结尾处的
revert()
--它确保了此不变函数没有副作用(即不会修改状态,可以把它看作是一个
view
函数),让我们试试吧
~/hide/smtchecker_demo ❯❯❯ solc --model-checker-engine chc --model-checker-show-unproved --model-checker-timeout 0 --model-checker-contracts 3.sol ...
这要花点时间(最多几个小时),对于一个简单的不变性来说,这可能不够实用。
是什么会使它变慢?我的猜测是地址和外部调用(
transferFrom
)-- SMTChecker 会将它们建模为未知实现的函数,可以做任何事情,包括回调你的合约。这很好,有时也很有用(可以可以帮助发现重入问题 [8]),但对于我们的场景来说并不实用。
我们重组合约:把所有的外部调用分出来,变成一个单独的合约。我们的
核心
合约将保持一个最小的状态,只作为一个数字计算者。额外的好处是--使它几乎自动遵循 CEI (检查-效果-交互)的原则。
contract AMMPairEngine { uint256 xReserves; uint256 yReserves; uint256 totalSupply; constructor(uint256 depositX, uint256 depositY) { require(depositX != 0, "depositX != 0"); require(depositY != 0, "depositY != 0"); xReserves = depositX; yReserves = depositY; totalSupply = depositX * depositY / 1e18; } function addLiquidityStateChange(uint256 depositX, uint256 depositY) internal returns (uint256) { require(depositX != 0, "depositX != 0"); require(depositY != 0, "depositY != 0"); require( (depositX * 1e18) / depositY == (xReserves * 1e18) / yReserves, "unbalancing" ); uint256 extraSupply = (depositX * totalSupply) / xReserves; xReserves += depositX; yReserves += depositY; totalSupply += extraSupply; return extraSupply; } function invariant1() public view { assert(xReserves > 0); assert(yReserves > 0); } function invariantAddLiquidity(uint256 depositX, uint256 depositY) public { uint256 oldSupply = totalSupply; uint256 oldXReserves = xReserves; uint256 supplyAdded = addLiquidityStateChange(depositX, depositY); assert(depositX / oldXReserves == supplyAdded / oldSupply); revert("all done"); } } contract AMMPair is AMMPairEngine { IERC20 x; IERC20 y; constructor( IERC20_x, IERC20_y, uint256 depositX, uint256 depositY ) AMMPairEngine(depositX, depositY) { require(_x.decimals() == 18); require(_y.decimals() == 18); x =_x; y =_y; x.transferFrom(msg.sender, address(this), depositX); y.transferFrom(msg.sender, address(this), depositY); } function addLiquidity(uint256 depositX, uint256 depositY) public { addLiquidityStateChange(depositX, depositY); x.transferFrom(msg.sender, address(this), depositX); y.transferFrom(msg.sender, address(this), depositY); } }
AMMPairEngine
有
addLiquidityStateChange
作为一个内部函数。它是由
AMMPair
调用的(继承自
AMMPairEngine
)。
AMMPairEngine
唯一的公共函数是不变性函数。如果我们不希望它们出现在部署的代码中,则它们可以被移到
AMMPairEngineTest is AMMPairEngine
合约中。
~/hide/smtchecker_demo ❯❯❯ time solc --model-checker-engine chc --model-checker-show-unproved --model-checker-timeout 0 --model-checker-contracts 3.sol:AMMPairEngine 3.sol Warning: CHC: Division by zero happens here. Counterexample: xReserves = 2, yReserves = 2, totalSupply = 0 depositX = 1 depositY = 1 oldSupply = 0 oldXReserves = 1 supplyAdded = 0Transaction trace: AMMPairEngine.constructor(1, 1) State: xReserves = 1, yReserves = 1, totalSupply = 0 AMMPairEngine.invariantAddLiquidity(1, 1) AMMPairEngine.addLiquidityStateChange(1, 1) -- internal call --> 3.sol:117:43: | 117 | assert(depositX / oldXReserves == supplyAdded / oldSupply); | ^^^^^^^^^^^^^^^^^^^^^^^Warning: CHC: Assertion violation happens here. --> 3.sol:117:9: | 117 | assert(depositX / oldXReserves == supplyAdded / oldSupply); | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^solc --model-checker-engine chc --model-checker-show-unproved 0 3.sol 7.11s user 0.17s system 98% cpu 7.357 total
可以看到会出现除以 0 会导致违反断言。反例(
depositX = 1; depositY = 1; oldSupply = 0
)使问题很明显:合约创建者存入了 1e-18 的 X 和 1e-18 的 Y 代币。这使得合约发行了 0 个 LP 代币(1e-36 太小了,无法用 18 位精度的数学表示)。我们将切换到 36 进制的数学,这应该可以解决这个问题。
contract AMMPairEngine { // ... constructor(uint256 depositX, uint256 depositY) { // ... totalSupply = depositX * depositY; // removed '/1e18' } // ... }
~/hide/smtchecker_demo ❯❯❯ time solc --model-checker-engine chc --model-checker-show-unproved --model-checker-timeout 0 --model-checker-contracts 3.sol:AMMPairEngine 3.sol Warning: CHC: Assertion violation might happen here. --> 3.sol:117:9: | 117 | assert(depositX / oldXReserves == supplyAdded / oldSupply); | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^solc --model-checker-engine chc --model-checker-show-unproved 0 3.sol 75.19s user 0.50s system 99% cpu 1:16.27 total
注意这个变化:现在没有除以 0 违反断言的情况,现在是
Assertion violation might happen here
。这里表达了不确定。我需要做更多的调查以更好地了解这里发生了什么。
更新 09/05/2021 : Leo Alt[9] 指出,
可能发生
并不足以称之为
部分成功
--而是 SMTChecker 真的很难证明这个断言,所以我们不能真的依赖它。
WechatIMG386 image-20210909173722020
顺便说一句,你可以手动证明最后一个例子中的数学公式 [10],但这显然没有扩展性,原代码中有断言违反,有一个反例:
1_H28r2hdKhCL9JAgarE53iA
证明新代码中没有违反断言的情况:
1_F9k9Dwa8_Lba-4zTG68q9w
结论
当我们编写合约的时候考虑到它,那每个人都可以享受到 SMTChecke 自动形式化验证的好处。
我希望能花些时间深入研究 SMTChecker,敬请关注。
其他的替代品
-
Manticore[11] 是一个符号执行引擎,可以做与 SMTChecker 类似的事情。一方面它是高度可编程的,但它做更少的事情(
invariantAddLiquidity
有两个参数,SMTChecker 为它们探索了所有可能的输入;Manticore 不会这样做)。另一方面,这些事情是可实现的,另外我们对验证过程有更多的控制(例如也许我们可以对外部合约做一些假设?) -
Echidna[12] 是一个模糊工具--使用类似于不变性的想法,随机地试图找到破坏它们的输入。它并不能 证明 不变性的成立(也许它只是没能找到那个边缘案例),但可以快速发现很多非边缘案例的缺陷。Echidna 使用与 Manticore 相同的语法,因此(至少在理论上)它们都可以并行使用。
-
Scribble[13] 采取了一种不同的方法--用 动态不变性 对每个函数进行注解。它使用自己的语言来描述不变性,并且可以用物化的不变性来记录你的代码。
-
大量的静态分析 / 其他模糊分析工具--它们非常有用,但不在本文的讨论范围之内。
鸣谢
Alberto Cuesta Cañada[14] 为上述大多数参考资料和最小 AMM 的想法。
本翻译由 CellETF[15] 赞助支持。
来源: https://medium.com/@sblowpckcr/smtchecker-almost-practical-superpower-5a3efdb3cf19
参考资料
[1]
登链翻译计划 : https://github.com/lbc-team/Pioneer
[2]
翻译小组 : https://learnblockchain.cn/people/412
[3]
Tiny 熊 : https://learnblockchain.cn/people/15
[4]
SMTChecker: https://docs.soliditylang.org/en/v0.8.7/smtchecker.html
[5]
积极 (aggressive): https://docs.soliditylang.org/en/v0.8.7/smtchecker.html#timeout
[6]
准确 (accurate): https://docs.soliditylang.org/en/v0.8.7/smtchecker.html#constrained-horn-clauses-chc
[7]
这里 : https://docs.soliditylang.org/en/v0.8.7/smtchecker.html#smt-and-horn-solvers
[8]
可以可以帮助发现重入问题 : https://docs.soliditylang.org/en/v0.8.7/smtchecker.html#external-calls-and-reentrancy
[9]
Leo Alt: https://twitter.com/leonardoalt
[10]
你可以手动证明最后一个例子中的数学公式 : https://github.com/sblOWPCKCR/smtchecker_demo/blob/main/z3.ipynb
[11]
Manticore: https://github.com/trailofbits/manticore
[12]
Echidna: https://github.com/crytic/echidna
[13]
Scribble: https://consensys.net/diligence/scribble/
[14]
Alberto Cuesta Cañada: https://medium.com/u/8206cbb70805?source=post_page-----5a3efdb3cf19--------------------------------
[15]