形式验证

智能合约使得创建去中心化、去信任和强大的应用程序成为可能，这些应用程序可以引入新的用例并为用户释放价值。

由于智能合约处理大量价值，因此安全性是开发人员的关键考虑因素。

形式验证是提高智能合约安全性的推荐技术之一。

形式验证使用形式化方法来指定、设计和验证程序，多年来一直用于确保关键硬件和软件系统的正确性。

在智能合约中实现时，形式验证可以证明合约的业务逻辑符合预定义的规范。

与其他评估合约代码正确性的方法（例如测试）相比，形式验证更能保证智能合约在功能上是正确的。

什么是形式验证？

形式验证是指评估系统相对于形式规范的正确性的过程。

简单来说，形式验证允许我们检查系统的行为是否满足某些要求（即，它是否满足我们的要求）。

系统的预期行为（在这种情况下是智能合约）使用形式建模来描述，而规范语言可以创建形式属性。

然后，形式验证技术可以验证合同的实施是否符合其规范，并得出前者正确性的数学证明。

当合同满足其规范时，它被描述为“功能正确”、“设计正确”或“构造正确”。

什么是正式模型？

在计算机科学中，形式模型是对计算过程的数学描述。程序被抽象为数学函数（方程），模型描述了在给定输入的情况下如何计算函数的输出。

形式模型提供了一个抽象级别，在该抽象级别上可以评估对程序行为的分析。形式模型的存在允许创建形式规范，该规范描述了所讨论模型的所需属性。

不同的技术用于对智能合约进行建模以进行形式验证。例如，一些模型用于推理智能合约的高级行为。这些建模技术将黑盒视图应用于智能合约，将它们视为接受输入并基于这些输入执行计算的系统。

高级模型侧重于智能合约与外部代理之间的关系，例如外部拥有账户（EOA）、合约账户和区块链环境。此类模型对于定义指定合同应如何响应某些用户交互的属性非常有用。

相反，其他正式模型关注智能合约的低级行为。

虽然高级模型可以帮助推理合约的功能，但它们可能无法捕获有关实现内部工作的详细信息。

低级模型将白盒视图应用于程序分析，并依靠智能合约应用程序的低级表示（例如程序跟踪和控制流图）来推理与合约执行相关的属性。

低级模型被认为是理想的，因为它们代表了智能合约在以太坊执行环境（即 EVM）中的实际执行。

低级建模技术在建立智能合约中的关键安全属性和检测潜在漏洞方面特别有用。

什么是正式规范？

规范只是特定系统必须满足的技术要求。在编程中，规范代表关于程序执行的一般想法（即程序应该做什么）。

在智能合约的上下文中，正式规范是指属性——对合约必须满足的要求的正式描述。

这些属性被描述为“不变量”，代表关于合约执行的逻辑断言，在所有可能的情况下都必须保持正确，没有任何例外。

因此，我们可以将正式规范视为用正式语言编写的描述智能合约预期执行的语句的集合。

规范涵盖了合同的属性，并定义了合同在不同情况下的行为方式。形式验证的目的是确定智能合约是否拥有这些属性（不变量），并且这些属性在执行期间没有被违反。

正式规范对于开发智能合约的安全实施至关重要。

未能实现不变量或在执行期间违反其属性的合约容易出现可能损害功能或导致恶意攻击的漏洞。

智能合约的正式规范类型

形式化规范可以对程序执行的正确性进行数学推理。

与正式模型一样，正式规范可以捕获合同实现的高级属性或低级行为。

形式规范是使用程序逻辑的元素导出的，它允许对程序的属性进行形式推理。

程序逻辑具有表达（用数学语言）程序预期行为的形式规则。

各种程序逻辑用于创建形式规范，包括可达性逻辑、时间逻辑和霍尔逻辑。

智能合约的正式规范可以大致分为高级规范或低级规范。

无论规范属于哪个类别，它都必须充分且明确地描述被分析系统的属性。

高级规格

顾名思义，高级规范（也称为“面向模型的规范”）描述了程序的高级行为。高级规范将智能合约建模为有限状态机 (FSM)，它可以通过执行操作在状态之间转换，时间逻辑用于定义 FSM 模型的形式属性。

