形式化验证：让智能合约更安全

形式化验证是增强智能合约安全性的推荐技术之一，在这个过程中，人类专家会将智能合约的逻辑转换为数学语句，然后通过自动化流程对照合约预期行为的模型检查实际逻辑。将形式化验证和人工审计相结合，可以对智能合约的安全性进行全面评估。

什么是智能合约

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

智能合约代码如果有安全漏洞，就可能造成毁灭性后果，比如被不法分子盗窃其持有的所有资产，比如2022年，因智能合约出现一个错误，Wormhole Bridge被盗走3.2亿美元。

因此，一开始就把智能合约程序弄对很重要。智能合约采用开源模式，这意味着一旦合约部署后，代码就会公开。如果黑客发现其中的错误，就可以立即加以利用。

此外，随着时间的推移修补安全漏洞的常规操作派不上用场，因为智能合约的代码在部署后通常无法修改。

智能合约的形式化验证技术

模型检查

模型检查是一种形式化验证技术，它使用一种算法根据规范检查智能合约的形式化模型。 在模型检查中，智能合约通常表示为状态转换系统，而允许的合约状态的属性使用时间逻辑来定义。

模型检查要求创建系统（即合约）的抽象数学表示并使用根植于命题逻辑（opens in a new tab）的公式表示该系统的属性。这简化了模型检查算法的任务，即证明一个数学模型满足给定的逻辑公式。

形式化验证的模型检查主要用来评估时间属性，后者描述合约在一段时间内的行为。 如前所述，智能合约的时间属性包括安全和活性。

例如，与访问控制有关的安全属性（例如，只有合约的所有者才能调用 selfdestruct）可以用形式化逻辑来编写。此后，模型检查算法能验证合约是否满足此形式化规范。

模型检查使用状态空间探索，其中涉及构造智能合约的所有可能状态以及尝试找到导致违反属性的可达状态。

然而，这可能导致无限多个状态（称为“状态爆炸问题”），因此模型检查器依靠抽象技术来实现智能合约的高效分析。

定理证明

定理证明是一种程序（包括智能合约）正确性的数学推理方法。 它涉及将合约系统的模型以及其规范转换成数学公式（逻辑语句）。

定理证明的目的是验证这些语句之间的逻辑等价性。 “逻辑等价性”（又称为“逻辑双向蕴含”）是指两个语句之间的一种关系类型，即当且仅当语句二为真时，语句一才能为真。

关于合约模型及其属性的语句之间的必要关系（逻辑等价性）被表述为一个可证明的语句（称为定理）。 使用形式化推理系统，自动化定理证明器可以验证该定理的有效性。

也就是说，定理证明器可以确证智能合约模型与其规范完全相符。

模型检查把合约建模成有限状态的转换系统，而定理证明可以处理对无限状态系统的分析。然而，这意味着自动化定理证明器无法总是知道一个逻辑问题是否是“可判定的”。

因此，往往需要人类的帮助来指导定理证明器推导出正确性证明。在定理证明中使用人力，使得它的使用成本明显高于模型检查，模型检查是完全自动化的。

符号执行

符号执行是一种通过使用符号值（例如 x > 5）而不是具体值（例如 x == 5）执行函数来分析智能合约的方法。 作为一种形式化验证技术，符号执行用来形式化推理合约代码中的执行轨迹级属性。

符号执行把执行轨迹表示成针对符号输入值的数学公式，也称为路径谓词。SMT 求解器（opens in a new tab）用来检查路径谓词是否“可满足”（即存在一个满足公式的值）。如果可以满足脆弱路径，SMT 求解器将产生一个具体值，将执行引向该路径。

假设智能合约的函数把 uint 值 （x） 作为输入，并且当 x 大于 5 且小于 10 时回滚。使用正常测试程序寻找一个触发错误的 x 值需要运行数十个测试用例（或者更多），而且不保证能实际找到一个触发错误的输入。

相反，符号执行工具使用符号值来执行函数：X > 5 ∧ X < 10（即，x 大于 5 同时 x 小于 10）。相关的路径谓词 x = X > 5 ∧ X < 10 将提供给 SMT 求解器来求解。

如果一个特定值满足公式 x = X > 5 ∧ X < 10，SMT 求解器将计算它，例如，求解器可能生成 7 作为 x 的值。

因为符号执行依赖于程序的输入，而探索所有可达状态的输入集可能是无限的，所以符号执行仍然是一种测试形式。然而，如例子所示，符号执行在寻找触发违反属性的输入方面比常规测试更高效。

此外，符号执行比其他随机产生函数输入的基于属性的技术（例如模糊处理）产生更少误报。 如果在符号执行时触发了错误状态，那么就可以产生一个触发该错误的具体值并重现该问题。

为什么对智能合约进行形式化验证

