智能合约是一项重要的技术，它使得创建去中心化、无需信任且稳健的应用成为可能，为用户带来了新的用例并释放了价值。由于智能合约处理大量价值，安全性对开发人员来说至关重要。因此，形式化验证成为提高智能合约安全性的一种推荐技术。
形式化验证采用正式方法来指定、设计和验证程序，多年来一直用于确保关键硬件和软件系统的正确性。当应用于智能合约时，形式化验证可以证明合同的业务逻辑符合预定义的规范。与其他用于评估合同代码正确性的方法（如测试）相比，形式化验证提供更强的保证，确保智能合约在功能上是正确的。
在接下来的章节中，我们将详细介绍形式化验证的各个方面，包括如何建立正式模型、定义正式规范以及使用模型检查、定理证明和符号执行等技术来验证智能合约的正确性。通过深入了解这些技术，读者将能够更好地理解如何应用形式化验证来提高智能合约的安全性。
什么是形式化验证？
形式化验证是指根据形式化规范评估系统正确性的过程。简单来说，形式化验证使我们能够检查系统的行为是否满足某些要求（即它做我们想要的事）。
系统的预期行为（在本例中为智能合约）使用形式化建模来描述，而规范语言则支持创建形式化属性。然后，形式化验证技术可以验证合约的实现是否符合其规范，并推导出前者正确性的数学证明。当合约满足其规范时，它被描述为“功能上正确”、“设计上正确”或“构建上正确”。
什么是正式模型？
在计算机科学中，正式模型（在新标签页中打开）是对计算过程的数学描述。程序被抽象为数学函数（方程），模型描述了给定输入时如何计算函数的输出。
正式模型提供了一个分析程序行为的抽象层次。正式模型的存在允许创建正式规范，它描述了所讨论模型的期望属性。
用于正式验证智能合约的不同技术手段。例如，一些模型用于推理智能合约的高层行为。这些建模技术将智能合约视为黑盒系统，接受输入并基于这些输入执行计算。
高层模型关注智能合约与外部代理的关系，如外部拥有的账户（EOA）、合约账户和区块链环境。这些模型有助于定义指定合约在特定用户交互下应有行为的属性。
相反，其他正式模型专注于智能合约的低层行为。尽管高层模型有助于推理合约的功能，但它们可能无法捕捉到实现的内部工作细节。低层模型将程序分析应用白盒视角，并依赖于智能合约应用的低层表示，如程序轨迹和控制流图（在新标签页中打开），来推理与合约执行相关的属性。
低层模型被认为是理想的，因为它们代表了智能合约在以太坊执行环境（即EVM）中的实际执行。低层建模技术在确立智能合约的关键安全属性和检测潜在漏洞方面特别有用。
什么是正式规范？
规范简单来说就是一个特定系统必须满足的技术要求。在编程中，规范代表了对程序执行的一般概念（即程序应该做什么）。
在智能合约的背景下，正式规范指的是属性——对合约必须满足的要求的正式描述。这些属性被描述为“不变量”，代表了关于合约执行的逻辑断言，在任何可能的情况下都必须保持真实，没有任何例外。
因此，我们可以将正式规范视为用正式语言编写的陈述集合，这些陈述描述了智能合约的预期执行方式。规范涵盖了合约的属性，并定义了合约在不同情况下应如何表现。正式验证的目的是确定一个智能合约是否具有这些属性（不变量），以及在执行过程中这些属性是否没有被违反。
在开发安全的智能合约实现方面，正式规范至关重要。未能实现不变量或在执行过程中违反其属性的合约容易出现漏洞，这可能损害功能或导致恶意利用。
智能合约的正式规范类型
智能合约的形式化规范类型
形式化规范使得可以用数学的方式推理程序执行的正确性。与形式化模型一样，形式化规范可以捕捉合约实现的高级属性或低级行为。
形式化规范是使用程序逻辑的元素推导出来的，这允许对程序的属性进行形式化推理。程序逻辑有形式化的规则，用数学语言表达程序预期的行为。在创建形式化规范时使用了各种程序逻辑，包括可达性逻辑、时态逻辑和霍尔逻辑。
智能合约的形式化规范可以大致分类为高级规范和低级规范。无论规范属于哪个类别，它都必须充分且明确地描述所分析系统的属性。
高级规范
正如其名称所示，高级规范（也称为“模型导向规范”）描述了程序的高级行为。高级规范将智能合约建模为有限状态机
（FSM），通过执行操作在状态之间转换，使用时序逻辑来定义FSM模型的形式属性。
是“关于时间方面的命题推理规则（例如，“我总是饿的”或“我最终会饿”）。”在形式验证中应用时，时序逻辑用于陈述关于以状态机为模型的系统正确行为的断言。具体来说，时序逻辑描述了智能合约可以处于的未来状态以及它如何在状态之间转换。
高级规范通常捕捉智能合约的两个关键时序属性：安全性和活性。安全性属性代表“永远不会发生坏事”的理念，通常表示为不变性。安全性属性可能定义一般软件要求，例如无死锁
，或表达合约的特定领域属性（例如，函数访问控制的不变性、状态变量的可接受值，或代币转移的条件）。
例如，这个涉及ERC-20代币合约中使用transfer()或transferFrom()的安全要求：“发送者的余额永远不会低于要发送的代币数量。”这种自然语言描述的合约不变量可以转换为形式化（数学）规范，然后可以严格检查其有效性。
活性属性主张“最终会发生某些好事”，并涉及合约通过不同状态的进展能力。活性属性的一个例子是“流动性”，指的是合约按要求向用户转移余额的能力。如果违反了这个属性，用户将无法提取存储在合约中的资产，就像发生在Parity钱包事件中的那样
（在新标签页中打开）。
低级规范
高级规范以有限状态模型的合约为起点，定义了这个模型的期望属性。相比之下，低级规范（也称为“属性导向规范”）通常将程序（智能合约）建模为包含一系列数学函数的系统，并描述这些系统的正确行为。
简单来说，低级规范分析程序跟踪，并试图定义智能合约在这些跟踪上的属性。跟踪指的是改变智能合约状态的一系列函数执行序列；因此，低级规范有助于指定合约内部执行的要求。
低级形式规范可以以霍尔属性或执行路径上的不变量来给出。
霍尔式属性
霍尔逻辑（Hoare Logic）为推理程序正确性（包括智能合约）提供了一套正式规则。霍尔式属性用霍尔三元组 {P}c{Q} 表示，其中 c 是一个程序，P 和 Q 是关于 c（即程序）状态的谓词，正式描述为前置条件和后置条件。
前置条件是描述函数正确执行所需条件的谓词；调用合约的用户必须满足这一要求。后置条件是描述如果函数正确执行后所建立的条件的谓词；用户可以期望在调用该函数后这一条件为真。霍尔逻辑中的不变量是指在函数执行中保持不变的谓词（即它不会改变）。
霍尔规范可以保证部分正确性或完全正确性。如果在执行函数之前前置条件成立，并且如果执行终止，后置条件也为真，则合约函数的实现被认为是“部分正确”的。如果在函数执行之前前置条件为真，且执行保证终止，当其终止时，后置条件为真，则可以证明完全正确性。
获得完全正确性的证明是困难的，因为某些执行可能在终止之前延迟，或根本不会终止。尽管如此，执行是否终止的问题可以说是无关紧要的，因为以太坊的 gas 机制防止了无限程序循环（执行要么成功终止，要么因“gas不足”错误而结束）。
使用霍尔逻辑创建的智能合约规范将为合约中的函数和循环的执行定义前置条件、后置条件和不变量。前置条件通常包括对函数的错误输入的可能性，后置条件描述对这些输入的预期响应（例如，抛出特定异常）。通过这种方式，霍尔属性对于确保合约实现的正确性是有效的。
许多形式验证框架使用霍尔式属性来证明函数的语义正确性。也可以通过在 Solidity 中使用 require 和 assert 语句，将霍尔属性（作为断言）直接添加到合约代码中。
require 语句表达前置条件或不变量，通常用于验证用户输入，而 assert 捕捉对安全性必要的后置条件。例如，通过使用 require 作为对调用账户身份的前置条件检查，可以实现函数的适当访问控制（一个安全属性的例子）。类似地，可以通过使用 assert 来确认函数执行后合约的状态，以保护合约中状态变量的允许值不受侵犯（例如，流通中的代币总数）。
追踪级属性
基于追踪的规范描述了使合约在不同状态之间转换的操作及这些操作之间的关系。如前所述，追踪是一系列改变合约状态的操作序列。
这种方法依赖于将智能合约视为带有一些预定义状态（由状态变量描述）的状态转换系统，以及一组预定义转换（由合约函数描述）。此外，控制流程图（CFG），即程序执行流的图形表示，通常用于描述合约的操作语义。在这里，每个追踪都表示为控制流图上的一条路径。
主要地，追踪级规范用于推理智能合约内部执行的模式。通过创建追踪级规范，我们断言智能合约的允许执行路径（即，状态转换）。使用诸如符号执行之类的技术，我们可以正式验证执行永远不会遵循未在正式模型中定义的路径。
让我们用一个DAO合约的例子来描述追踪级属性。这里，我们假设DAO合约允许用户执行以下操作：
存款
存款后对提案进行投票
如果他们不对提案进行投票，则可要求退款
追踪级属性的示例可以是“未存款的用户不能对提案进行投票”或“未对提案进行投票的用户应始终能够要求退款”。这两个属性都断言了首选的执行序列（投票不能在存款之前发生，要求退款不能在对提案进行投票之后发生）。
智能合约的形式验证技术
模型检查
模型检查是一种形式化验证技术，其中算法会检查智能合约的形式化模型是否符合其规范。在模型检查中，智能合约通常被表示为状态转换系统，而允许的合约状态属性则使用时序逻辑来定义。
模型检查需要创建一个系统（即合约）的抽象数学表示，并使用基于命题逻辑的公式来表达此系统的属性。这简化了模型检查算法的任务，即证明数学模型满足给定的逻辑公式。
在形式化验证中，模型检查主要用于评估描述合约随时间行为的时序属性。智能合约的时序属性包括安全性和活性，我们之前已经解释过了。
例如，与访问控制相关的安全属性（例如，只有合约的所有者才能调用 selfdestruct）可以用形式逻辑来编写。之后，模型检查算法可以验证合约是否满足这个形式规范。
模型检查使用状态空间探索，包括构建智能合约的所有可能状态，并尝试找到导致属性违规的可达状态。然而，这可能导致无限数量的状态（称为“状态爆炸问题”），因此模型检查器依赖于抽象技术，以使对智能合约的有效分析成为可能。
定理证明
定理证明是一种用于数学上推理程序正确性的方法，包括智能合约。它涉及将合约系统的模型及其规格转换成数学公式（逻辑语句）。
定理证明的目的是验证这些语句之间的逻辑等价性。所谓的“逻辑等价性”（也称为“逻辑双条件”）是指两个语句之间的一种关系，使得第一个语句真实仅当且仅当第二个语句真实。
关于合约模型及其属性的所需关系（逻辑等价性）被形式化为一个可证明的语句（称为定理）。通过使用一个正式的推理系统，自动定理证明器可以验证定理的有效性。换句话说，定理证明器可以确凿地证明智能合约的模型与其规格完全匹配。
尽管模型检查将合约建模为具有有限状态的转换系统，但定理证明可以处理无限状态系统的分析。然而，这意味着自动定理证明器并不总是知道逻辑问题是否“可判定”。
因此，通常需要人为协助来引导定理证明器推导出正确性证明。定理证明中使用人力使其比全自动的模型检查更昂贵。
符号执行
符号执行是一种通过使用符号值（例如，x > 5）而不是具体值（例如，x == 5）执行函数来分析智能合约的方法。作为一种形式验证技术，符号执行用于形式化地推理合约代码中的跟踪级属性。
符号执行将执行跟踪表示为对符号输入值的数学公式，也称为路径谓词。SMT解算器用于检查路径谓词是否“可满足”（即存在可以满足公式的值）。如果一个脆弱路径是可满足的，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 的值。
因为符号执行依赖于程序的输入，而探索所有可达状态的输入集可能是无限的，它仍然是一种测试形式。然而，正如示例所示，符号执行比常规测试更有效地找到触发属性违规的输入。
此外，与其他基于属性的技术（例如，随机生成函数输入的模糊测试）相比，符号执行产生的误报更少。如果在符号执行期间触发了错误状态，那么可以生成一个触发错误的具体值并重现问题。
符号执行还可以提供某种程度的正确性数学证明。考虑以下具有溢出保护的合约函数示例：
导致整数溢出的执行跟踪需要满足以下公式：z = x + y 且 (z >= x) 且 (z>=y) 且 (z < x 或 z < y) 这样的公式不太可能被解出，因此它作为 safe_add 函数永不溢出的数学证明。
为什么对智能合约使用形式化验证？
对于可靠性的需求
形式化验证用于评估安全关键系统的正确性，这些系统的失败可能会导致灾难性后果，如死亡、受伤或财务崩溃。智能合约是控制巨大价值的高价值应用程序，设计中的简单错误可能会给用户造成不可挽回的损失。
然而，在部署之前对合约进行形式化验证，可以增加它在区块链上运行时表现如预期的保证。
可靠性是任何智能合约中非常渴望的质量，特别是因为在以太坊虚拟机（EVM）中的代码通常是不可变的。由于发布后升级不易实现，因此保证合同可靠性的需要使得形式验证成为必要。形式验证能够检测棘手的问题，例如整数下溢和溢出、可重入以及较差的 Gas 优化，这些问题可能会被审计员和测试人员忽略。
证明功能正确性
程序测试是证明智能合约满足某些要求的最常见方法。这涉及使用预期处理的数据样本执行合约并分析其行为。如果合约返回样本数据的预期结果，那么开发人员就可以客观地证明其正确性。
但是，此方法无法证明对于不属于样本的输入值的正确执行。因此，测试合约可能有助于检测错误（即，如果某些代码路径在执行过程中未能返回所需的结果），但它不能最终证明不存在错误。
相反，形式验证可以正式证明智能合约满足无限范围的执行要求，而无需运行合约。这需要创建一个精确描述正确合约行为的正式规范，并开发合约系统的正式（数学）模型。然后我们可以遵循正式的证明程序来检查合同模型与其规范之间的一致性。
通过形式化验证，验证合约的业务逻辑是否满足要求的问题是一个可以证明或反驳的数学命题。通过形式化地证明一个命题，我们可以用有限的步骤验证无限数量的测试用例。通过这种方式，形式验证更有可能证明合同在功能上相对于规范是正确的。
理想的验证目标
验证目标描述了要形式化验证的系统。形式验证最适合用于“嵌入式系统”（构成较大系统一部分的小型、简单的软件）。它们也非常适合规则很少的专门领域，因为这使得修改用于验证特定领域属性的工具变得更加容易。
智能合约——至少在某种程度上——满足了这两个要求。例如，以太坊合约的小规模使其易于接受形式验证。同样，EVM 遵循简单的规则，这使得指定和验证 EVM 中运行的程序的语义属性变得更加容易。
更快的开发周期
形式验证技术，例如模型检查和符号执行，通常比智能合约代码的常规分析（在测试或审计期间执行）更有效。这是因为形式验证依赖于符号值来测试断言（“如果用户尝试提取 n 以太怎么办？”），这与使用具体值的测试（“如果用户尝试提取 5 以太怎么办？”）不同。
符号输入变量可以覆盖多个类别的具体值，因此形式验证方法可以在更短的时间内覆盖更多的代码。如果有效使用，形式验证可以加快开发人员的开发周期。
形式验证还可以通过减少代价高昂的设计错误来改进构建去中心化应用程序（dapp）的过程。升级合约（如果可能）以修复漏洞需要大量重写代码库并在开发上投入更多精力。形式验证可以检测合同实施中的许多错误，这些错误可能会被测试人员和审计人员忽略，并提供充足的机会在部署合同之前解决这些问题。
形式验证的缺点
体力劳动成本
形式验证，尤其是由人类引导证明者得出正确性证明的半自动验证，需要大量的体力劳动。此外，创建正式规范是一项复杂的活动，需要高水平的技能。
与评估合同正确性的常用方法（例如测试和审计）相比，这些因素（努力和技能）使得形式验证要求更高、成本更高。尽管如此，考虑到智能合约实施中错误的成本，支付全面验证审计的费用是可行的。
漏报
形式化验证只能检查智能合约的执行是否符合形式化规范。因此，确保规范正确描述智能合约的预期行为非常重要。
如果规范写得不好，那么正式的验证审计就无法检测到违反属性的行为（这表明执行过程中存在漏洞）。在这种情况下，开发人员可能会错误地认为合约没有错误。
性能问题
形式验证会遇到许多性能问题。例如，在模型检查和符号检查期间分别遇到的状态和路径爆炸问题可能会影响验证过程。此外，形式验证工具通常在其底层使用 SMT 求解器和其他约束求解器，并且这些求解器依赖于计算密集型过程。
此外，程序验证者并不总是能够确定某个属性（描述为逻辑公式）是否可以满足（“可判定性问题”）因为程序可能永远不会终止。因此，即使合约明确指定，也可能无法证明合约的某些属性。
以太坊智能合约的形式化验证工具
用于创建正式规范的规范语言
行为:法案允许指定存储更新、前置/后置条件和契约不变量。其工具套件还具有证明后端，能够通过 Coq、SMT 求解器或 hevm 证明许多属性。
Scribble 将 Scribble 规范语言中的代码注释转换为检查规范的具体断言。
Dafny 是一种可验证的编程语言，它依靠高级注释来推理和证明代码的正确性。
用于检查正确性的程序验证器
Certora Prover 是一种自动形式验证工具，用于检查智能合约中代码的正确性。规范以 CVL（Certora 验证语言）编写，并结合静态分析和约束求解来检测属性违规。
Solidity SMTChecker-Solidity 的 SMTChecker 是基于 SMT（可满足性模理论）和 Horn 求解的内置模型检查器。它确认合约的源代码在编译期间是否符合规范，并静态检查是否违反安全属性。
solc-verify 是 Solidity 编译器的扩展版本，可以使用注释和模块化程序验证对 Solidity 代码进行自动化形式验证。
KEVM 是用 K 框架编写的以太坊虚拟机（EVM）的形式语义。 KEVM 是可执行的，可以使用可达性逻辑证明某些与属性相关的断言。
定理证明的逻辑框架
Isabelle/HOL 是一个证明助手，允许用形式语言表达数学公式，并提供证明这些公式的工具。主要应用是数学证明的形式化，特别是形式验证，包括证明计算机硬件或软件的正确性以及证明计算机语言和协议的属性。
Coq 是一个交互式定理证明器，可让您使用定理定义程序并交互式生成机器检查的正确性证明。
用于检测智能合约中易受攻击模式的基于符号执行的工具
Manticore - 一款基于符号执行的EVM字节码分析工具。
hevm - hevm 是 EVM 字节码的符号执行引擎和等价检查器。
Consensys/mythril-用于检测以太坊智能合约漏洞的符号执行工具
声明：
- 本文转载自[ethereum]，著作权归属原作者[@ abooo96]，如对转载有异议，请联系Gate Learn团队，团队会根据相关流程尽速处理。
- 免责声明：本文所表达的观点和意见仅代表作者个人观点，不构成任何投资建议。
- 文章其他语言版本由Gate Learn团队翻译， 在未提及Gate.io的情况下不得复制、传播或抄袭经翻译文章。
相关文章
如何质押 ETH？
