跑了五百个用例全绿，形式化验证一跑，合约直接炸了

导读： 我已经做了六年的智能合约审计工作, 我见到过太多的测试报告写得漂漂亮亮。然后这些项目一上线。就被人薅走了百万美元。形式化验证和区块链测试的关系。说白了就是体检和CT检查的区别。...

我已经做了六年的智能合约审计工作, 我见到过太多的测试报告写得漂漂亮亮。然后这些项目一上线。就被人薅走了百万美元。形式化验证和区块链测试的关系。说白了就是体检和CT检查的区别。你觉得自己没病。不代表就一定没有病。该查的东西还是要去查一下的。

形式化验证能替代区块链测试吗

不能, 谁要是这么说的话, 谁那就是在忽悠你。形式化验证做的事情是数学层面的证明工作, 它管束的是逻辑上在什么样的条件下方才会出现错误这个范畴, 比如说转账函数在面对并发调用的时候是否有溢出的可能、权限函数是否可以被非所有者身份的主体所绕过等等。

但是它没法管束你在区块链上的真实交互过程, 也处理不了 gas 费用的估算边界问题, 更无法解决你和预言机接口之间所存在的那段质量非常差的代码状况。测试是把路径给跑通, 这个说法是成立的。而验证是要去证明所有的路径都已经处理过了。这两件事压根就不是在同一个层级上的。

我这边负责一个跨链桥的项目, 其中模糊测试的运行时间达到了两周这么久,期间没有发现任何异常情况。但是, 当使用Coq这一工具对核心状态机部分完整地开展了形式化验证工作之后, 结果就直接暴露出来了一条可以进行重入攻击的路径漏洞。

如果这种存在隐患的程序真的被部署到了主网环境中运行, 那么在某种意义上这就相当于给从事安全研究的白帽子人士提供了一台可以随时提取利益的提款机器设备。

区块链测试怎么用形式化验证

实际上, 这个操作过程并没有大家想得那么神秘和难以捉摸, 你先把合约里那些最核心的、绝对不可以发生变化的规则给列清楚, 比如代币的余额绝对不能变成负数, 总的供应量必须保持恒定不变, 以及所有关键的函数在运行的时候都必须经过多个签名的验证才可以执行, 接着, 你就可以去使用Certifa或者K Framework这些工具来做进一步的形式化证明了, 至于测试用例的部分, 你还是按照规定的那样去写代码来跑测试就可以了, 但是那条不变量的清单必须同步地交给验证工具也运行一遍, 只有当这两者的运行结果能够完全对应上的时候, 你才能说系统的稳定性是真正达到了稳当的标准。

不要把期望寄托在一套流程就能完全应对所有场景的想法上面。必须清楚地知道, DeFi借贷协议与NFT市场合约这两者在测试的重点上存在着明显的差异, 这意味着形式化验证在进行建模时所覆盖的范围也必须随之进行调整, 如果选择盲目地套用以往经验, 那么最终的结果只能是白白浪费掉时间。

千万不要把“测试全绿”这个现象当成是你的免死金牌, 形式化验证这个东西它确实不是什么银弹, 但是它在你的系统上线之前, 确实是你最后的一个从数学意义上讲非常靠谱的保险设施, 如果你在这一步上面为了少出钱或者是省事儿, 那么你就是在为自己增加一份担心和风险。