一文读懂智能合约的形式化验证
引言
随着区块链上资产的价值迅速增长，各个项目轮番推出不同的加密经济应用场景。在此情况下，预防可能的漏洞和威胁比以往任何时候都更加重要。
比特币最初是为取代银行而设计的，但区块链技术却显示出它有取代所有中介的能力。在这个过程中，它带来了数字货币的全新可能性，比如编程货币，这是纸币无法实现的。这种数字货币通过允许合同的自动执行、用高透明度且无需人为干预的方法，推动了去中心化的发展。由此，律师和合同可以在金融交易中被替代。然而，智能合约究竟如何运作？我们真的可以信任这种不依赖信任的系统吗？
本文将深入探讨智能合约的形式化验证，分析其优缺点及其对加密生态的影响，特别是以太坊的应用。
智能合约发展简史
来源: CryptoSlate
尼克·萨博（Nick Szabo），美国计算机科学家和密码学家，常被认为是中本聪本人。作为智能合约创始人，他在1994年首次提出了“智能合约”这一概念。萨博将智能合约定义为用于自动执行协议条款的数字交易协议。他的初衷是改进电子交易方式，如POS系统，并将其能力扩展至数字领域。
萨博设想未来的协议将如同自动售货机一样，自动化、可靠且无法篡改。尽管当时的技术条件尚无法完全实现他的构想，但他的理念为后来区块链行业的变革奠定了基础。2015年，以太坊的推出使得智能合约真正得以应用，而萨博的理论也成为为去中心化应用中的关键技术。
他的愿景是让合约能够以精确、自动化的条款管理双方关系，减少对人为干预和监督需求。这一方法提供了一种更安全高效的协议管理方式，为智能合约的发展铺平了道路，使其成为区块链生态系统中的重要工具。萨博的早期见解至今仍在影响着数字交易和智能合约的发展。
什么是形式化验证？
来源: Medium
形式化验证是一种严格检查系统（如智能合约）是否符合既定规则或规范的过程。简而言之，它就是验证系统能否按预期运行，确保它满足必要的条件，并无误差地执行其预定功能。
为实现这一目标，该验证技术首先通过形式化模型描述系统的预期行为，然后使用规范语言定义合约必须满足的具体条件。随着文章的深入，我们会看到更多实际案例。形式化验证技术通过数学方式将合约的实际执行情况与其规范对照，确保其准确性。一旦合约符合这些规范，它就被认为是“功能正确”或“设计正确”，从而确认了其在区块链环境中的可靠性和安全性。
智能合约的形式化规范类型
来源: Ever Scale
形式化规范通过数学推理来验证程序运行是否准确。这些规范可以从整体行为（高层次）或合约内部运行细节（低层次）来描述。通过数学定义合约的行为，形式化规范确保合约按预期工作。
高层规范
高层规范，也称为模型导向规范，描述了智能合约的整体运行状态，把它看作是一个有限状态机（FSM），通过特定操作在不同状态之间进行转换。时序逻辑经常用于定义这些转换的规则，详细说明合约如何随着时间推移发生状态的改变，以及必须满足的条件。
高层规范主要强调两个方面：安全性和活性。安全性可以避免意外事件的发生，比如发送者的账户余额不足以进行交易。活性则保证合约能持续正常运行，如维持足够的流动性，确保用户能够随时提取资金。二者共同确保智能合约的安全性与可靠性，保护用户的资产与交互体验。
低层规范
低层规范也称为属性导向规范，重点在于通过分析合约内部的执行过程来定义其行为是否正确。不同于高层规范将合约视为有限状态机，低层规范将智能合约视为数学函数系统，并分析函数执行的顺序（称为轨迹），这些轨迹会引起合约状态的变化。
智能合约的形式化验证技术
来源: Ever Scale
模型检测
模型检测是一种利用算法来检查智能合约模型是否符合预定规范的验证方法。智能合约通常被表示为状态转换系统，其属性通过时序逻辑来定义。这一方法通过创建一个数学模型并用逻辑公式来描述其行为，进而让算法验证该模型是否符合要求。
定理证明
与模型检查不同，定理证明是一种数学方法，用于验证程序（包括智能合约）的正确性。此方法将合约的模型和规范转换为逻辑公式，以验证它们的逻辑等价性，即一个命题为真，另一个命题也为真。通过将这种关系表述为定理，自动定理证明工具可以验证合约模型与其规范的正确性。
与仅限于有限状态系统的模型检测不同，定理证明可以分析无限状态系统，但通常需要人工指导来解决复杂的逻辑问题。因此，定理证明往往比完全自动化的模型检测更加耗时耗力。
符号执行
符号执行是一种强大的智能合约分析方法，通过使用符号值而非具体输入来执行函数。这种方法将合约的执行路径转化为数学公式（称为路径谓词），并利用SMT求解器来确定这些谓词是否成立，即是否存在符合条件的输入。
例如，如果某个合约函数在值为5到10之间时发生回滚，符号执行可以通过评估条件X > 5 且 X < 10 来快速找到触发这一条件的值。这种方法比传统测试更有效，误报率较低，并且能够直接生成能触发错误的具体数值，是确保智能合约可靠性的强大工具。
什么是智能合约？
来源: Tenderly
智能合约是运行在区块链上的自动化程序，在满足特定条件时自动执行相应操作。它们可以从简单协议到复杂的程序，能够管理数百万甚至数十亿美元的资产。
智能合约不仅有可能彻底变革政治投票、供应链管理、医疗和房地产等领域，本文则侧重于其在加密货币领域的应用。智能合约的设计能够让多方在无需担心操控风险的前提下进行合作，提供了一个透明且安全的框架，提升了效率与创新。然而，我们也需要意识到智能合约仍然存在安全漏洞和挑战。
智能合约的安全漏洞
智能合约代码中的安全漏洞可能会导致灾难性的后果，例如合约中所有资产的丧失。近期发生的事件充分说明了这一点。
- 2021年，自动做市商Uranium Finance 因智能合约中的一个拼写错误，被盗取了5000万美元。
- 同样在2021年，Compound Finance 由于一个字符错误，意外发放了8000万美元的未赚取奖励。
- 2022年，Wormhole Bridge 因智能合约中的漏洞被盗取了3.2亿美元。
这些例子表明，智能合约在部署之前，必须确保其代码的准确性。智能合约是开源的，一旦部署，代码公开可见，黑客就可以轻松利用发现的漏洞。此外，智能合约的不可修改性决定了代码一旦发布，安全漏洞通常无法被修复。所以，如果开发不够精确，它们将始终在风险之中。
智能合约的验证是如何进行的？
来源: Certik
该过程包括以下步骤：
- 使用形式化语言明确合约的规范和期望的功能。
- 将合约代码转化为数学模型或逻辑表达式等形式化表示。
- 使用自动定理验证器或模型检查器来确认合约的规范和属性是否有效。
- 通过反复验证，发现并修正与预期属性不符的错误或偏差。
智能合约的关键特性
来源: Certik
可以将智能合约视为“刻在石头上的协议”，一旦创建便无法修改。这些合约运行在区块链的不可篡改账本上，无需中介即可自动执行条款，从而加速交易并降低成本。这种固定的特性不仅增强了安全性，还实现了去中心化管理，大大降低了欺诈和腐败的风险。
为什么智能合约的验证如此重要？
通过数学推理，形式化验证确保智能合约不存在漏洞、错误或意外行为。合约执行过程的严格提升了人们对合约的信任度，因为其功能和属性已被彻底地验证过。
智能合约验证的成功案例突显了其在避免重大财务损失方面的重要作用。
Uniswap
例如，著名的自动做市商Uniswap在其V1智能合约开发期间进行形式化验证，发现并修复了可能导致资金损失的错误。
Balancer
同样，另一个AMM Balancer V2通过形式化验证发现了与闪电贷相关的费用计算错误，从而避免了潜在的盗窃风险。
SafeMoon
SafeMoon V1 在部署后通过形式化验证识别出一个细微的漏洞。这个漏洞允许所有者在特定条件下放弃所有权并重新获得控制权，而这一细节由于复杂性被大多数人工审计忽略。而形式化验证通过分析变量值的特定组合，能有效捕捉到人工审计可能遗漏的问题。
形式化验证与人工审计如何共同协作？
形式化验证是一种自动化的、系统的方法，用来检查智能合约的逻辑和行为是否符合其预期功能。这种方法能够简化发现和修正错误的过程，尤其是在人工审计可能忽略的复杂问题上。
而人工审计则是由专家对合约代码、设计和部署的全面检查。审计员利用他们的经验发现潜在的安全隐患，并评估合约的整体安全状况。他们还可以验证形式化验证过程的准确性，并找出自动化工具可能忽略的漏洞。形式化验证与人工审计相结合，能够提供全面的安全评估，增加发现和修复漏洞的可能性，结合以往的经验和自动化分析，从而建立强大的安全防线。
智能合约的优缺点
来源: Blockonomi
智能合约虽然并不完美，但其优点显著多余缺点。它们简化了复杂的交易，节省了时间和成本，同时提高了工作流程的透明度并减少了争议。此外，智能合约依赖于代码运行，也减少了人为错误。其加密保护同样确保了极高的安全性。然而，智能合约缺乏灵活性，难以应对意外情况。并且，设置智能合约需要专业的编程技能，这对一些人来说是一个障碍。尽管挑战存在，智能合约正在推动多个行业的变革。
智能合约的优点
- 自动化操作，提高效率，节省时间和金钱。
- 提高透明度，减少争议，各方均可访问相同的信息。
- 减少错误，因为它们依赖代码，消除人为错误。
- 通过加密技术加强安全性，难以被篡改。
智能合约的缺点
- 缺乏灵活性，难以应对意外情况。
- 需要专业的编程技能，广泛使用依赖于技术门槛。
以太坊智能合约的形式化验证工具
来源: Calibraint
用于编写形式化规范的语言
- Act: Act允许用户定义存储更新、前置条件、后置条件以及合约的不变性。它的工具套件提供了可以使用Coq、SMT求解器或hevm来验证各种属性的验证后端。
- Scribble: Scribble能够将用其特定语言编写的代码注释转换为验证规范的断言。
- Dafny: Dafny是一种专为验证设计的编程语言，借助高级注释来帮助推理并验证代码的正确性。
用于验证合约正确性的工具
- Certora Prover: Certora Prover是一种自动化的形式化验证工具，专门用于检查智能合约代码的正确性。它使用Certora验证语言（CVL）创建合约规范，并通过静态分析和约束求解技术来检测潜在的属性违规。
- Solidity SMTChecker: 这是Solidity内置的模型检查器，它利用SMT（可满足性模理论）和Horn求解技术来确保合约源代码在编译时符合预定规范，并检测安全属性是否存在违规。
- Solc-verify: Solc-verify是Solidity编译器的增强版，它能够通过注释和模块化的程序验证来实现Solidity代码的自动化形式化验证。
- KEVM: KEVM是通过K框架创建的以太坊虚拟机（EVM）的形式化表示。它能够执行并使用可达性逻辑验证特定属性。
用于定理证明的工具框架
- Isabelle: Isabelle/HOL是一个帮助用户以形式化语言表达数学公式的证明助手，并提供了证明这些公式的工具。它主要用于形式化数学证明，尤其在验证计算机硬件、软件和编程语言等方面的正确性。
- Coq：Coq是一个交互式定理证明工具，它通过交互式过程帮助用户定义程序与定理，并创建机器可验证的正确性证明。
基于符号执行的漏洞检测工具
- Manticore - Manticore是一款使用符号执行分析EVM字节码的工具，专门用于检测漏洞。GitHub
- Hevm - hevm是一个符号执行引擎，用于检查EVM字节码的等价性。
- Mythril - Mythril是一种符号执行工具，专门用于发现以太坊智能合约中的潜在漏洞。
结论
为了确保智能合约的安全性，将形式化验证与人工审计结合是至关重要的。这种组合能够全面评估合约安全性。尽管形式化验证耗费资源，但对于高风险或涉及大量资金的合约来说，这是一项值得投入的安全保障。智能合约不只是一个流行概念，它们已经在全球业务中发挥了重要作用。尽管存在一些挑战，但智能合约在提高效率、减少错误和提升安全性方面具备独特优势。它们将简化业务流程，增强数字交易中的信任度。而那些现在正在采用这项技术的公司，将在未来强调透明度和可靠性的加密经济大环境中占据优势。
相关文章
如何质押 ETH？
一文读懂智能合约的形式化验证
引言
随着区块链上资产的价值迅速增长，各个项目轮番推出不同的加密经济应用场景。在此情况下，预防可能的漏洞和威胁比以往任何时候都更加重要。
比特币最初是为取代银行而设计的，但区块链技术却显示出它有取代所有中介的能力。在这个过程中，它带来了数字货币的全新可能性，比如编程货币，这是纸币无法实现的。这种数字货币通过允许合同的自动执行、用高透明度且无需人为干预的方法，推动了去中心化的发展。由此，律师和合同可以在金融交易中被替代。然而，智能合约究竟如何运作？我们真的可以信任这种不依赖信任的系统吗？
本文将深入探讨智能合约的形式化验证，分析其优缺点及其对加密生态的影响，特别是以太坊的应用。
智能合约发展简史
来源: CryptoSlate
尼克·萨博（Nick Szabo），美国计算机科学家和密码学家，常被认为是中本聪本人。作为智能合约创始人，他在1994年首次提出了“智能合约”这一概念。萨博将智能合约定义为用于自动执行协议条款的数字交易协议。他的初衷是改进电子交易方式，如POS系统，并将其能力扩展至数字领域。
萨博设想未来的协议将如同自动售货机一样，自动化、可靠且无法篡改。尽管当时的技术条件尚无法完全实现他的构想，但他的理念为后来区块链行业的变革奠定了基础。2015年，以太坊的推出使得智能合约真正得以应用，而萨博的理论也成为为去中心化应用中的关键技术。
他的愿景是让合约能够以精确、自动化的条款管理双方关系，减少对人为干预和监督需求。这一方法提供了一种更安全高效的协议管理方式，为智能合约的发展铺平了道路，使其成为区块链生态系统中的重要工具。萨博的早期见解至今仍在影响着数字交易和智能合约的发展。
什么是形式化验证？
来源: Medium
形式化验证是一种严格检查系统（如智能合约）是否符合既定规则或规范的过程。简而言之，它就是验证系统能否按预期运行，确保它满足必要的条件，并无误差地执行其预定功能。
为实现这一目标，该验证技术首先通过形式化模型描述系统的预期行为，然后使用规范语言定义合约必须满足的具体条件。随着文章的深入，我们会看到更多实际案例。形式化验证技术通过数学方式将合约的实际执行情况与其规范对照，确保其准确性。一旦合约符合这些规范，它就被认为是“功能正确”或“设计正确”，从而确认了其在区块链环境中的可靠性和安全性。
智能合约的形式化规范类型
来源: Ever Scale
形式化规范通过数学推理来验证程序运行是否准确。这些规范可以从整体行为（高层次）或合约内部运行细节（低层次）来描述。通过数学定义合约的行为，形式化规范确保合约按预期工作。
高层规范
高层规范，也称为模型导向规范，描述了智能合约的整体运行状态，把它看作是一个有限状态机（FSM），通过特定操作在不同状态之间进行转换。时序逻辑经常用于定义这些转换的规则，详细说明合约如何随着时间推移发生状态的改变，以及必须满足的条件。
高层规范主要强调两个方面：安全性和活性。安全性可以避免意外事件的发生，比如发送者的账户余额不足以进行交易。活性则保证合约能持续正常运行，如维持足够的流动性，确保用户能够随时提取资金。二者共同确保智能合约的安全性与可靠性，保护用户的资产与交互体验。
低层规范
低层规范也称为属性导向规范，重点在于通过分析合约内部的执行过程来定义其行为是否正确。不同于高层规范将合约视为有限状态机，低层规范将智能合约视为数学函数系统，并分析函数执行的顺序（称为轨迹），这些轨迹会引起合约状态的变化。
智能合约的形式化验证技术
来源: Ever Scale
模型检测
模型检测是一种利用算法来检查智能合约模型是否符合预定规范的验证方法。智能合约通常被表示为状态转换系统，其属性通过时序逻辑来定义。这一方法通过创建一个数学模型并用逻辑公式来描述其行为，进而让算法验证该模型是否符合要求。
定理证明
与模型检查不同，定理证明是一种数学方法，用于验证程序（包括智能合约）的正确性。此方法将合约的模型和规范转换为逻辑公式，以验证它们的逻辑等价性，即一个命题为真，另一个命题也为真。通过将这种关系表述为定理，自动定理证明工具可以验证合约模型与其规范的正确性。
与仅限于有限状态系统的模型检测不同，定理证明可以分析无限状态系统，但通常需要人工指导来解决复杂的逻辑问题。因此，定理证明往往比完全自动化的模型检测更加耗时耗力。
符号执行
符号执行是一种强大的智能合约分析方法，通过使用符号值而非具体输入来执行函数。这种方法将合约的执行路径转化为数学公式（称为路径谓词），并利用SMT求解器来确定这些谓词是否成立，即是否存在符合条件的输入。
例如，如果某个合约函数在值为5到10之间时发生回滚，符号执行可以通过评估条件X > 5 且 X < 10 来快速找到触发这一条件的值。这种方法比传统测试更有效，误报率较低，并且能够直接生成能触发错误的具体数值，是确保智能合约可靠性的强大工具。
什么是智能合约？
来源: Tenderly
智能合约是运行在区块链上的自动化程序，在满足特定条件时自动执行相应操作。它们可以从简单协议到复杂的程序，能够管理数百万甚至数十亿美元的资产。
智能合约不仅有可能彻底变革政治投票、供应链管理、医疗和房地产等领域，本文则侧重于其在加密货币领域的应用。智能合约的设计能够让多方在无需担心操控风险的前提下进行合作，提供了一个透明且安全的框架，提升了效率与创新。然而，我们也需要意识到智能合约仍然存在安全漏洞和挑战。
智能合约的安全漏洞
智能合约代码中的安全漏洞可能会导致灾难性的后果，例如合约中所有资产的丧失。近期发生的事件充分说明了这一点。
- 2021年，自动做市商Uranium Finance 因智能合约中的一个拼写错误，被盗取了5000万美元。
- 同样在2021年，Compound Finance 由于一个字符错误，意外发放了8000万美元的未赚取奖励。
- 2022年，Wormhole Bridge 因智能合约中的漏洞被盗取了3.2亿美元。
这些例子表明，智能合约在部署之前，必须确保其代码的准确性。智能合约是开源的，一旦部署，代码公开可见，黑客就可以轻松利用发现的漏洞。此外，智能合约的不可修改性决定了代码一旦发布，安全漏洞通常无法被修复。所以，如果开发不够精确，它们将始终在风险之中。
智能合约的验证是如何进行的？
来源: Certik
该过程包括以下步骤：
- 使用形式化语言明确合约的规范和期望的功能。
- 将合约代码转化为数学模型或逻辑表达式等形式化表示。
- 使用自动定理验证器或模型检查器来确认合约的规范和属性是否有效。
- 通过反复验证，发现并修正与预期属性不符的错误或偏差。
智能合约的关键特性
来源: Certik
可以将智能合约视为“刻在石头上的协议”，一旦创建便无法修改。这些合约运行在区块链的不可篡改账本上，无需中介即可自动执行条款，从而加速交易并降低成本。这种固定的特性不仅增强了安全性，还实现了去中心化管理，大大降低了欺诈和腐败的风险。
为什么智能合约的验证如此重要？
通过数学推理，形式化验证确保智能合约不存在漏洞、错误或意外行为。合约执行过程的严格提升了人们对合约的信任度，因为其功能和属性已被彻底地验证过。
智能合约验证的成功案例突显了其在避免重大财务损失方面的重要作用。
Uniswap
例如，著名的自动做市商Uniswap在其V1智能合约开发期间进行形式化验证，发现并修复了可能导致资金损失的错误。
Balancer
同样，另一个AMM Balancer V2通过形式化验证发现了与闪电贷相关的费用计算错误，从而避免了潜在的盗窃风险。
SafeMoon
SafeMoon V1 在部署后通过形式化验证识别出一个细微的漏洞。这个漏洞允许所有者在特定条件下放弃所有权并重新获得控制权，而这一细节由于复杂性被大多数人工审计忽略。而形式化验证通过分析变量值的特定组合，能有效捕捉到人工审计可能遗漏的问题。
形式化验证与人工审计如何共同协作？
形式化验证是一种自动化的、系统的方法，用来检查智能合约的逻辑和行为是否符合其预期功能。这种方法能够简化发现和修正错误的过程，尤其是在人工审计可能忽略的复杂问题上。
而人工审计则是由专家对合约代码、设计和部署的全面检查。审计员利用他们的经验发现潜在的安全隐患，并评估合约的整体安全状况。他们还可以验证形式化验证过程的准确性，并找出自动化工具可能忽略的漏洞。形式化验证与人工审计相结合，能够提供全面的安全评估，增加发现和修复漏洞的可能性，结合以往的经验和自动化分析，从而建立强大的安全防线。
智能合约的优缺点
来源: Blockonomi
智能合约虽然并不完美，但其优点显著多余缺点。它们简化了复杂的交易，节省了时间和成本，同时提高了工作流程的透明度并减少了争议。此外，智能合约依赖于代码运行，也减少了人为错误。其加密保护同样确保了极高的安全性。然而，智能合约缺乏灵活性，难以应对意外情况。并且，设置智能合约需要专业的编程技能，这对一些人来说是一个障碍。尽管挑战存在，智能合约正在推动多个行业的变革。
智能合约的优点
- 自动化操作，提高效率，节省时间和金钱。
- 提高透明度，减少争议，各方均可访问相同的信息。
- 减少错误，因为它们依赖代码，消除人为错误。
- 通过加密技术加强安全性，难以被篡改。
智能合约的缺点
- 缺乏灵活性，难以应对意外情况。
- 需要专业的编程技能，广泛使用依赖于技术门槛。
以太坊智能合约的形式化验证工具
来源: Calibraint
用于编写形式化规范的语言
- Act: Act允许用户定义存储更新、前置条件、后置条件以及合约的不变性。它的工具套件提供了可以使用Coq、SMT求解器或hevm来验证各种属性的验证后端。
- Scribble: Scribble能够将用其特定语言编写的代码注释转换为验证规范的断言。
- Dafny: Dafny是一种专为验证设计的编程语言，借助高级注释来帮助推理并验证代码的正确性。
用于验证合约正确性的工具
- Certora Prover: Certora Prover是一种自动化的形式化验证工具，专门用于检查智能合约代码的正确性。它使用Certora验证语言（CVL）创建合约规范，并通过静态分析和约束求解技术来检测潜在的属性违规。
- Solidity SMTChecker: 这是Solidity内置的模型检查器，它利用SMT（可满足性模理论）和Horn求解技术来确保合约源代码在编译时符合预定规范，并检测安全属性是否存在违规。
- Solc-verify: Solc-verify是Solidity编译器的增强版，它能够通过注释和模块化的程序验证来实现Solidity代码的自动化形式化验证。
- KEVM: KEVM是通过K框架创建的以太坊虚拟机（EVM）的形式化表示。它能够执行并使用可达性逻辑验证特定属性。
用于定理证明的工具框架
- Isabelle: Isabelle/HOL是一个帮助用户以形式化语言表达数学公式的证明助手，并提供了证明这些公式的工具。它主要用于形式化数学证明，尤其在验证计算机硬件、软件和编程语言等方面的正确性。
- Coq：Coq是一个交互式定理证明工具，它通过交互式过程帮助用户定义程序与定理，并创建机器可验证的正确性证明。
基于符号执行的漏洞检测工具
- Manticore - Manticore是一款使用符号执行分析EVM字节码的工具，专门用于检测漏洞。GitHub
- Hevm - hevm是一个符号执行引擎，用于检查EVM字节码的等价性。
- Mythril - Mythril是一种符号执行工具，专门用于发现以太坊智能合约中的潜在漏洞。
结论
为了确保智能合约的安全性，将形式化验证与人工审计结合是至关重要的。这种组合能够全面评估合约安全性。尽管形式化验证耗费资源，但对于高风险或涉及大量资金的合约来说，这是一项值得投入的安全保障。智能合约不只是一个流行概念，它们已经在全球业务中发挥了重要作用。尽管存在一些挑战，但智能合约在提高效率、减少错误和提升安全性方面具备独特优势。它们将简化业务流程，增强数字交易中的信任度。而那些现在正在采用这项技术的公司，将在未来强调透明度和可靠性的加密经济大环境中占据优势。
相关文章
如何质押 ETH？