什么是智能合约的形式化验证？

2023-11-18 22:41 更新

本文由社区成员发布。作者为David Tarditi，一家Web3智能合约审计公司CertiK的工程副总裁。

摘要

对智能合约进行形式化验证可避免它们出现错误、漏洞和其他不利的情况。在这个过程中，人类专家会将智能合约的逻辑转换为数学语句，然后通过自动化流程对照合约预期行为的模型检查实际逻辑。将形式化验证和人工审计相结合，我们就可以对智能合约的安全性进行全面评估。

简介

智能合约是部署在区块链上的计算机程序，在满足某些条件时会自动运行。智能合约可能非常简单，也可能极其复杂，可以持有价值数百万甚至数十亿美元的资产。

智能合约代码如果有安全漏洞，就可能造成毁灭性后果，比如被不法分子盗窃其持有的所有资产。2021年，由于智能合约中的一个拼写错误，自动做市商(AMM)Uranium Finance被盗取了5,000万美元。

同样在2021年，由于单个代码错误，Compound Finance错误发放了8000万美元的奖励。2022年，因智能合约出现一个错误，Wormhole Bridge被盗走3.2亿美元。

因此，一开始就把智能合约程序弄对很重要。智能合约采用开源模式，这意味着一旦合约部署后，代码就会公开。如果黑客发现其中的错误，就可以立即加以利用。此外，随着时间的推移修补安全漏洞的常规操作派不上用场，因为智能合约的代码在部署后通常无法修改。

智能合约的形式化验证是通过将智能合约的逻辑和预期行为呈现为数学语句来实现的。随后，审计师会使用自动化工具检查这些语句是否正确。

该过程涉及：

通过运用数学推理，有助于确保经过形式化验证的智能合约避免出现错误、漏洞和其他不利的情况。验证也有助于增加对合约的信赖和信心，因为其特性已经过了严格检验，正确可靠。

以下这些示例大致说明了智能合约验证如何帮助防止重大财务损失和其他灾难性后果。

Uniswap是一家著名的AMM。Uniswap V1智能合约在开发过程中，进行了形式化验证。在发布前，这项形式化验证发现并修复了一些舍入误差，避免了Uniswap V1的资金被吸干殆尽。

Balancer V2也是一个经过验证的AMM。形式化验证发现并修复了智能合约中闪电贷款功能的费用计算错误，该错误会使交易平台很容易遭受盗窃。

SafeMoon V1在部署后，通过形式化验证发现了一个极其微小的错误，如果该错误没被发现，合约所有人如果在放弃所有权之前进行了某些操作，那合约所有人在放弃之后有可能重新获得该合约。

大多数对SafeMoon V1分叉的人工审计都遗漏了这个错误，因为需要分析程序变量值的特定组合才能发现这个错误。人类很容易错过这个问题，但机器却能及时地捕捉到它。

形式化验证提供了一种系统化、自动化的办法，来根据合约的预期特性检查合约的逻辑和行为。这样可以更轻松地识别和修复任何潜在的错误或漏洞。这对于人工检查难以发现的复杂、细微的问题特别有用。

人工审计则包括专家对合约的代码、设计和部署进行审查。审计师会利用自己的经验和专业知识，来识别安全风险并评估合约的整体安全状况。他们还可以确认形式化验证过程是否正确执行，并检查是否存在自动化工具可能无法检测到的任何问题。

将形式化验证和人工审计相结合，我们就可以对智能合约的安全性进行全面评估。这可以提高发现和修复任何漏洞的几率。这样一来，我们就相当于采用了一种结合人类和机器各自专长的深度防御安全措施。

为了确保智能合约的安全性，必须将形式化验证和人工审计相结合，从而确保对智能合约的安全态势进行全面而彻底的评估。

虽然形式化验证对资源消耗较高，但对于具有高价值或高风险因素的合约来说，这是一项值得的投资。毕竟归根结底，安全重于泰山，一定要优先考虑安全性并确保智能合约远离错误、漏洞和不利的意外行为。