形式化验证让区块链测试更靠谱

智能合约在区块链上部署以后, 几乎难以进行更改是常有的状况, 这使得测试成为开发社群的痛点。传统测试方法是靠运行代码来确定是否报错, 然而一旦出现问题, 就会造成实实在在的经济损失。形式化验证的问世, 正在打破这种困境, 它并非简单地进行测试,而是运用数学方法来证实代码不存在缺陷。

形式化验证为什么能发现测试发现不了的漏洞

将传统的测试比作在黑漆麻乌的屋子里摸索物件, 你仅能够触及部分角落, 测试覆盖率高并不意味着代码逻辑全然无误。形式化验证的逻辑绝然不同, 它把代码转译为数学公式, 随后借助定理证明器证实这些公式于所有情形下均能成立。

例如, 有一个DeFi借贷协议, 传统的测试也许仅仅检查了常规的借贷流程, 然而形式化验证却会去检查所有有可能出现的极端情形, 像是用户进行闪电贷后立刻还款, 清算价格恰好卡在边界位置, 多个用户同时开展操作等。这些边界条件, 通过手动测试是很难将其全部覆盖上的。

曾有团队针对一个看上去测试覆盖率达百分之百的合约开展形式化验证, 最终发觉了一个唯有在特定时间戳、特定交易顺序之际方可触发的漏洞, 这般的漏洞, 常规测试即便运行一万次都不见得能够碰到。

区块链项目如何低成本引入形式化验证

好多团队只要一听到“形式化验证”, 就会觉得其有着较高的门槛以及较大的成本。的确如此, 在早期的时候, 这一事物是需要专业的数学人才的, 然而如今情况已然发生了变化。在市面上, 出现了不少已然成熟的工具, 像Certora、VerX、KEVM等这类工具, 它们已经将形式化验证的门槛降低到了“能够写出基础数学表达式”这样的程度。

刚起步的小规模团队能从具有关键意义的模块着手开展工作, 没必要非得追求全面覆盖。举例来说, 像是先将资金池范畴内的存款取款相关逻辑, 以及治理投票环节的计数选票方面的逻辑, 还有跨链桥的检验证实逻辑等这些存在较高风险的模块来展开符合规定格式及要求的验证工作。有一种较为典型的实施办法是: 首先撰写传统风格的测试以确保基本功能处于正常状态, 接着针对核心合约开展符合规定格式及要求的验证工作以此保证不存在任何漏洞。

于成本这一方面, 当下存在着不少以开源之形式呈现的形式化验证库, 像Solidity的SMTChecker, 它直接被集成至编译器当中。仅需零成本便能够加以使用。团队可以率先从这些免费的工具展开使用, 进而逐步积累经验。

由区块链行业的天性所决定, 它对于安全性有着极高的要求。形式化验证并非是无所不能的, 然而它能够波及测试所覆盖不到的那些死角区域。相对理性的一种做法是, 以传统测试作为基础支撑, 再运用形式化验证来填补漏洞之处, 只有将这两者配合起来加以使用, 才能够把风险降低到最低限度。