可靠性需要

形式化验证用来评估安全至上的系统的正确性，这类系统如果失败，将产生灾难性后果，例如死亡、受伤或者经济损失。

智能合约是具有高价值的应用程序，控制着大量价值，设计上的小错误将导致用户蒙受难以挽回的损失（opens in a new tab）。然而，在部署前形式化验证合约，可以增加一些保障，确保合约在区块链上运行后表现如同预期一样。

可靠性是所有智能合约渴求的一种品质，尤其是因为部署在以太坊虚拟机 （EVM） 上的代码通常是不可更改的。

由于发布后的升级不容易获得，并且合约可靠性是需要保证的，因此形式化验证必不可少。

形式化验证能够发现棘手的问题，例如整数下溢和溢出、重入攻击和糟糕的燃料优化，审计人员和测试人员可能会漏掉这些问题。

证明功能的正确性

程序测试是最常见的证明智能合约满足某些要求的方法。

程序测试使用一些期望合约处理的样本数据来执行合约并分析合约的行为。如果合约根据样本数据返回预期的结果，那么开发者就有了其正确性的客观证明。

然而，这种方法无法证明不在样本里的输入值的正确执行。因此，测试合约可能有助于检测到漏洞（即是否一些代码路径在执行过程中未能返回预期结果），但是它无法确证没有漏洞存在。

相反，形式化验证可以形式化证明智能合约在无限执行范围内满足要求，而无需运行合约。这需要制定精确描述正确合约行为的形式化规范并开发合约系统的形式化（数学）模型。

然后，我们可以按照形式化证明程序来检查合约模型与其规范是否一致。

通过形式化验证，验证合约的业务逻辑是否满足要求的问题就变成一个能被证明或否定的数学命题。通过形式化证明一个命题，可以使用有限的步骤验证无数个测试用例。这种方式使形式化验证有更好的前景，可以证明依据规划合约的功能正确。

理想的验证目标

验证目标描述要进行形式化验证的系统。 形式化验证最好用于“嵌入式系统”（简单的小型软件组成一个大系统）。 形式化验证也非常适合规则很少的专业化领域，因为更容易修改验证领域特有属性的工具。

智能合约至少在某种程度上符合这两项要求。 例如，以太坊合约不大，这让它们更适合形式化验证。 同样，以太坊虚拟机遵循简单规则，指定和验证在以太坊虚拟机中运行的程序的语义属性更简单。

更快的开发周期

形式化验证技术，例如模型检查和符号执行，通常比常规智能合约代码分析（在测试或审计期间执行）更高效。这是因为形式化验证依赖于符号值来测试断言（“如果用户尝试提取 n 个以太币将如何？”），与之不同的是，测试使用具体值（“如果用户尝试提取 5 个以太币将如何？”）。

符号输入变量可以涵盖多个类的具体值，因此形式化验证方法保证在更短的时间能覆盖更多代码。如果有效利用，形式化验证可以加速开发者的开发周期。

形式化验证还可以通过减少代价高昂的设计错误，改进构造去中心化应用程序的过程。通过升级合约（在可能的情况下）来修复漏洞需要大量重写代码库以及更多的开发工作。

形式化验证可以检测到合约实现中许多可能被测试人员和审计人员漏掉的错误，并在部署合约前提供充分的机会来修复这些问题。

智能合约形式化验证示例

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

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

Uniswap

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

Balancer

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

SafeMoon

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

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

形式化验证的缺点

人工成本

形式化验证，尤其是需要人为引导证明器来推导出正确性证明的半自动化验证，需要大量人力。此外，制定形式化规范是一项复杂的活动，需要高水平技能。

这些因素（人力和技能）让形式化验证相比于评估合约正确性的普通方法（如测试和审计），要求更高且和成本更大。

尽管如此，考虑到智能合约实现中出现错误的代价，支付全面验证审计的费用也是很实际的。

漏报

形式化验证只能检查智能合约的执行是否符合形式化规范。因此，确保规范能正确地描述智能合约的预期行为非常重要。

如果规范编写拙劣，形式化验证审计则无法检测到违反属性，导致易受攻击的执行。在这种情况下，开发者可能错误地假定合约没有漏洞。

性能问题

形式化验证会遇到一些性能问题。

例如，在模型检查和符号检查中分别遇到的状态爆炸和路径爆炸问题会影响验证过程。 此外，形式化验证工具通常在底层使用 SMT 求解器和其他约束求解器，这些求解器依赖于计算密集型过程。

而且，程序验证器并不是总能确定一个属性（描述成一个逻辑公式）是否能被满足（“可判定性问题(opens in a new tab)”），因为一个程序也许永远不会终止。

因此，即便合约的规范合理，也可能无法证明合约的一些属性。

形式化验证和人工审计的配合

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

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

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