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