以太坊合并后时代，「形式化验证技术」如何检测智能合约安全？

admin

140350
文章

117
评论

2022年10月1日09:46:44评论45 views字数 5291阅读17分38秒阅读模式

所谓的形式化验证，简单而言就是用数学工具进行验证的方法，把代码编成数学模型，从设计到实现整个流程，通过证明手段来证明代码是完备安全的。

形式化验证作为成都链安的核心技术之一，已经帮助上千份智能合约解决安全问题。可能很多人会问，为什么人工不能检测到的问题，形式化验证可以呢？

这是因为，对于形式化验证，可以无需理解合约具体实现的细节，无需构造特定的场景，无需数据枚举；通过逻辑关系凝练出可复用的安全属性，对合约每条路径都会进行严谨的数学公式推理，自动检测每个可能的系统状态及操作，计算出可满足的解，并根据求解结果对比是否违反安全属性最终检测出每条路径下可能存在的安全问题。

以太坊合并“后时代”，智能合约安全同样不可忽视，今天，我们为大家准备了一个以太坊生态的案例，看看下面这份合约是如何在我们的智能合约形式化验证平台“链必验”检测出漏洞的。

链必验，是一款全球领先的“一键式”智能合约形式化验证平台。检测准确率高达97%以上，精确定位风险代码位置并给出修改建议，自动检测智能合约80余项的常规安全漏洞及功能逻辑缺陷。现已拥有生态用户10万+，是全球首套同时支持蚂蚁链、腾讯区块链、FISCO-BCOS、Fabric等的智能合约形式化验证平台。可以极大提高智能合约的人工审计效率，有效降低安全隐患遗漏风险。

01.

准备需要验证的示例Wizard_game.sol

说明：

🧊原合约为以太坊上真实存在的一个巫师决斗合约。为了看起来简单明了并且能够使用形式化检测验证问题，本合约根据逻辑关系只保留巫师决斗超时的处理接口；

🧊resolveTimedOutDuel是更新处理超时情况下的巫师决斗结果的接口；

🧊其中每个巫师有自己的决斗场和决斗能量；

🧊若巫师1满足胜利条件，则将巫师2的决斗能量转移给巫师1，再将巫师2的决斗能量清零。

🧊原始详细代码如下：

// SPDX-License-Identifier: MITpragma solidity ^0.8.0;contract ETHGame{
    struct BattleWizard{  //定义决斗属性        bytes32 currentDuel; //决斗场        uint power;  //决斗能量    }
    mapping (uint => BattleWizard) public wizards;  //记录每个巫师的信息    mapping (bytes32 => mapping (uint => uint256)) public revealedMoves; //记录各个巫师各场的决斗的胜负信息
    function resolveTimedOutDuel(uint256 wizardId1, uint256 wizardId2) public{  //更新处理超时情况下的巫师决斗结果        BattleWizard storage wiz1 = wizards[wizardId1]; //巫师1的决斗属性        BattleWizard storage wiz2 = wizards[wizardId2]; //巫师2的决斗属性        bytes32 duelId = wiz1.currentDuel;  //巫师1的决斗场        require(duelId != 0 && wiz2.currentDuel == duelId); //约束：巫师1的决斗场存在，并且巫师2的决斗场需和巫师1的决斗场相同才可以继续进行后续操作        if (revealedMoves[duelId][wizardId1] != 0){ //如果巫师1满足胜利条件，则更新决斗能量            _updatePower(wiz1,wiz2.power);  //更新巫师1的能量，将巫师2的能量给巫师1            wiz2.power = 0; //巫师2的能量清零        }    }
    function _updatePower(BattleWizard storage wizard, uint256 power) private{  //定义巫师能量更新接口        require(wizard.power + power >= wizard.power);  //确保巫师更新后的能量不少于更新前的能量        wizard.power = wizard.power + power;    //执行巫师能量更新    }}

🧊形式化验证前准备：

①先记录决斗状态更新之前的巫师能量：

uint old_power1 = wiz1.power; //记录巫师1决斗前的能量

uint old_power2 = wiz2.power; //记录巫师2决斗前的能量

②再等决斗状态更新之后增加一条形式化验证属性assert断言：

assert(wiz1.power+wiz2.power == old_power1+old_power2); //添加assert断言：确保状态更新前后总的决斗能量不发生变化

③由于代码逻辑是巫师的决斗能量互相转移，所以总的决斗能量不会发生变化，新增的assert断言条件应当是随时满足的。否则会存在某种逻辑上的漏洞导致总的决斗能量发生的变化，导致assert的限制条件出现了不满足的情况。

🧊增加形式化验证属性详细代码如下：