时序逻辑是“对时间限定的命题进行推理的规则（例如，“我总是饿”或“我最终会饿”）。当应用于形式验证时，时间逻辑用于声明关于被建模为状态机的系统的正确行为的断言。具体来说，时间逻辑描述了智能合约可能处于的未来状态以及它如何在状态之间转换。

高级规范通常捕获智能合约的两个关键时间属性：安全性和活性。安全属性代表“没有什么不好的事情发生”的想法，通常表示不变性。安全属性可以定义一般软件要求，例如免于死锁，或表达合同的特定领域属性（例如，函数访问控制的不变量、状态变量的可接受值或令牌传输的条件）。

以这个安全要求为例，它涵盖了在 ERC-20 代币合约中使用 transfer() 或 transferFrom() 的条件：“发送者的余额永远不会低于请求发送的代币数量。”。这种对契约不变量的自然语言描述可以被翻译成正式的（数学）规范，然后可以严格检查其有效性。

活跃性属性断言“最终会发生好事”并关注合约在不同状态下进展的能力。活性属性的一个例子是“流动性”，它指的是合约根据请求将其余额转移给用户的能力。如果违反此属性，用户将无法提取存储在合约中的资产，就像 Parity 钱包事件发生的那样。

低级规范

高级规范以合同的有限状态模型为起点，并定义该模型的所需属性。

相比之下，低级规范（也称为“面向属性的规范”）通常将程序（智能合约）建模为包含数学函数集合的系统，并描述此类系统的正确行为。

简而言之，低级规范分析程序跟踪并尝试在这些跟踪上定义智能合约的属性。

跟踪是指改变智能合约状态的函数执行序列； 因此，低级规范有助于指定合同内部执行的要求。

低级形式规范可以作为 Hoare 风格的属性或执行路径上的不变量给出。

霍尔式属性 Hoare-style properties

Hoare Logic 提供了一套用于推理程序正确性的正式规则，包括智能合约。

Hoare 风格的属性由 Hoare 三元组 {P}c{Q} 表示，其中 c 是程序，P 和 Q 是关于 c 的状态（即程序）的谓词，正式描述为前置条件和后置条件，分别。

前置条件是描述正确执行函数所需条件的谓词；调用合约的用户必须满足这个要求。后置条件是一个谓词，描述了一个函数在正确执行时所建立的条件；调用函数后，用户可以预期此条件为真。 Hoare 逻辑中的不变量是通过执行函数保留的谓词（即，它不会改变）。

霍尔式规范可以保证部分正确或完全正确。如果在函数执行之前前提条件成立，则合约函数的实现是“部分正确的”，并且如果执行终止，则后置条件也成立。如果在函数执行之前先决条件为真，则获得完全正确性的证明，保证执行终止，并且当它终止时，后置条件成立。

获得完全正确性的证明是困难的，因为某些执行可能会在终止之前延迟，或者根本不会终止。也就是说，执行是否终止的问题可以说是一个有争议的问题，因为以太坊的气体机制可以防止无限的程序循环（执行成功终止或由于“气体不足”错误而结束）。

使用 Hoare 逻辑创建的智能合约规范将具有为合约中函数和循环的执行定义的前置条件、后置条件和不变量。前置条件通常包括错误输入函数的可能性，后置条件描述对此类输入的预期响应（例如，抛出特定异常）。以这种方式，Hoare 风格的属性对于确保合约实现的正确性是有效的。

许多形式验证框架使用 Hoare 风格的规范来证明函数的语义正确性。也可以使用 Solidity 中的 require 和 assert 语句直接将 Hoare 风格的属性（作为断言）添加到合约代码中。

require 语句表示前置条件或不变量，通常用于验证用户输入，而 assert 捕获安全所需的后置条件。

例如，可以使用 require 作为对调用帐户身份的先决条件检查来实现对功能（安全属性的示例）的适当访问控制。

类似地，合约中状态变量允许值的不变量（例如，流通中的代币总数）可以通过在函数执行后使用 assert 来确认合约状态来防止违规

跟踪级属性

