SMTChecker 检查合约漏洞的超能力

这篇文章主要介绍了SMTChecker 检查合约漏洞的超能力 ,文中通过代码以及文档配合进行讲解,很详细,它对在座的每个人的研究和工作具有很经典的参考价值。 如果需要,让我们与区块链资料网一起学习。

https://www.interchains.cc/24546.html

SMTChecker 检查合约漏洞的超能力是很好的区块链资料,他说明了区块链当中的经典原理,可以给我们提供资料,SMTChecker 检查合约漏洞的超能力学习起来其实是很简单的,

不多的几个较为抽象的概念也很容易理解,之所以很多人感觉SMTChecker 检查合约漏洞的超能力比较复杂,一方面是因为大多数的文档没有做到由浅入深地讲解,概念上没有注意先后顺序,给读者的理解带来困难

SMTChecker 检查合约漏洞的超能力

  • 安全
  • SMTChecker

SMTChecker 检查合约漏洞的超能力

  • 原文:https://medium.com/@sblowpckcr/smtchecker-almost-practical-superpower-5a3efdb3cf19
  • 译文出自:登链翻译计划
  • 译者:翻译小组
  • 校对:Tiny 熊
  • 本文永久链接:learnblockchain.cn/article…

理论:什么是SMTChecker?

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

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

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

SMTChecker是一个对合约进行形式化验证的工具:你定义一个规范(你的合约应该做什么),SMTChecker 以证明该合约符合该规范。如果不符合,SMTChecker通常会给你一个具体的反例:一个破坏规范的交易序列。

最重要的是什么?如果你使用Solidity,你已经有了SMTChecker – 它是Solidity编译器的一部分。

不过它决不是一个无懈可击的解决方案 — 验证错误是慢的。最重要的是,要定义一个完整的规范是非常困难的。但即使如此,SMTChecker仍然值得一试。

以跳棋合约为例

该合约实现了一个计数器 — 一个在8×8棋盘上玩的跳棋(或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);     } }

AMMPairEngineaddLiquidityStateChange作为一个内部函数。它是由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真的很难证明这个断言,所以我们不能真的依赖它。

SMTChecker 检查合约漏洞的超能力

SMTChecker 检查合约漏洞的超能力

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

SMTChecker 检查合约漏洞的超能力

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

SMTChecker 检查合约漏洞的超能力

结论

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

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

其他的替代品

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

鸣谢

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


本翻译由 CellETF 赞助支持。

  • 发表于 4小时前
  • 阅读 ( 59 )
  • 学分 ( 56 )
  • 分类:以太坊eth

部分转自网络,侵权联系删除www.interchains.cchttps://www.interchains.cc/24546.html

区块链毕设网(www.interchains.cc)全网最靠谱的原创区块链毕设代做网站 部分资料来自网络,侵权联系删除! 最全最大的区块链源码站 ! QQ3039046426
区块链知识分享网, 以太坊dapp资源网, 区块链教程, fabric教程下载, 区块链书籍下载, 区块链资料下载, 区块链视频教程下载, 区块链基础教程, 区块链入门教程, 区块链资源 » SMTChecker 检查合约漏洞的超能力

提供最优质的资源集合

立即查看 了解详情