LOADING...
LOADING...
LOADING...
当前位置: 玩币圈首页 > 新闻观点 > 形式化验证——合约安全的终局解决方案

形式化验证——合约安全的终局解决方案

2023-09-12 金色财经 来源:区块链网络

作者:@dvzhangtz;来源:作者推特@dvzhangtz

最近看了一些形式化验证的项目,感觉在新周期中其依旧会是有趣的叙事。

但该技术作为合约安全中最重要的组成,却在推上几乎看不到中文帖。所以总结了一下学习中得到的认知...

现在,你可以用五分钟拿走这些认知。

背景:智能合约是区块链世界核心之一,合约发生安全问题,Dapp 中的钱就全部凉凉。 根据 Rekt 榜上可以看到,因为合约安全造成的直接损失单次最高达 $ 600M,间接损失更加严重,合约不安全会令社区对项目失去信心。https://rekt.news/leaderboard/

传统上如果为了让合约更安全,思路是叠甲,比如:

1 使用标准函数包如@OpenZeppelin的包来写代码,让代码更安全

2 写完后使用一些工具进行初步筛查,看有没有问题

3 写一些测试程序,对合约分模块用样本数据测试

4 ......

但铠甲再厚也总会有漏洞,测试程序也只能用一些样本进行测试,不可能穷尽所有可能性。所以这些方法都只能降低出现安全问题的可能性,不能保证合约没有问题 有没有一种办法能像预言家验狼人一样,能确保合约没有某方面安全漏洞? 答案是——形式化验证

想进行一次形式化验证,需要几步:

1. 写形式化规范,里面定义我们想要验证的东西

2. 使用形式化分析框架验证,这类工具会自动验证合约是否符合我们定义的规范

3. 发现某些情况下出现问题

4. 改代码解决问题

一个真实案例:巫师决斗@CHZWZRDS

https://github.com/dapperlabs/cheezyverse/blob/fef271db4c18c00949de291da0b46a1397216306/contracts/BasicTournament.sol#L2059…

下面的代码时说:在游戏超时时,巫师 1 会吸走巫师 2 的能量,巫师 2 能量清零。

作为一个 gamefi,这个能量自然很重要。

理论上这个能量只能在两个巫师之间转移,但如果黑客发现这段程序的漏洞,可以让能量凭空增加 / 消失,无疑会对这个 Gamefi 造成重大影响。

使用正常的安全验证方式,我们用了几个测试数据,发现一切都运行的很 nice,我们甚至准备直接上链部署了。 不过等等,为什么不试试形式化验证?

第一步:定义形式化规范

我们希望能量只会在巫师之间相互转移,不会凭空增加/消失,也就是: wiz1.power + wiz2.power = old_wiz1.power + old_wiz2.power 。

第二步:形式化分析框架自动验证

这类工具实质上是一种用于探索合约执行的所有可能路径的技术,以确保在所有可能的执行路径上都满足规范。

第三步:发现问题

发现了一个问题!一个神奇的问题,如果决斗的两个巫师是一个人,也就是决斗双方的地址一致,就会让该用户的能量清零! 第四步:改正问题 既然发现了问题,其实很容易改,我们只需要加一行代码,预先审核,确保决斗双方不是一个人就好啦~

类似的问题还有经典的 K 值校验问题。Uniswap 的核心是恒定乘积模型 K=x*y,其中的 K 值是该 pair 合约持有代币数量的乘积,且要求之后的每一笔交易完成后 K 值须增加(手续费) 如果有黑客发现了合约中的漏洞,可以使得自己的交易不用符合恒定乘积,这样合约就是提款机了,用上文思路也可避免该问题。

从上文可以感受到形式化验证的几个特点:

1. 终局性:在所验证问题上可以证出合约不存在某些问题;

2. 对规范的依赖(严重):上文只是验证了一个规范,但实际合约会面临的问题很多,我们可能会漏掉某些规范,而书写规范本身也是比较耗人力的,所以形式化验证主要是对合约一些关键属性进行验证。

3. 性能问题(严重):使用形式化分析框架自动验证,本质上是探索合约执行的所有可能路径上都符合规范,这有可能会遇到状态爆炸和路径爆炸问题,同时其底层使用 SMT 求解器和其他约束求解器,这些求解器也是耗算力的大户。 所以,未来将这件事以一个什么样的方式外包出去降低成本,也许能促进其发展。

如果想进行形式化验证,相关工具如下:?

书写形式化规范的语言

Act:https://github.com/ethereum/act

Scribble:https://docs.scribble.codes

Dafny:https://github.com/dafny-lang/dafny…

用于检验正确性的验证器

Certora Prover:https://docs.certora.com/en/latest/index.html…

Solidity SMTChecker:https://github.com/ethereum/solidity…

solc-verify:https://github.com/SRI-CSL/solidity…

KEVM:https://github.com/runtimeverification/evm-semantics…

查看更多

—-

编译者/作者:金色财经

玩币圈申明:玩币圈作为开放的资讯翻译/分享平台,所提供的所有资讯仅代表作者个人观点,与玩币圈平台立场无关,且不构成任何投资理财建议。文章版权归原作者所有。

LOADING...
LOADING...