基于跟踪的规范描述了在不同状态之间转换合同的操作以及这些操作之间的关系。如前所述，跟踪是以特定方式改变合约状态的操作序列。

这种方法依赖于智能合约模型作为具有一些预定义状态（由状态变量描述）以及一组预定义转换（由合约函数描述）的状态转换系统。此外，控制流图（CFG）是程序执行流程的图形表示，通常用于描述合约的操作语义。在这里，每个跟踪都表示为控制流图上的一条路径。

首先，跟踪级规范用于推理智能合约中的内部执行模式。通过创建跟踪级规范，我们为智能合约断言了可接受的执行路径（即状态转换）。使用符号执行等技术，我们可以正式验证执行永远不会遵循正式模型中未定义的路径。

让我们使用一个 DAO 合约的示例，该合约具有一些可公开访问的函数来描述跟踪级别的属性。在这里，我们假设 DAO 合约允许用户执行以下操作：

存入资金

存入资金后对提案进行投票

如果他们没有对提案进行投票，则要求退款

示例跟踪级别属性可以是“不存入资金的用户不能对提案投票”或“不对提案投票的用户应该始终能够要求退款”。

这两个属性都断言首选的执行顺序（在存入资金之前不能进行投票，并且在对提案进行投票之后不能要求退款）。

智能合约的正式验证技术

模型检查

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

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

形式验证中的模型检查主要用于评估描述合约随时间变化的行为的时间属性。智能合约的时间属性包括我们之前解释过的安全性和活性。

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

模型检查使用状态空间探索，这涉及构建智能合约的所有可能状态并尝试找到导致财产违规的可达状态。然而，这可能导致无限数量的状态（称为“状态爆炸问题”），因此模型检查器依赖抽象技术来使智能合约的有效分析成为可能。

定理证明

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

定理证明的目的是验证这些陈述之间的逻辑等价性。 “逻辑等价”（也称为“逻辑蕴涵”）是两个陈述之间的一种关系，其中陈述 A 只有当且仅当陈述 B 为真时才为真。

关于合同模型及其属性的陈述之间所需的关系（逻辑等价）被表述为可证明的陈述（称为定理）。使用正式的推理系统，自动定理证明器可以验证定理的有效性。换句话说，定理证明者可以最终证明智能合约的模型与其规范完全匹配。

虽然模型检查模型收缩为具有有限状态的过渡系统，但定理证明可以处理无限状态系统的分析。然而，这意味着自动定理证明器不能总是知道逻辑问题是否“可判定”。

因此，通常需要人工协助来指导定理证明者推导正确性证明。在定理证明中使用人力使其比完全自动化的模型检查更昂贵。

象征性执行

符号执行涉及使用符号输入值而不是具体值执行程序（通常是静态的）。由于符号值可以代表多个具体值，因此可以探索智能合约的多个执行路径，而无需一一遍历。

在形式验证中，符号执行用于推理智能合约的跟踪级属性。如前所述，跟踪是指每当用户触发其代码运行时智能合约所采用的某种执行路径。因此，符号执行的目标是发现违反智能合约属性的执行路径。

符号执行背后的想法是将每个跟踪表示为符号输入值的数学公式，将执行引导到该路径。符号执行引擎（有时称为 SMT 求解器）用于确定特定路径是否可满足。 SMT 求解器还可以与模型检查算法相结合，以提高形式验证的有效性。

如果违反属性断言的路径是可满足的，则 SMT 求解器可用于计算将执行引导至易受攻击的代码路径的具体输入值（称为路径约束）。这使得符号执行对于测试用例的生成很有用。通过使用 SMT 求解器求解路径约束，用户可以导出特定的输入值，这些值可以执行合约的所有有趣行为（这对于单元测试很有用）。

SMT 求解器可以与模型检查算法相结合，以确定智能合约相对于规范的正确性。然而，许多基于符号执行的形式化验证工具大多用于通过静态或动态执行智能合约来检测易受攻击的代码路径。

例如，模糊测试技术依靠符号执行来检测智能合约程序的输入值，这可能导致财产违规。

为什么要对智能合约使用形式验证？

需要可靠性

