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

作者：@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 值须增加(手续费) 如果有黑客发现了合约中的漏洞，可以使得自己的交易不用符合恒定乘积，这样合约就是提款机了，用上文思路也可避免该问题。

形式化验证