SMTChecker 检查合约漏洞的超能力

SMTChecker 检查合约漏洞的超能力

理论：什么是SMTChecker？

你是否敢打赌保证，你刚刚部署的合约没有严重的漏洞吗？如果你像我一样，想必答案是一个响亮的 不。

我在传统的软件工程中见过足够多的黑客，知道你永远不可能100%确定。这很可怕，但不同技术的组合使用可以让我们相当接近到所需要的信心。

SMTChecker就是这样给我信心的技术之一。

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)但非准确(accurate)模式）。

~/src/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做了一个详尽的分析：在一个循环中调用了所有的公共函数，其中有所有可能的输入，有所有可能的组合。实际上，它并没有采用蛮力方法(那样太昂贵了)，而是依靠数学来实现(我不会假装完全理解了，有一些细节在这里)。

下面是另一个例子，说明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));
    }
}
~/src/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代币；
  • 任何人可以再次存入x1X和y1Y代币，只要这不改变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函数），让我们试试吧

~/src/smtchecker_demo ❯❯❯ solc --model-checker-engine chc --model-checker-show-unproved --model-checker-timeout 0 --model-checker-contracts 3.sol
...

这要花点时间（最多几个小时），对于一个简单的不变性来说，这可能不够实用。

是什么会使它变慢？我的猜测是地址和外部调用（transferFrom）-- SMTChecker会将它们建模为未知实现的函数，可以做任何事情，包括回调你的合约。这很好，有时也很有用（可以可以帮助发现重入问题），但对于我们的场景来说并不实用。

我们重组合约：把所有的外部调用分出来，变成一个单独的合约。我们的 核心合约将保持一个最小的状态，只作为一个数字计算者。额外的好处是--使它几乎自动遵循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合约中。

~/src/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'
    }
    // ...
}
~/src/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指出，可能发生并不足以称之为 部分成功--而是SMTChecker真的很难证明这个断言，所以我们不能真的依赖它。

WechatIMG386

image-20210909173722020

顺便说一句，你可以手动证明最后一个例子中的数学公式，但这显然没有扩展性，原代码中有断言违反，有一个反例：

1_H28r2hdKhCL9JAgarE53iA

证明新代码中没有违反断言的情况：

1_F9k9Dwa8_Lba-4zTG68q9w

结论

当我们编写合约的时候考虑到它，那每个人都可以享受到SMTChecke自动形式化验证的好处。

我希望能花些时间深入研究SMTChecker，敬请关注。

其他的替代品

  1. Manticore是一个符号执行引擎，可以做与SMTChecker类似的事情。一方面它是高度可编程的，但它做更少的事情（invariantAddLiquidity有两个参数，SMTChecker为它们探索了所有可能的输入；Manticore不会这样做）。另一方面，这些事情是可实现的，另外我们对验证过程有更多的控制（例如也许我们可以对外部合约做一些假设？）
  2. Echidna是一个模糊工具--使用类似于不变性的想法，随机地试图找到破坏它们的输入。它并不能证明不变性的成立（也许它只是没能找到那个边缘案例），但可以快速发现很多非边缘案例的缺陷。Echidna使用与Manticore相同的语法，因此（至少在理论上）它们都可以并行使用。
  3. Scribble采取了一种不同的方法--用动态不变性对每个函数进行注解。它使用自己的语言来描述不变性，并且可以用物化的不变性来记录你的代码。
  4. 大量的静态分析/其他模糊分析工具--它们非常有用，但不在本文的讨论范围之内。

鸣谢

Alberto Cuesta Cañada为上述大多数参考资料和最小AMM的想法。

本翻译由 CellETF 赞助支持。

点赞 0
收藏 4
分享
本文参与登链社区写作激励计划 ，好文好收益，欢迎正在阅读的你也加入。

0 条评论

请先 登录 后评论
翻译小组
翻译小组
0x9e64...7c84
大家看到好的文章可以在 GitHub 提 Issue： https://github.com/lbc-team/Pioneer/issues 欢迎关注我的 Twitter： https://twitter.com/UpchainDAO

翻译小组

如果觉得我的文章对您有用，请随意打赏。你的支持将鼓励我继续创作！