智能合约的形式化验证
智能合约使创建去中心化、无须信任且稳健的应用程序成为可能，这些应用程序引入了新的用例并为用户解锁了价值。由于智能合约处理大量价值，安全性是开发者需要考虑的关键因素。
形式化验证是提高智能合约安全性的推荐技术之一。形式化验证使用形式化方法 (opens in a new tab)来规范、设计和验证程序，多年来一直用于确保关键硬件和软件系统的正确性。
在智能合约中实施时，形式化验证可以证明合约的业务逻辑符合预定义的规范。与测试等其他评估合约代码正确性的方法相比，形式化验证为智能合约在功能上的正确性提供了更强有力的保证。
什么是形式化验证？
形式化验证是指根据形式化规范评估系统正确性的过程。简而言之，形式化验证允许我们检查系统的行为是否满足某些要求（即它是否执行了我们想要的操作）。
系统（在本例中为智能合约）的预期行为使用形式化建模来描述，而规范语言则支持创建形式化属性。然后，形式化验证技术可以验证合约的实现是否符合其规范，并得出前者正确性的数学证明。当合约满足其规范时，它被称为“功能正确”、“设计正确”或“构造正确”。
什么是形式化模型？
在计算机科学中，形式化模型 (opens in a new tab)是计算过程的数学描述。程序被抽象为数学函数（方程式），模型描述了在给定输入的情况下如何计算函数的输出。
形式化模型提供了一定程度的抽象，在此基础上可以评估对程序行为的分析。形式化模型的存在允许创建_形式化规范_，该规范描述了相关模型的所需属性。
不同的技术用于对智能合约进行建模以进行形式化验证。例如，一些模型用于推理智能合约的高级行为。这些建模技术对智能合约应用黑盒视图，将它们视为接受输入并根据这些输入执行计算的系统。
高级模型侧重于智能合约与外部代理之间的关系，例如外部拥有账户 (EOA)、合约账户和区块链环境。此类模型可用于定义属性，这些属性指定合约在响应某些用户交互时应如何表现。
相反，其他形式化模型侧重于智能合约的低级行为。虽然高级模型可以帮助推理合约的功能，但它们可能无法捕获有关实现内部工作原理的详细信息。低级模型将白盒视图应用于程序分析，并依赖于智能合约应用程序的较低级别表示（例如程序跟踪和控制流图 (opens in a new tab)）来推理与合约执行相关的属性。
低级模型被认为是理想的，因为它们代表了智能合约在以太坊执行环境（即 EVM）中的实际执行。低级建模技术在建立智能合约的关键安全属性和检测潜在漏洞方面特别有用。
什么是形式化规范？
规范仅仅是特定系统必须满足的技术要求。在编程中，规范代表了关于程序执行的一般概念（即程序应该做什么）。
在智能合约的背景下，形式化规范是指_属性_——对合约必须满足的要求的形式化描述。此类属性被描述为“不变量”，代表关于合约执行的逻辑断言，这些断言在任何可能的情况下都必须保持为真，没有任何例外。
因此，我们可以将形式化规范视为用形式化语言编写的语句集合，这些语句描述了智能合约的预期执行。规范涵盖了合约的属性，并定义了合约在不同情况下的行为方式。形式化验证的目的是确定智能合约是否具备这些属性（不变量），并且这些属性在执行期间不会被违反。
形式化规范在开发安全的智能合约实现中至关重要。未能实现不变量或在执行期间其属性被违反的合约很容易出现漏洞，这些漏洞可能会损害功能或导致恶意利用。
智能合约形式化规范的类型
形式化规范支持对程序执行正确性进行数学推理。与形式化模型一样，形式化规范可以捕获高级属性或合约实现的低级行为。
形式化规范是使用程序逻辑 (opens in a new tab)的元素推导出来的，这允许对程序的属性进行形式化推理。程序逻辑具有形式化规则，这些规则（用数学语言）表达了程序的预期行为。各种程序逻辑用于创建形式化规范，包括可达性逻辑 (opens in a new tab)、时序逻辑 (opens in a new tab)和霍尔逻辑 (Hoare logic) (opens in a new tab)。
智能合约的形式化规范可以大致分为高级或低级规范。无论规范属于哪个类别，它都必须充分且明确地描述所分析系统的属性。
高级规范
顾名思义，高级规范（也称为“面向模型的规范”）描述了程序的高级行为。高级规范将智能合约建模为有限状态机 (opens in a new tab) (FSM)，它可以通过执行操作在状态之间转换，并使用时序逻辑为 FSM 模型定义形式化属性。
时序逻辑 (opens in a new tab)是“用于推理在时间上受限的命题的规则（例如，‘我_总是_很饿’或‘我_最终_会饿’）”。当应用于形式化验证时，时序逻辑用于陈述关于建模为状态机的系统正确行为的断言。具体来说，时序逻辑描述了智能合约未来可能处于的状态以及它如何在状态之间转换。
高级规范通常捕获智能合约的两个关键时序属性：安全性和活性。安全属性代表“永远不会发生坏事”的理念，通常表达不变性。安全属性可以定义一般的软件要求，例如没有死锁 (opens in a new tab)，或者表达合约的特定领域属性（例如，函数访问控制的不变量、状态变量的允许值或代币转账的条件）。
以涵盖在 ERC-20 代币合约中使用 transfer() 或 transferFrom() 条件的安全要求为例：“发送者的余额永远不会低于请求发送的代币数量。”。这种对合约不变量的自然语言描述可以转化为形式化（数学）规范，然后可以对其有效性进行严格检查。
活性属性断言“最终会发生好事”，并涉及合约在不同状态之间取得进展的能力。活性属性的一个例子是“流动性”，它是指合约根据请求将其余额转账给用户的能力。如果违反了此属性，用户将无法提取存储在合约中的资产，就像 Parity 钱包事件 (opens in a new tab)中发生的那样。
低级规范
高级规范以合约的有限状态模型为起点，并定义该模型的所需属性。相比之下，低级规范（也称为“面向属性的规范”）通常将程序（智能合约）建模为包含数学函数集合的系统，并描述此类系统的正确行为。
简而言之，低级规范分析_程序跟踪_，并尝试在这些跟踪上定义智能合约的属性。跟踪是指改变智能合约状态的函数执行序列；因此，低级规范有助于指定合约内部执行的要求。
低级形式化规范可以作为霍尔风格 (Hoare-style) 属性或执行路径上的不变量给出。
霍尔风格属性
霍尔逻辑 (opens in a new tab)提供了一组用于推理程序（包括智能合约）正确性的形式化规则。霍尔风格属性由霍尔三元组 {P}c{Q} 表示，其中 c 是程序，P 和 Q 是关于 c（即程序）状态的谓词，分别被形式化地描述为_前置条件_和_后置条件_。
前置条件是描述函数正确执行所需条件的谓词；调用合约的用户必须满足此要求。后置条件是描述函数如果正确执行所建立的条件的谓词；用户可以期望在调用函数后此条件为真。霍尔逻辑中的_不变量_是通过执行函数而保留（即不改变）的谓词。
霍尔风格规范可以保证_部分正确性_或_完全正确性_。如果在执行函数之前前置条件为真，并且如果执行终止，后置条件也为真，则合约函数的实现是“部分正确”的。如果在函数执行之前前置条件为真，保证执行终止，并且当它终止时，后置条件为真，则获得完全正确性的证明。
获得完全正确性的证明很困难，因为某些执行可能会在终止之前延迟，或者根本不终止。话虽如此，执行是否终止的问题可以说是一个没有实际意义的问题，因为以太坊的 Gas 机制可以防止无限的程序循环（执行要么成功终止，要么由于“Gas 耗尽”错误而结束）。
使用霍尔逻辑创建的智能合约规范将为合约中函数和循环的执行定义前置条件、后置条件和不变量。前置条件通常包括函数输入错误的可能性，后置条件描述对这些输入的预期响应（例如，抛出特定异常）。通过这种方式，霍尔风格属性可有效确保合约实现的正确性。
许多形式化验证框架使用霍尔风格规范来证明函数的语义正确性。也可以通过在 Solidity 中使用 require 和 assert 语句，将霍尔风格属性（作为断言）直接添加到合约代码中。
require 语句表达前置条件或不变量，通常用于验证用户输入，而 assert 捕获安全所需的后置条件。例如，可以使用 require 作为对调用账户身份的前置条件检查，来实现对函数的适当访问控制（安全属性的一个例子）。类似地，通过使用 assert 在函数执行后确认合约的状态，可以保护合约中状态变量的允许值（例如，流通中的代币总数）的不变量不被违反。
跟踪级属性
基于跟踪的规范描述了在不同状态之间转换合约的操作以及这些操作之间的关系。如前所述，跟踪是以特定方式改变合约状态的操作序列。
这种方法依赖于将智能合约建模为状态转换系统，该系统具有一些预定义状态（由状态变量描述）以及一组预定义转换（由合约函数描述）。此外，控制流图 (opens in a new tab) (CFG) 是程序执行流的图形表示，通常用于描述合约的操作语义。在这里，每个跟踪都表示为控制流图上的一条路径。
主要地，跟踪级规范用于推理智能合约中内部执行的模式。通过创建跟踪级规范，我们断言智能合约的允许执行路径（即状态转换）。使用符号执行等技术，我们可以形式化地验证执行永远不会遵循形式化模型中未定义的路径。
让我们使用一个具有一些可公开访问函数的去中心化自治组织 (DAO) 合约的示例来描述跟踪级属性。在这里，我们假设 DAO 合约允许用户执行以下操作：
-
存入资金
-
存入资金后对提案进行投票
-
如果他们不对提案进行投票，则申领退款
跟踪级属性的示例可以是_“未存入资金的用户不能对提案进行投票”或“未对提案进行投票的用户应始终能够申领退款”_。这两个属性都断言了首选的执行顺序（投票不能在存入资金_之前_发生，申领退款不能在对提案进行投票_之后_发生）。
智能合约形式化验证技术
模型检查
模型检查是一种形式化验证技术，其中算法根据其规范检查智能合约的形式化模型。在模型检查中，智能合约通常表示为状态转换系统，而允许的合约状态的属性则使用时序逻辑定义。
模型检查需要创建系统（即合约）的抽象数学表示，并使用植根于命题逻辑 (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 的值。
因为符号执行依赖于程序的输入，并且探索所有可达状态的输入集可能是无限的，所以它仍然是一种测试形式。然而，如示例所示，在寻找触发属性违规的输入方面，符号执行比常规测试更有效。
此外，与其他随机生成函数输入的基于属性的技术（例如模糊测试）相比，符号执行产生的误报更少。如果在符号执行期间触发了错误状态，则可以生成触发错误的具体值并重现该问题。
符号执行还可以提供一定程度的正确性数学证明。考虑以下具有溢出保护的合约函数示例：
function safe_add(uint x, uint y) returns(uint z){
z = x + y;
require(z>=x);
require(z>=y);
return z;
}
导致整数溢出的执行跟踪需要满足公式：z = x + y AND (z >= x) AND (z >= y) AND (z < x OR z < y) 这样的公式不太可能被求解，因此它作为数学证明，证明函数 safe_add 永远不会溢出。
为什么对智能合约使用形式化验证？
对可靠性的需求
形式化验证用于评估安全关键系统的正确性，这些系统的故障可能会产生毁灭性的后果，例如死亡、受伤或财务破产。智能合约是控制巨大价值的高价值应用程序，设计中的简单错误可能会导致用户遭受不可挽回的损失 (opens in a new tab)。然而，在部署之前对合约进行形式化验证，可以增加其在区块链上运行后按预期执行的保证。
可靠性是任何智能合约中都非常需要的品质，特别是因为部署在以太坊虚拟机 (EVM) 中的代码通常是不可变的。由于发布后的升级不容易实现，保证合约可靠性的需求使得形式化验证成为必要。形式化验证能够检测出棘手的问题，例如整数下溢和溢出、重入以及糟糕的 Gas 优化，这些问题可能会逃过审计员和测试员的眼睛。
证明功能正确性
程序测试是证明智能合约满足某些要求的最常见方法。这涉及使用预期处理的数据样本执行合约并分析其行为。如果合约返回样本数据的预期结果，那么开发者就有了其正确性的客观证明。
然而，这种方法无法证明不属于样本的输入值的正确执行。因此，测试合约可能有助于检测错误（即，如果某些代码路径在执行期间未能返回所需结果），但它不能最终证明没有错误。
相反，形式化验证可以形式化地证明智能合约满足无限范围执行的要求，而_完全不需要_运行合约。这需要创建一个精确描述正确合约行为的形式化规范，并开发合约系统的形式化（数学）模型。然后我们可以遵循形式化证明程序来检查合约模型与其规范之间的一致性。
通过形式化验证，验证合约的业务逻辑是否满足要求的问题是一个可以被证明或证伪的数学命题。通过形式化地证明一个命题，我们可以用有限的步骤验证无限数量的测试用例。通过这种方式，形式化验证在证明合约在功能上符合规范方面具有更好的前景。
理想的验证目标
验证目标描述了要进行形式化验证的系统。形式化验证最适合用于“嵌入式系统”（构成更大系统一部分的小型、简单的软件）。它们也是规则很少的专业领域的理想选择，因为这使得修改用于验证特定领域属性的工具变得更加容易。
智能合约——至少在某种程度上——满足了这两个要求。例如，以太坊合约体积小，使其易于进行形式化验证。类似地，EVM 遵循简单的规则，这使得为在 EVM 中运行的程序指定和验证语义属性变得更加容易。
更快的开发周期
形式化验证技术（例如模型检查和符号执行）通常比对智能合约代码的常规分析（在测试或审计期间执行）更有效。这是因为形式化验证依赖于符号值来测试断言（“如果用户尝试提取 n 个以太币会怎样？”），这与使用具体值（“如果用户尝试提取 5 个以太币会怎样？”）的测试不同。
符号输入变量可以涵盖多类具体值，因此形式化验证方法有望在更短的时间内提供更多的代码覆盖率。如果有效使用，形式化验证可以加速开发者的开发周期。
形式化验证还通过减少代价高昂的设计错误来改进构建去中心化应用 (dapp) 的过程。升级合约（在可能的情况下）以修复漏洞需要大量重写代码库并在开发上花费更多精力。形式化验证可以检测出合约实现中许多可能逃过测试员和审计员眼睛的错误，并提供了在部署合约之前修复这些问题的充足机会。
形式化验证的缺点
人工成本
形式化验证，特别是半自动化验证（其中人工指导证明者得出正确性证明），需要大量的人工劳动。此外，创建形式化规范是一项复杂的活动，需要高水平的技能。
与评估合约正确性的常用方法（例如测试和审计）相比，这些因素（精力和技能）使得形式化验证要求更高且更昂贵。尽管如此，考虑到智能合约实现中错误的代价，为全面验证审计支付成本是切合实际的。
假阴性（漏报）
形式化验证只能检查智能合约的执行是否与形式化规范相匹配。因此，确保规范正确描述智能合约的预期行为非常重要。
如果规范编写得很差，形式化验证审计就无法检测到属性违规（这指向易受攻击的执行）。在这种情况下，开发者可能会错误地认为合约没有错误。
性能问题
形式化验证会遇到许多性能问题。例如，在模型检查和符号检查期间分别遇到的状态和路径爆炸问题可能会影响验证程序。此外，形式化验证工具通常在其底层使用 SMT 求解器和其他约束求解器，而这些求解器依赖于计算密集型程序。
此外，程序验证器并不总是能够确定属性（描述为逻辑公式）是否可以被满足（“可判定性问题 (opens in a new tab)”），因为程序可能永远不会终止。因此，即使合约规范良好，也可能无法证明其某些属性。
以太坊智能合约的形式化验证工具
用于创建形式化规范的规范语言
Act：Act 允许规范存储更新、前置/后置条件和合约不变量。其工具套件还具有证明后端，能够通过 Coq、SMT 求解器或 hevm 证明许多属性。
Scribble - Scribble 将 Scribble 规范语言中的代码注释转换为检查规范的具体断言。
Dafny - Dafny 是一种支持验证的编程语言，它依赖于高级注释来推理和证明代码的正确性。
用于检查正确性的程序验证器
Certora Prover - Certora Prover 是一种自动形式化验证工具，用于检查智能合约中的代码正确性。规范使用 CVL（Certora 验证语言）编写，并结合静态分析和约束求解来检测属性违规。
Solidity SMTChecker - Solidity 的 SMTChecker 是一个基于 SMT（可满足性模理论）和 Horn 求解的内置模型检查器。它在编译期间确认合约的源代码是否与规范匹配，并静态检查是否违反了安全属性。
solc-verify - solc-verify 是 Solidity 编译器的扩展版本，可以使用注释和模块化程序验证对 Solidity 代码执行自动形式化验证。
KEVM - KEVM 是用 K 框架编写的以太坊虚拟机 (EVM) 的形式化语义。KEVM 是可执行的，并且可以使用可达性逻辑证明某些与属性相关的断言。
用于定理证明的逻辑框架
Isabelle - Isabelle/HOL 是一个证明助手，允许用形式化语言表达数学公式，并提供证明这些公式的工具。主要应用是数学证明的形式化，特别是形式化验证，其中包括证明计算机硬件或软件的正确性以及证明计算机语言和协议的属性。
Rocq - Rocq 是一个交互式定理证明器，可让您使用定理定义程序并交互式地生成机器检查的正确性证明。
基于符号执行的工具，用于检测智能合约中的易受攻击模式
曼蒂科尔 - 一个基于符号执行的 EVM 字节码分析工具。
hevm - hevm 是一个用于 EVM 字节码的符号执行引擎和等价性检查器。
Mythril - 一个用于检测以太坊智能合约漏洞的符号执行工具