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

admin 2022年10月1日09:46:44评论36 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的限制条件出现了不满足的情况。

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

// 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{ //巫师1和巫师2决斗属性更新接口 BattleWizard storage wiz1 = wizards[wizardId1]; BattleWizard storage wiz2 = wizards[wizardId2];
uint old_power1 = wiz1.power; //记录巫师1决斗前的能量 uint old_power2 = wiz2.power; //记录巫师2决斗前的能量
bytes32 duelId = wiz1.currentDuel; require(duelId != 0 && wiz2.currentDuel == duelId); if (revealedMoves[duelId][wizardId1] != 0){ _updatePower(wiz1,wiz2.power); wiz2.power = 0; }
assert(wiz1.power+wiz2.power == old_power1+old_power2); //添加assert断言:确保状态更新前后总的决斗能量不发生变化 }
function _updatePower(BattleWizard storage wizard, uint256 power) private{ require(wizard.power + power >= wizard.power); wizard.power = wizard.power + power; }}


2.合约上传 

🧊新增项目

“链必验”工具中创建需要检测的项目。本次检测的项目为ETH类型项目,那么根据需求点击工具左上方“新增项目”按钮,输入项目名称,选择项目类型,点击确定。

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


🧊新增合约文件夹

选择刚创建好的项目,点击工具左上方的“新增合约文件夹”按钮,输入文件夹名称。

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


🧊上传合约文件

选择刚创建好的文件夹,点击工具左上方的“上传”按钮,上传准备好检测的合约文件。

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


3.合约检测 

🧊新增项目

将待检测合约上传完成之后,选择此合约,按照合约内容输入检测参数,然后点击开始检测。

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


4.查看结果

待合约检测完成之后,查看检测结果,通过代码定位、错误描述、修复建议了解明确该漏洞的具体信息,然后查看代码逻辑寻找问题并进行修复。

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


5.结果分析

经分析,产生此漏洞的原因是在执行resolveTimedOutDuel接口更新巫师1和巫师2的决斗属性时,未考虑巫师1和巫师2相等的情况,在此场景下,巫师1的决斗能量会先翻倍,然后再清零,导致巫师1状态更新前后总的决斗能量发生了改变,所以导致了assert断言的失败。

6.形式化验证逻辑

在本合约中,由于巫师1和巫师2之间执行决斗能量转移,所以逻辑关系为巫师1和巫师2决斗能量之和为定值,不发生变化,所以可以编写出形式化验证属性:“assert(wiz1.power+wiz2.power == old_power1+old_power2);”;

其检测流程为:

🧊由于输入不是真实值,所以会将wizardId1,wizardId2抽象为符号值;此时存在两种情况:

① wizardId1 != wizardId2;

② wizardId1 ==wizardId2;

🧊在执行_updatePower接口前先记录wiz1.power和wiz2.power的值,用old_power1,old_power2表示,此时同样存在两种情况:

① 当wizardId1 != wizardId2时: 

old_power1+old_power2

② 当wizardId1 == wizardId2时:

old_power1+old_power2 = 2*old_power1 = 2*old_power2

🧊待_updatePower接口执行完成之后,wiz1.power和wiz2.power的值发生了改变,依然存在两种情况:

①当wizardId1 != wizardId2时: 

由于wiz1.power=old_power1+old_power2,wiz1.power=0,所以存在:

wiz1.power+wiz2.power = old_power1+old_power2+0 = old_power1+old_power2;

此时巫师1和巫师2决斗能量之和不变;

②当wizardId1 == wizardId2时: 由于wiz2.power=0,所以存在:

wiz1.power+wiz2.power = 2*wiz2.power = 2*0 = 0。

此时巫师1和巫师2决斗能量之和为0。

🧊由于形式化验证会求解各条路径下的值,所以当满足wizardId1 == wizardId2的路径时,wiz1.power+wiz2.power == 0,若此时同时满足old_power1+old_power2 != 0时,会出现一个非0值等于0的错误,即“ old_power1+old_power2 != wiz1.power+wiz2.power ”,导致求解结果违反了形式化属性的限制条件,从而发现程序漏洞。

7.问题解决

此时在resolveTimedOutDuel接口中添加一个限制条件“require(wizardId1 != wizardId2);”,确保在执行决斗属性更新时巫师1和巫师2不相等,查看是否还存在此问题。

8.漏洞检测难度人工难以察觉,随机测试难以出现这种情况

对于智能合约的验证,通常是伴随人工验证,靠自身经验不断尝试枚举各项可能不满足的输入条件,从而比对输出来判断是否存在漏洞;其存在的问题就是人工成本昂贵,测试时无法覆盖到所有的路径,测试具有一定的机械性、重复性、工作量往往较大。

而对于智能合约的另外一种验证方式-fuzzing模糊测试,虽然可以解决人工成本昂贵的问题,但是由于其没有实际执行规则机制原因,仅靠“蛮力”不断枚举各个输入,同样存在可能出现某种输入漏掉的问题,并且无法根据路径检测出一些逻辑性的漏洞。

因此,形式化验证工具依然是智能合约安全的保障利器。目前,链必验已放免费试用,如果您想更深入了解和体验产品,可添加下方微信咨询。

作为一家致力于区块链安全生态建设的全球领先区块链安全公司,也是最早将形式化验证技术应用到区块链安全的公司,成都链安目前已与国内外头部区块链企业建立了深度合作;为全球2500多份智能合约、100多个区块链平台和落地应用系统提供了安全审计与防御部署服务。成都链安同时具备全链条打击虚拟货币犯罪和反洗钱技术服务能力,为公安等执法部门提供案件前、中、后期全链条技术支持服务1000+,包括数起进入混币器平台Tornado Cash的案件,成功协助破获案件总涉案金额数百亿。欢迎点击公众号留言框,与我们联系。

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

微信扫码添加,开通产品免费试用

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

更多智能合约安全检测相关内容戳这里

▶智能合约安全审计利器“链必验”,如何检测出14W个地址合约存在的K值校验问题?
▶联盟链智能合约安全检测工具邀您免费来体验
▶如何为你的智能合约“上保险”,形式化验证了解一下?
▶智能合约自动检测工具『链必验』,如何带你解锁Web3.0世界
▶链必验V3.1版本上线 | 找100人,试试冰山力量


Web3安全态势深度研报下载



2022年上半年Web 3安全态势如何?


成都链安官方微信公众号后台留言回复关键词:研报 即可获取《成都链安2022年上半年Web 3安全态势深度研报》PDF下载链接!


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


点个关注了再走吧~

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



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

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

原文始发于微信公众号(成都链安):以太坊合并“后时代”,「形式化验证技术」如何检测智能合约安全?

  • 左青龙
  • 微信扫一扫
  • weinxin
  • 右白虎
  • 微信扫一扫
  • weinxin
admin
  • 本文由 发表于 2022年10月1日09:46:44
  • 转载请保留本文链接(CN-SEC中文网:感谢原作者辛苦付出):
                   以太坊合并后时代,「形式化验证技术」如何检测智能合约安全?http://cn-sec.com/archives/1319634.html

发表评论

匿名网友 填写信息