形式验证用于评估安全关键系统的正确性，这些系统的故障可能会造成毁灭性后果，例如死亡、受伤或财务破产。智能合约是控制巨额价值的高价值应用程序，设计中的简单错误可能给用户带来无法挽回的损失。然而，在部署之前正式验证合同可以增加保证一旦在区块链上运行就会按预期执行。

可靠性是任何智能合约都非常需要的质量，尤其是因为部署在以太坊虚拟机 (EVM) 中的代码通常是不可变的。由于无法轻松获得发布后升级，因此需要保证合同的可靠性，因此需要进行形式验证。形式验证能够检测出棘手的问题，例如整数下溢和溢出、重入和不良气体优化，这些问题可能会被审计员和测试员忽略。

证明功能正确性

程序测试是证明智能合约满足某些要求的最常用方法。这涉及使用预期处理的数据样本执行合同并分析其行为。如果合约返回了样本数据的预期结果，那么开发人员就有了其正确性的客观证据。

但是，这种方法不能证明对不属于样本的输入值的正确执行。因此，测试合约可能有助于检测错误（即，如果某些代码路径在执行期间未能返回所需的结果），但它不能最终证明不存在错误。

相反，形式验证可以正式证明智能合约满足无限范围执行的要求，而根本不需要运行合约。这需要创建一个准确描述正确合约行为的正式规范，并开发合约系统的正式（数学）模型。然后我们可以按照正式的证明程序来检查合约模型和规范之间的一致性。

通过形式验证，验证合约的业务逻辑是否满足要求的问题是一个可以证明或反驳的数学命题。通过形式化证明一个命题，我们可以用有限的步骤验证无限数量的测试用例。以这种方式，形式验证有更好的前景来证明合同在功能上相对于规范是正确的。

理想的验证目标

验证目标描述要正式验证的系统。形式验证最适用于“嵌入式系统”（构成较大系统一部分的小而简单的软件）。它们也是规则很少的专业领域的理想选择，因为这使得修改用于验证特定领域属性的工具变得更加容易。

智能合约——至少在某种程度上——满足了这两个要求。例如，以太坊合约的小规模使其易于进行形式验证。同样，EVM 遵循简单的规则，这使得指定和验证在 EVM 中运行的程序的语义属性更容易

更快的开发周期

形式验证技术，例如模型检查和符号执行，通常比定期分析智能合约代码（在测试或审计期间执行）更有效。

这是因为形式验证依赖于符号值来测试断言（“如果用户尝试提取 n 以太怎么办？”），而测试使用具体值（“如果用户尝试提取 5 以太怎么办？”）。

符号输入变量可以覆盖多类具体值，因此形式验证方法可以在更短的时间内保证更多的代码覆盖率。

如果有效使用，形式验证可以加快开发人员的开发周期。

形式验证还通过减少代价高昂的设计错误来改进构建去中心化应用程序（dapps）的过程。

升级合约（在可能的情况下）以修复漏洞需要大量重写代码库并在开发上花费更多精力。形式验证可以检测合同实施中的许多错误，这些错误可能会绕过测试人员和审计人员，并提供充足的机会在部署合同之前解决这些问题。

正式验证的缺点

体力劳动成本

形式化验证，尤其是人工指导证明者推导正确性证明的半自动验证，需要大量的体力劳动。此外，创建正式规范是一项复杂的活动，需要高水平的技能。

与评估合同正确性的常用方法（例如测试和审计）相比，这些因素（努力和技能）使形式验证更加苛刻和昂贵。尽管如此，考虑到智能合约实施中的错误成本，支付全面验证审计的成本是可行的。

假阴性

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

如果规范写得不好，形式验证审计就无法检测到违反属性（指向易受攻击的执行）。在这种情况下，开发人员可能会错误地认为合约没有错误。

性能问题

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

此外，程序验证者并不总是可能确定是否可以满足属性（描述为逻辑公式）（“可判定性问题”），因为程序可能永远不会终止。因此，即使合同明确规定，也可能无法证明合同的某些属性。

参考资料

https://ethereum.org/zh/developers/docs/smart-contracts/formal-verification/