跳到主要内容

智能合约的形式化验证与 AI 辅助审计

· 阅读需 43 分钟
Dora Noda
Dora Noda
Software Engineer

智能合约审计中的形式化验证​

形式化验证是指使用基于数学和逻辑的技术来证明智能合约的正确性和安全性。在实践中，这涵盖了一系列方法：从基于属性的模糊测试和符号执行，到严格的定理证明和模型检查。其目标是确保合约满足其规范，并且在所有可能的输入和状态下不包含可利用的漏洞。鉴于 DeFi 协议中锁定了数十亿美元的巨额资金，形式化方法对于以太坊和其他区块链平台变得越来越重要。

传统方法： 以太坊早期的形式化方法包括像 Oyente 和 Mythril 这样的符号执行工具，以及像 Slither 和 Securify 这样的静态分析器。符号执行通过符号输入探索程序路径以检测问题（例如重入、整数溢出），而静态分析则使用基于规则的模式匹配。这些工具取得了一定的成功，但也存在局限性：例如，Oyente 即使在简单的合约上也会产生许多误报，而 Slither 基于模式的检测器也可能产生一些假阳性。此外，2023 年的一项研究发现，超过 80% 的可利用合约漏洞（尤其是复杂的“业务逻辑”漏洞）被现有工具所忽略，这凸显了对更强大验证技术的需求。

全面验证的前景与挑战： 理论上，形式化验证可以通过对所有状态进行详尽的不变量检查来证明漏洞不存在。像 Certora Prover 或以太坊基金会的 KEVM 框架等工具旨在根据形式化规范对智能合约进行数学验证。例如，Certora 的“自动化数学审计器”使用一种规范语言 (CVL) 来证明或反驳用户定义的规则。然而，在实践中，完全证明真实世界合约的属性通常是无法实现或非常耗费人力的。代码可能需要重写为简化的形式以便验证，必须编写自定义规范，循环和复杂算术可能需要手动设置边界或进行抽象，而 SMT 求解器在处理复杂逻辑时经常超时。正如 Trail of Bits 的工程师所指出的，在非平凡的代码库上*“证明漏洞不存在通常是无法实现的”*，并且实现这一目标通常需要大量的用户干预和专业知识。因此，形式化验证工具传统上仅用于代码的关键部分（例如，验证代币的不变量或共识算法），而不是端到端地验证整个合约。

Foundry 的模糊测试和不变量测试​

近年来，基于属性的测试已成为完全形式化证明的一种实用替代方案。Foundry 是一个流行的以太坊开发框架，它内置了对模糊测试和不变量测试的支持——这些技术极大地增强了测试覆盖率，可以被视为轻量级的形式化验证。Foundry 的模糊测试会自动生成大量输入，试图违反指定的属性，而不变量测试则将此扩展到一系列改变状态的操作：

  • 模糊测试： 开发者不再为特定输入编写单元测试，而是指定应在任何输入下都成立的属性或不变量。然后，Foundry 生成成百上千个随机输入来测试该函数，并检查该属性是否始终成立。这有助于捕捉开发者可能不会手动想到去测试的边缘情况。例如，模糊测试可能会断言函数的返回值始终为非负数，或者某个后置条件在任何输入下都为真。Foundry 的引擎使用智能启发式方法——它分析函数签名并引入边缘情况值（0, max uint 等）——以触及可能破坏属性的角落案例。如果断言失败，Foundry 会报告一个违反该属性的反例输入。

  • 不变量测试： Foundry 的不变量测试（也称为状态模糊测试）更进一步，它会按顺序执行多个函数调用和状态转换。开发者编写在合约生命周期内应始终为真的不变量函数（例如，总资产 = 用户余额之和）。然后，Foundry 随机生成调用序列（带有随机输入）来模拟多种可能的使用场景，并定期检查不变量条件是否仍然为真。这可以发现只有在特定操作序列后才会显现的复杂漏洞。本质上，不变量测试更彻底地探索了合约的状态空间，确保任何有效的交易序列都不能违反所声明的属性。

Foundry 的重要性： Foundry 使这些先进的测试技术变得易于使用。模糊测试和不变量功能原生于开发者工作流——不需要特殊的测试工具或外部工具，测试与单元测试一起用 Solidity 编写。得益于基于 Rust 的引擎，Foundry 可以快速执行数千个测试（并行化它们），并为任何不变量违规提供详细的失败跟踪。开发者报告说，Foundry 的模糊测试器易于使用且性能高，只需要少量配置（例如，设置迭代次数或添加假设来约束输入）。Foundry 文档中的一个简单例子是 divide(a,b) 函数的模糊测试，它使用 vm.assume(b != 0) 来避免无意义的无效输入，然后断言数学后置条件，如 result * b <= a。通过用数千个随机的 (a,b) 对运行这样的测试，Foundry 可能会迅速发现难以通过手动推理找到的边缘情况（如溢出边界）。

比较： Foundry 的方法建立在社区先前工作的基础上。Trail of Bits 的 Echidna 模糊测试器是早期用于以太坊的基于属性的测试工具。Echidna 同样生成随机交易来寻找违反不变量的情况，这些不变量表示为返回布尔值的 Solidity 函数。它以“智能”输入生成（结合了覆盖率引导的模糊测试）而闻名，并已用于发现许多漏洞。事实上，安全研究人员指出，Echidna 的引擎非常有效——“Trail of Bits 的 Echidna 是目前最好的模糊测试器，因为它有智能的随机数选择”——尽管 Foundry 的集成工作流使开发者编写测试更简单。在实践中，Foundry 的模糊测试通常被视为安全 Solidity 开发的新的**“最低标准”**，补充了传统的单元测试。它不能证明漏洞不存在（因为它是随机的而不是详尽的），但通过覆盖大量的输入和状态组合，它极大地增加了信心。

超越模糊测试：形式化证明和高级工具​

虽然模糊测试和不变量测试能捕捉到许多问题，但在某些情况下会使用更强的形式化方法。模型检查和定理证明涉及用形式化逻辑指定期望的属性，并使用自动证明器来对照合约代码进行检查。Certora Prover（最近已开源）是这一类别中的一个著名工具。它允许开发者用一种领域特定语言 (CVL) 编写规则，然后自动检查合约是否违反这些规则。Certora 已被用于验证 MakerDAO 和 Compound 等协议中的关键不变量；例如，它识别出了 MakerDAO 中被忽视了四年的“DAI 债务不变量”漏洞（一个微妙的记账不一致问题）。值得注意的是，Certora 的引擎现在支持多个平台（EVM、Solana 的 VM 和 eWASM），并且通过在 2025 年开源，它使得工业级的形式化验证在以太坊、Solana 和 Stellar 上免费可用。此举承认了形式化证明不应只是资金雄厚的团队的奢侈品。

其他形式化工具包括运行时验证方法（例如，以太坊的 KEVM 语义，或用于 Move-based 链的 Move Prover）。特别是 Move Prover 内置于 Move 语言中（被 Aptos 和 Sui 区块链使用）。它允许在代码旁边编写形式化规范，并能以类似于 linter 或类型检查器的用户体验自动证明某些属性。这种紧密的集成降低了这些平台上的开发者在开发过程中使用形式化验证的门槛。

总结： 如今的智能合约审计融合了这些方法。模糊测试和不变量测试（以 Foundry 和 Echidna 为代表）因其易用性和在捕捉常见漏洞方面的有效性而被广泛采用。符号执行和静态分析器仍然用于快速扫描已知的漏洞模式（像 Slither 这样的工具通常被集成到 CI 管道中）。与此同时，形式化验证工具正在成熟并扩展到多个链，但由于其复杂性，它们通常被保留用于特定的关键属性或由专业的审计公司使用。在实践中，许多审计结合了这些方法：例如，使用模糊测试器查找运行时错误，使用静态工具标记明显的错误，并对关键不变量（如“代币余额不超过总供应量”）进行形式化规范检查。

使用大语言模型的 AI 辅助审计​

像 OpenAI 的 GPT-3/4 (ChatGPT) 和 Codex 这样的大语言模型 (LLMs) 的出现，为智能合约分析引入了一种新的范式。这些模型在大量代码和自然语言上进行训练，能够推理程序行为、解释代码，甚至通过模式识别和“常识”知识检测某些漏洞。问题是：AI 能否增强甚至自动化智能合约审计？

基于 LLM 的漏洞分析工具​

已经出现了几项将 LLM 应用于智能合约审计的研究工作和原型工具：

  • OpenAI Codex / ChatGPT (通用模型)： 早期的实验只是简单地向 GPT-3 或 Codex 提供合约代码并询问潜在的漏洞。开发者发现 ChatGPT 可以识别一些众所周知的漏洞模式，甚至建议修复方案。然而，响应时好时坏，并不可靠地全面。最近的一项学术评估指出，在基准数据集上，天真地提示 ChatGPT 进行漏洞检测*“与随机预测相比，并未产生显著更好的结果”*——基本上，如果模型没有得到适当的引导，它可能会捏造不存在的问题或错过真正的漏洞。这凸显了需要精心设计的提示词或微调才能获得有用结果。

  • AuditGPT (2024)： 这是一个学术工具，专门利用 ChatGPT (GPT-3.5/4) 来检查以太坊合约中的 ERC 标准合规性。研究人员观察到，许多 ERC20/ERC721 代币合约违反了标准的微妙规则（这可能导致安全或兼容性问题）。AuditGPT 的工作方式是将审计分解为小任务，并为每种规则类型设计专门的提示词。结果令人印象深刻：在对真实合约的测试中，AuditGPT “成功地指出了 418 个 ERC 规则违规，并且只报告了 18 个误报”，展示了高准确性。事实上，该论文声称 AuditGPT 在发现 ERC 合规性漏洞方面优于专业的审计服务，且成本更低。这表明，对于定义明确、范围狭窄的领域（如执行一系列标准规则），一个带有良好提示词的 LLM 可以非常有效和精确。

  • LLM-SmartAudit (2024)： 另一个研究项目 LLM-SmartAudit 采用更广泛的方法，使用多代理对话系统来审计 Solidity 代码。它设置了多个专门的 GPT-3.5/GPT-4 代理（例如，一个“审计员”专注于正确性，一个“攻击者”思考如何利用），它们相互交谈来分析一个合约。在他们的评估中，LLM-SmartAudit 能够检测到广泛的漏洞。值得注意的是，在与传统工具的对比测试中，基于 GPT-3.5 的系统实现了最高的整体召回率 (74%)，超过了他们测试的所有传统静态和符号分析器（次好的是 Mythril，召回率为 54%）。它还能够找到他们测试套件中所有 10 种类型的漏洞（而每个传统工具都在某些类别上表现不佳）。此外，通过切换到 GPT-4 并集中分析（他们称之为目标分析模式），该系统可以检测到像 Slither 和 Mythril 完全错过的复杂逻辑缺陷。例如，在一组真实世界的 DeFi 合约上，基于 LLM 的方法发现了数百个逻辑漏洞，而静态工具*“在检测这些问题上没有表现出任何效果”*。这些结果展示了 LLM 在捕捉超出传统分析器模式匹配范围的微妙漏洞方面的潜力。

  • Prometheus (PromFuzz) (2023)： 一种混合方法是使用 LLM 来指导其他技术。一个例子是 PromFuzz，它使用一个基于 GPT 的“审计员代理”来识别代码中的可疑区域，然后自动生成不变量检查器并将其输入到模糊测试引擎中。本质上，LLM 进行第一遍分析（从善意和攻击者的角度），以将模糊测试集中在可能的漏洞上。在评估中，这种方法实现了非常高的漏洞发现率——例如，在某些基准测试集中召回率超过 86%，且零误报——显著优于独立的模糊测试器或以前的工具。这是一个有前途的方向：使用 AI 来协调和增强像模糊测试这样的经典技术，结合两者的优势。

  • 其他 AI 工具： 社区已经看到了各种其他 AI 辅助审计的概念。例如，Trail of Bits 的“Toucan”项目将 OpenAI Codex 集成到他们的审计工作流中（下文将详细介绍其发现）。一些安全初创公司也在宣传 AI 审计器（例如，“ChainGPT Audit”服务），通常是用自定义提示词包装 GPT-4 来审查合约。开源爱好者在论坛上创建了基于 ChatGPT 的审计机器人，可以接收 Solidity 代码片段并输出潜在问题。虽然其中许多是实验性的，但总体趋势是明确的：AI 正在安全审查过程的各个层面被探索，从自动代码解释和文档生成到漏洞检测，甚至建议修复方案。

LLM 审计器的能力与局限性​

LLM 在智能合约审计中展示了显著的能力：

  • 广泛的知识： 像 GPT-4 这样的 LLM 已经在无数的代码和漏洞上进行了训练。它“知道”常见的安全陷阱（重入、整数溢出等），甚至一些历史上的漏洞利用。这使得它能够识别可能表明存在漏洞的模式，并从文档中回忆起最佳实践。例如，它可能记得 ERC-20 的 transferFrom 应该检查授权（并将缺少此类检查标记为违规）。与只标记已知模式的静态工具不同，LLM 可以对新颖的代码应用推理，并推断出工具开发者没有明确编码进去的问题。

  • 自然的解释： AI 审计器可以提供人类可读的潜在问题解释。这对开发者体验非常有价值。传统工具通常输出需要专业知识才能解释的神秘警告，而基于 GPT 的工具可以生成一段用通俗英语解释漏洞的段落，甚至建议修复方案。例如，AuditGPT 不仅标记了 ERC 规则违规，还描述了代码为何违反规则以及其影响。这有助于引导经验较少的开发者了解安全概念。

  • 灵活性： 通过提示词工程，可以引导 LLM 关注不同的方面或遵循自定义的安全策略。它们不受固定规则集的限制——如果你能用语言描述一个属性或模式，LLM 就可以尝试检查它。这使得它们在审计可能具有独特不变量或逻辑的新协议时很有吸引力（在这种情况下，从头开始编写自定义静态分析是不可行的）。

然而，也观察到了重大的挑战和可靠性问题：

  • 推理限制： 当前的 LLM 有时难以进行安全分析所需的复杂逻辑推理。Trail of Bits 报告说，“这些模型无法很好地推理某些更高级别的概念，例如合约的所有权、重入和函数间关系”。例如，GPT-3.5/4 可能在理论上理解什么是重入（甚至可以解释它），但如果需要理解跨函数的调用序列和状态变化，它可能无法识别出重入漏洞。模型也可能错过涉及多合约交互或时间依赖逻辑的漏洞，因为这些超出了单个代码片段分析的范围。

  • 误报和幻觉： 一个主要问题是 LLM 可能会产生听起来自信但实际上不正确的结论。在审计中，“幻觉”可能是标记一个实际上不存在的漏洞，或误解代码。Trail of Bits 使用 Codex (GPT) 的实验发现，当他们扩展到更大的真实世界合约时，“误报和幻觉率变得过高”，以至于会因为太多虚假的报告而减慢审计员的速度。这种不可预测性是有问题的——一个经常“狼来了”的工具不会被开发者信任。AuditGPT 在保持低误报率（数百个发现中只有 18 个）方面的成功令人鼓舞，但那是在一个受限的领域。在通用用途中，需要仔细的提示词设计和可能的人工审查循环来过滤 AI 的发现。

  • 上下文限制： LLM 有上下文窗口限制，这意味着它们一次只能“看到”一定数量的代码。复杂的合约通常跨越多个文件和数千行代码。如果 AI 无法消化整个代码库，它可能会错过重要的联系。像代码切片（分块提供合约）这样的技术被使用，但它们有失去全局视野的风险。LLM-SmartAudit 团队指出，使用 GPT-3.5 的 4k token 限制，他们无法分析一些大型的真实世界合约，直到他们切换到具有更大上下文的 GPT-4。即便如此，将分析分成部分也可能导致它忽略只有在考虑整个系统时才会显现的漏洞。这使得 AI 对整个协议（具有多个交互合约）的分析目前仍然是一个真正的挑战。

  • 集成和工具： 围绕 AI 审计器的强大开发者工具仍然缺乏。运行 LLM 分析不像运行 linter 那样直接。它涉及对模型的 API 调用、处理提示词工程、速率限制以及解析 AI 的响应。正如一个审计团队所说，“围绕将 LLM 与传统软件集成的软件生态系统过于粗糙，一切都很麻烦”。几乎没有现成的框架可以在 CI 管道中持续部署 AI 审计器，同时管理其不确定性。这种情况正在慢慢改善（一些项目正在探索使用 GPT-4 进行代码审查的 CI 机器人），但这还处于早期阶段。此外，调试 AI 给出某个结果的原因很困难——与确定性工具不同，你无法轻易地追踪导致模型标记或错过某事的逻辑。

  • 成本和性能： 使用像 GPT-4 这样的大型模型是昂贵的，而且可能很慢。如果你想将 AI 审计集成到 CI/CD 管道中，它可能会为每个合约增加几分钟的时间，并为大型代码产生显著的 API 成本。微调模型或开源 LLM 可以降低成本，但它们的能力往往不如 GPT-4。目前正在进行关于用于代码安全的更小、更专业模型的研究，但目前最好的结果来自大型专有模型。

总而言之，LLM 辅助审计前景广阔，但并非万能药。 我们看到的是混合方法，其中 AI 帮助生成测试或分析特定方面，而不是端到端地完成整个审计。例如，AI 可能会建议潜在的不变量或风险区域，然后由人工或其他工具进行调查。正如一位安全工程师所说，鉴于推理差距和集成障碍，该技术尚未准备好取代人类审计员来完成关键任务。然而，它已经可以成为一个有用的助手——在传统工具不足的情况下，“不完美的东西可能比什么都没有要好得多”。

不同工具链的准确性和可靠性​

比较所讨论的各种审计方法的准确性、覆盖率和可靠性是很有启发性的。以下是来自研究和行业评估的发现摘要：

  • 静态分析工具： 像 Slither 这样的静态分析器因其快速反馈和易用性而受到重视。它们通常具有高精确率但中等召回率——这意味着它们报告的大多数问题都是真实问题（设计上误报很少），但它们只检测某些类别的漏洞。一项 2024 年的基准研究 (LLM-SmartAudit 的 RQ1) 发现，Slither 在一个测试套件中捕获了约 46% 的已知漏洞。Mythril（符号执行）表现稍好，召回率为 54%。每种工具在特定漏洞类型上都有优势（例如，Slither 非常擅长发现算术问题或 tx.origin 的使用，而符号工具则擅长发现简单的重入场景），但没有一个具有全面的覆盖率。像 Slither 这样的成熟工具的误报率相对较低——其开发者宣传*“误报最少，执行速度快（每个合约不到 1 秒）”*，使其适合在 CI 中使用。尽管如此，如果代码使用复杂的模式，静态工具可能会出错；它们可能会标记实际上已处理的边缘情况，或错过不匹配任何已知反模式的深层逻辑漏洞。

  • 模糊测试和属性测试： 像 Foundry 的模糊/不变量测试或 Trail of Bits 的 Echidna 这样的模糊测试器在发现运行时错误和不变量违规方面非常有效。这些工具的误报率几乎为零，因为如果报告了一个漏洞（断言失败），它就是一个真实的反例执行。权衡在于漏报——如果一个漏洞在测试的输入空间或运行次数内没有显现，它就可能被漏掉。覆盖率取决于模糊测试器探索状态空间的好坏。只要有足够的时间和好的启发式方法，模糊测试器已经发现了许多静态分析错过的严重漏洞。例如，Echidna 能够快速重现 MakerDAO 和 Compound 的漏洞，而这些漏洞需要形式化验证才能找到。然而，模糊测试并不能保证找到每一个逻辑错误。随着合约变得越来越复杂，模糊测试器可能需要编写额外的不变量或使用更智能的搜索策略来触及更深的状态。在指标方面，模糊测试没有一个单一的“召回率”数字，但轶事证据表明，如果重要的不变量是可破坏的，通常可以被模糊测试器破坏。它所发现的东西可靠性很高（不需要手动筛选误报），但必须记住，通过模糊测试并不等于正确性的证明——只是信心的增加。

  • 形式化验证工具： 在适用时，形式化验证提供最高的保证——一个成功的证明意味着100% 的状态都满足该属性。在准确性方面，对于它能证明的属性，它实际上是完美的（健全且完备的）。这里最大的问题不是结果的准确性，而是使用的难度和范围的狭窄。形式化工具在实践中也可能有漏报：它们可能因为复杂性而无法证明一个真实的属性（产生无结果或超时，这不是误报，但意味着我们未能验证实际上安全的东西）。它们也可能有规范错误，即工具“证明”了不是你意图的属性（用户错误）。在实际审计中，形式化方法已经捕获了一些关键漏洞（Certora 的成功案例包括在部署前捕获了一个微妙的 SushiSwap 漏洞和一个 PRBMath 库问题）。但它们的记录受限于它们被全面应用的频率——正如 Trail of Bits 指出的，“很难找到仅通过形式化验证发现的公开问题，相比之下，通过模糊测试发现的漏洞很多”。因此，虽然形式化验证在成功时非常可靠，但其对整体工具链覆盖率的影响受限于所需的精力和专业知识。

  • 基于 LLM 的分析： AI 审计器的准确性目前是一个移动的目标，因为新技术（和更新的模型）正在迅速推动其发展。我们可以收集到一些数据点：

    • AuditGPT 系统专注于 ERC 规则，实现了非常高的精确率（按误报数计算约 96%），并发现了数百个静态工具或人类忽略的问题。但这是在一个具有结构化提示词的狭窄领域。我们不应将此推广为 ChatGPT 在任意漏洞搜寻中将有 96% 的准确性——在受控设置之外，其性能较低。
    • 在更广泛的漏洞检测中，LLM-SmartAudit (GPT-3.5) 在一个基准测试中显示出约 74% 的召回率和中等的误报率，这比任何单一的传统工具都要好。当升级到带有专门提示词的 GPT-4 (TA 模式) 时，它显著改善——例如，在一组 1400 个真实世界漏洞上，GPT-4 代理找到了约 48% 的特定问题和约 47% 的复杂逻辑问题，而 Slither/Mythril/Conkas 各自找到了约 0%（无）的那些特定复杂问题。这表明 LLM 可以极大地扩展覆盖范围，涵盖静态分析完全错过的漏洞类型。另一方面，LLM 没有找到超过一半的问题（所以它也有大量的漏报），并且不清楚它报告的问题中有多少是误报——该研究更关注召回率而不是精确率。
    • Trail of Bits 的 Codex/GPT-4 “Toucan” 实验说明了可靠性问题。最初，在小例子上，Codex 可以通过仔细的提示词识别已知的漏洞（所有权问题、重入）。但一旦他们尝试扩大规模，就遇到了不一致和不正确的结果。他们报告说*“即使在平均大小的代码中，失败的次数也很高”并且难以预测。最终，他们得出结论，GPT-4（截至 2023 年初）只是一个增量改进*，并且仍然*“缺少关键功能”*，如推理跨函数流程。结果是，AI 并未显著减少他们静态工具的误报，也未能可靠地加快他们的审计工作流程。换句话说，在该试验中，专业审计员认为通用 LLM 作为审计器的当前可靠性不足。

总结一下，每个工具链都有不同的优势：

  • 静态工具： 可靠地快速检测已知问题；噪音低，但漏洞类型有限（在基准测试中召回率中等，约 40-50%）。
  • 模糊/不变量测试： 精确率非常高（几乎没有误报），并且在发现功能性和状态依赖性漏洞方面表现出色；覆盖范围可以很广，但不能保证（没有简单的度量标准，取决于时间和不变量的质量）。如果给予足够的指导，通常能找到与形式化证明相同的漏洞。
  • 形式化验证： 特定属性绝对正确性的黄金标准；如果成功应用，对于这些属性的召回率/精确率基本上是 100%。但实际上仅限于狭窄的问题，并需要大量精力（还不是一个用于全面审计的一键式解决方案）。
  • AI (LLM) 分析： 潜在的高覆盖率——可以发现跨类别的漏洞，包括其他工具错过的漏洞——但精确率可变。通过专门的设置，它可以既精确又广泛（如 AuditGPT 对 ERC 检查所示）。没有仔细的限制，它可能会撒一张大网，需要人工审查结果。ChatGPT 在漏洞检测上的“平均”准确性并不出色（在一项研究中接近猜测），但使用 LLM 的最佳工程系统正在推动性能超越传统工具。目前有积极的研究旨在使 AI 输出更值得信赖（例如，通过让多个代理交叉验证，或将 LLM 与静态推理相结合以复核 AI 的结论）。

值得注意的是，结合各种方法可以产生最佳结果。例如，可以先运行 Slither（以无噪音的方式捕获低垂的果实），然后使用 Foundry/Echidna 来模糊测试更深层次的行为，或许再使用基于 LLM 的工具来扫描任何未考虑到的模式或不变量。每种方法都会覆盖其他方法的不同盲点。

实际采用中的挑战与局限性​

在实践中，在开发工作流中采用形式化验证或 AI 工具会带来实际的挑战。一些关键问题包括：

  • 开发者体验和专业知识： 传统的形式化验证有陡峭的学习曲线。编写形式化规范（用 CVL、Coq、Move 的规范语言等）更像是编写数学证明而不是编写代码。许多开发者缺乏这方面的背景，而形式化方法专家供不应求。相比之下，使用 Foundry 进行模糊测试或用 Solidity 编写不变量要容易得多——感觉就像编写额外的测试。这是模糊测试在以太坊社区比形式化证明更快普及的一个重要原因。Trail of Bits 团队明确指出，在许多情况下，模糊测试**“产生类似的结果，但所需的技能和时间要少得多”**。因此，即使形式化验证可以捕获不同的漏洞，许多团队还是选择更简单的方法，以较低的精力获得足够好的结果。

  • 集成到开发工作流中： 一个工具要被广泛采用，它需要适应 CI/CD 管道和日常编码。像 Slither 这样的工具在这方面表现出色——它*“可以轻松集成到 CI/CD 设置中，简化自动化并帮助开发者。”* 开发者可以将 Slither 或 Mythril 添加到 GitHub Action 中，并在发现问题时使构建失败。Foundry 的模糊测试可以作为每次 forge test 的一部分运行。不变量测试甚至可以使用像 CloudExec 这样的工具在云中持续运行，任何失败都可以使用 fuzz-utils 自动转换成单元测试。这些集成意味着开发者可以获得快速反馈并进行迭代。相比之下，像 Certora Prover 这样的工具在历史上是作为单独的进程运行（或由外部审计团队运行），可能需要数小时才能产生结果——这不是你会在每次提交时都运行的东西。基于 AI 的工具也面临集成障碍：调用 API 并在 CI 中确定性地处理其输出并非易事。还有一个安全和隐私的问题——许多组织对于将专有合约代码发送到第三方 AI 服务进行分析感到不安。自托管的 LLM 解决方案目前还不如大型云 API 强大，因此这是 AI 审计器在 CI 中采用的一个症结。

  • 误报和噪音： 一个报告许多误报或低严重性发现的工具会降低开发者的信任。静态分析器过去一直受此困扰——例如，一些工具的早期版本会用警告淹没用户，其中许多是无关紧要的。信号与噪音之间的平衡至关重要。Slither 因其最少的误报而受到称赞，而像 Securify（在其研究形式中）这样的工具通常会产生许多需要手动过滤的警告。如前所述，如果不进行适当的目标定位，LLM 可能会产生噪音。这就是为什么目前 AI 的建议通常被视为建议性的，而不是绝对的。如果一个嘈杂的工具由单独的安全团队或在审计环境中使用，团队更有可能采用它，但对于日常使用，开发者更喜欢提供清晰、可操作、低噪音结果的工具。理想情况是仅在确定存在漏洞时**“使构建失败”**，而不是基于假设。实现这种可靠性是一个持续的挑战，特别是对于 AI 工具。

  • 可扩展性和性能： 形式化验证可能是计算密集型的。如前所述，求解器可能会在复杂的合约上超时。这使得它难以扩展到大型系统。如果验证一个属性需要数小时，你不会在每次代码更改时都检查几十个属性。模糊测试也面临可扩展性限制——探索巨大的状态空间或具有许多方法的合约在组合上可能会很慢（尽管在实践中，模糊测试器可以在后台或通宵运行以加深其搜索）。AI 模型有固定的上下文大小，增加模型容量是昂贵的。虽然 GPT-4 的 128k-token 上下文是一个福音，但向其提供数百 KB 的合约代码成本高昂，并且对于非常大的项目仍然不够（想象一个包含许多合约的复杂协议——你可能会超过这个限制）。还有一个多链扩展的问题：如果你的项目涉及不同链上合约之间的交互（以太坊 ↔ 另一条链），验证或分析这种跨链逻辑更加复杂，并且可能超出了当前工具的能力。

  • 人工监督和验证： 归根结底，大多数团队仍然依赖专家级的人类审计员进行最终签核。自动化工具是辅助工具，而不是替代品。所有这些工具的一个局限性是它们在已知属性或模式的范围内操作。它们可能会错过一种全新的漏洞类型或 DeFi 协议设计中微妙的经济缺陷。人类审计员利用直觉和经验来思考攻击者可能如何接近系统，有时是以任何工具都没有明确编程的方式。有些情况下，合约通过了所有自动化检查，但后来有人在业务逻辑或创造性的攻击向量中发现了漏洞。因此，一个挑战是避免产生虚假的安全感——开发者必须正确解释形式化工具和 AI 的输出，而不是假设“未发现问题”就意味着代码 100% 安全。

  • 维护规范和测试： 特别是对于形式化验证，一个实际问题是规范漂移。随着代码的演变，规范（不变量、规则等）可能会过时。确保代码及其形式化规范保持同步是一项不小的管理任务。如果开发者不警惕，证明可能会“通过”，仅仅因为它们证明的东西与代码的实际需求不再相关。同样，随着系统预期行为的变化，不变量测试也必须更新。这需要一种并非所有团队都具备的、以不变量驱动的开发文化（尽管正在推动鼓励这种文化）。

总而言之，主要的限制是人和流程，而不是技术的原始能力。形式化和 AI 辅助方法可以极大地提高安全性，但它们必须以适合开发者工作流程和技能集的方式部署。令人鼓舞的是，像不变量驱动开发（从第一天起就写下关键不变量）这样的趋势正在获得关注，并且工具正在慢慢改进，使高级分析更加即插即用。主要工具的开源（例如 Certora Prover）和模糊测试集成到流行框架（Foundry）正在降低门槛。随着时间的推移，我们期望在使用这些强大的验证技术方面，“普通开发者”能做的和“博士研究员”能做的之间的差距将会缩小。

开源与商业审计工具​

智能合约安全工具的领域包括开源项目和商业服务。两者各有其角色，并且常常互为补充：

  • 开源工具： 以太坊生态系统中大多数广泛使用的审计工具都是开源的。这包括 Slither（静态分析器）、Mythril（符号执行）、Echidna（模糊测试器）、Manticore（符号/混合执行）、Securify（来自苏黎世联邦理工学院的分析器）、Solhint/Ethlint（linter），当然还有 Foundry 本身。开源工具受到青睐有几个原因：（1）透明度——开发者可以看到工具如何工作，并相信没有恶意或隐藏的东西发生（这在一个开放的生态系统中很重要）。（2）社区贡献——规则和功能由广泛的社区添加（例如，Slither 有许多社区贡献的检测器）。（3）成本——它们是免费使用的，这对于 Web3 中许多小型项目/初创公司很重要。（4）集成——开源工具通常可以在本地或 CI 中运行，没有法律障碍，并且通常可以为项目特定需求进行定制或编写脚本。

    开源工具发展迅速。例如，Slither 对新 Solidity 版本和模式的支持由 Trail of Bits 持续更新。由 ConsenSys 开发的 Mythril 不仅可以分析以太坊，还可以通过处理字节码来分析任何 EVM 兼容链——这展示了开源工具如何轻松地跨链重用。开源工具的缺点是它们通常带有*“使用风险自负”*的声明——没有官方支持或保证。它们可能无法扩展或没有商业产品 UI 的精美。但在区块链领域，即使是许多公司也在内部使用开源作为其核心工具（有时会进行轻微的自定义修改）。

  • 商业服务和工具： 一些公司将安全分析作为产品提供。例子包括 MythX（ConsenSys Diligence 的基于云的扫描 API）、Certora（在开源之前将其证明器作为服务提供）、CertiK 和 SlowMist（这些公司拥有内部扫描器和 AI，用于审计或通过仪表板提供），以及一些新进入者，如来自 ChainSecurity 的 Securify（该公司被收购，其工具在内部使用）或 SolidityScan（一个输出审计报告的云扫描器）。商业工具通常旨在提供更用户友好的体验或集成服务。例如，MythX 与 IDE 扩展和 CI 插件集成，以便开发者可以将他们的合约发送到 MythX 并获得详细的报告，包括漏洞评分和修复细节。这些服务通常在后台运行多种分析技术的组合（模式匹配、符号执行等），并经过调整以最小化误报。

    商业工具的价值主张通常是便利性和支持。它们可能会维护一个持续更新的漏洞知识库，并提供客户支持来解释结果。它们也可能在云中处理繁重的计算（这样你就不需要在本地运行求解器）。然而，成本是一个因素——鉴于有免费的替代品，许多项目选择不为这些服务付费。此外，本着去中心化的精神，一些开发者对依赖闭源服务来保障安全持保留态度（“验证，而不是信任”的理念）。Certora Prover 在 2025 年的开源是一个值得注意的事件：它将一个高端商业工具变成了社区资源。此举预计将加速其采用，因为现在任何人都可以尝试在没有付费许可的情况下形式化验证他们的合约，并且代码的开放性将允许研究人员改进该工具或将其应用于其他链。

  • 人工审计服务： 值得一提的是，除了软件工具，许多审计是由专业公司（Trail of Bits、OpenZeppelin、Certik、PeckShield 等）完成的。这些公司使用上述工具（主要是开源的）和专有脚本的混合。这些工作的产出通常是保密的，或仅在审计报告中进行总结。这里并不完全是“开源与商业”的二分法，因为即使是商业审计公司也严重依赖开源工具。区别更多在于专业知识和手动工作。话虽如此，一些公司正在开发专有的 AI 辅助审计平台，以给自己带来优势（例如，有报道称*“ChainGPT”被用于内部审计，或 CertiK 开发了一个名为Skynet*的 AI 用于链上监控）。这些本身不是公共工具，因此它们的准确性和方法没有被广泛记录。

在实践中，一种常见的模式是开源优先，商业可选。团队在开发和测试期间会使用开源工具（因为它们可以轻松集成并根据需要频繁运行）。然后，他们可能会在部署前使用一两个商业服务作为额外的检查——例如，运行一次 MythX 扫描以获得“第二意见”，或聘请一家使用像 Certora 这样的高级工具来形式化验证关键组件的公司。随着界限变得模糊（Certora 开源，MythX 的结果经常与开源工具重叠），区别更多地在于支持和便利性，而不是能力。

一个值得注意的交叉点是 Certora 的多链支持——通过正式支持 Solana 和 Stellar，他们解决了在这些平台上开源替代品较少的问题（例如，以太坊有许多开源工具，而 Solana 直到最近几乎没有）。随着安全工具扩展到新的生态系统，我们可能会看到更多的商业产品填补空白，至少在开源赶上之前是这样。

最后，值得注意的是，开源与商业在这里并非对立关系；它们常常相互学习。例如，在学术/商业工具中开创的技术（如 Securify 中使用的抽象解释）最终会进入开源工具，反之，来自开源工具使用的数据可以指导商业工具的改进。双方追求的最终结果是为整个生态系统提供更好的安全性。

跨链适用性​

虽然以太坊一直是大多数这些工具的焦点（鉴于其在智能合约活动中的主导地位），但形式化验证和 AI 辅助审计的概念也适用于其他区块链平台。以下是它们如何应用的：

  • EVM 兼容链： 像 BSC、Polygon、Avalanche C-Chain 等使用以太坊虚拟机 (EVM) 的区块链，可以直接使用所有相同的工具。模糊测试或静态分析不关心你的合约是部署在以太坊主网上还是 Polygon 上——字节码和源语言（Solidity/Vyper）是相同的。实际上，Mythril 和 Slither 可以通过从地址拉取字节码来分析任何 EVM 链的合约（Mythril 只需要一个 RPC 端点）。这些链上的许多 DeFi 项目运行 Slither 和 Echidna 的方式与以太坊项目完全相同。对 BSC 或 Avalanche 上协议的审计通常使用与以太坊审计相同的工具包。因此，在 EVM 环境中，跨链主要意味着重用以太坊的工具链。

  • Solana： Solana 的智能合约是用 Rust 编写的（通常通过 Anchor 框架），并在 BPF 虚拟机上运行。这与以太坊的环境非常不同，所以以太坊特定的工具无法直接使用。然而，同样的原则适用。例如，可以使用 Rust 的原生模糊测试库或像 cargo-fuzz 这样的工具对 Solana 程序进行模糊测试。直到最近，Solana 上的形式化验证几乎不存在。Certora 和 Solana 工程师之间的合作为 Solana 程序产生了一个内部验证工具，可以根据规范证明 Rust/Anchor 合约。如前所述，Certora 将其证明器扩展到了 Solana 的 VM，这意味着开发者可以像为 Solidity 那样编写关于 Solana 程序行为的规则并进行检查。这很重要，因为 Solana 的快速发展方式意味着许多合约在没有经过以太坊那种严格测试的情况下就启动了；形式化工具可以改善这一点。对 Solana 的 AI 审计也是可行的——一个理解 Rust 的 LLM 可以被提示检查 Solana 程序的漏洞（如缺少所有权检查或算术错误）。它可能需要针对 Solana 特定的模式进行微调，但鉴于 Rust 的流行度，GPT-4 在阅读 Rust 代码方面相当熟练。我们可能很快就会看到类似“ChatGPT for Anchor”的工具出现。

  • Polkadot 和基于 Substrate 的链： Polkadot 的智能合约可以用 Rust 编写（编译成 WebAssembly），使用 ink! 框架，或者你可以运行一个 EVM pallet（就像 Moonbeam 那样），这再次允许使用 Solidity。在 ink!/Wasm 的情况下，验证工具仍处于起步阶段。可以尝试使用通用的 Wasm 验证框架来形式化验证 Wasm 合约的属性（例如，微软的 Project Verona 或其他项目已经研究了 Wasm 的安全性）。Certora 的开源证明器也提到了对 Stellar 的 WASM 智能合约的支持，这在概念上与任何基于 Wasm 的链相似。因此，它很可能也适用于 Polkadot 的 Wasm 合约。对 ink! 合约进行模糊测试可以通过编写 Rust 测试来完成（Rust 中的属性测试可以起到类似的作用）。对 ink! 合约的 AI 审计也需要分析 Rust 代码，这同样是 LLM 在有正确上下文的情况下可以做到的（尽管它可能在没有一些提示的情况下不知道特定的 ink! 宏或 trait）。

    此外，Polkadot 正在探索使用 Move 语言进行并行智能合约开发（正如一些社区论坛所暗示的）。如果 Move 在 Polkadot 平行链上被使用，Move Prover 就会随之而来，从设计上就带来了形式化验证能力。Move 对安全性的强调（面向资源的编程）和内置的证明器展示了形式化方法从一开始就在跨链传播。

  • 其他区块链： 像 Tezos（Michelson 智能合约）和 Algorand（TEAL 程序）这样的平台各自都有形式化验证的努力。例如，Tezos 有一个名为 Mi-Cho-Coq 的工具，它提供了 Michelson 的形式化语义并允许证明属性。这些更多是学术性的，但表明任何具有明确定义的合约语义的区块链都可以进行形式化验证。原则上，AI 审计可以应用于任何编程语言——这只是一个适当地训练或提示 LLM 的问题。对于不太常见的语言，LLM 可能需要一些微调才能有效，因为它可能没有在足够多的例子上进行预训练。

  • 跨链交互： 一个新的挑战是验证跨链的交互（如桥接或链间消息传递）。这里的形式化验证可能涉及对多个链的状态和通信协议进行建模。这非常复杂，目前超出了大多数工具的能力，尽管特定的桥接协议已经过手动安全分析。AI 可能有助于审查跨链代码（例如，审查一个与 Cosmos 上的 IBC 协议交互的 Solidity 合约），但目前还没有现成的解决方案。

本质上，以太坊的工具为其他链铺平了道路。许多开源工具正在被改造：例如，有努力创建一个类似 Slither 的 Solana (Rust) 静态分析器，而不变量测试的概念是语言无关的（基于属性的测试存在于许多语言中）。强大引擎的开源（如 Certora 的多 VM 引擎）对于跨链安全尤其有前途——同一个平台可以用来验证 Solidity 合约、Solana 程序和 Move 合约，只要每个都有适当的规范编写。这鼓励了整个行业更统一的安全态势。

还值得注意的是，AI 辅助审计将使所有链受益，因为模型可以被教导关于任何上下文中的漏洞。只要向 AI 提供正确的信息（语言规范、该生态系统中的已知漏洞模式），它就可以应用类似的推理。例如，可以要求 ChatGPT 用适当的提示词审计一个 Solidity 合约或一个 Move 模块，它两者都能做到——如果它有这个概念，它甚至可能捕获到类似*“这个 Move 模块可能违反了资源守恒”*的问题。限制在于 AI 是否接触到了足够多的该链的训练数据。以太坊作为最受欢迎的链，很可能使模型偏向于最擅长 Solidity。随着其他链的增长，未来的 LLM 或微调的衍生品也可以覆盖这些。

结论​

智能合约形式化验证与 AI 辅助审计是一个快速发展的领域。我们现在拥有一个丰富的工具包：从提高代码可靠性的确定性静态分析器和模糊测试框架，到能够以类似人类的方式推理代码的前沿 AI。形式化验证，曾是一个小众的学术追求，正通过更好的工具和集成变得更加实用。AI，尽管目前存在局限性，但在自动化安全分析方面已经展现出改变游戏规则的能力的曙光。

目前还没有一刀切的解决方案——现实世界的审计结合了多种技术以实现纵深防御。Foundry 的模糊测试和不变量测试已经提高了部署前的期望标准（捕获了许多会绕过基本测试的错误）。AI 辅助审计，如果谨慎使用，可以作为审计员的力量倍增器，以手动审查无法比拟的规模和速度突出问题并验证合规性。然而，人类的专业知识对于驱动这些工具、解释它们的发现以及定义要检查的正确属性仍然至关重要。

展望未来，我们可以期待这些方法的更大程度的融合。例如，AI 可能帮助编写形式化规范或建议不变量（“AI，这个 DeFi 合约应该遵守哪些安全属性？”）。模糊测试工具可能会结合 AI 来更智能地引导输入生成（正如 PromFuzz 所做的那样）。形式化验证引擎可能会使用机器学习来决定应用哪些引理或启发式方法。所有这些都将有助于在不仅是以太坊，而且是所有区块链平台上构建更安全的智能合约。最终的愿景是，未来关键的智能合约可以在对其正确性有高度信心的情况下部署——这个目标很可能通过形式化方法和 AI 辅助的协同使用来实现，而不是单独依赖任何一种。

来源：

  • Foundry 模糊测试和不变量测试概述
  • Trail of Bits 关于模糊测试与形式化验证的论述
  • Trail of Bits 关于形式化验证局限性的论述
  • Patrick Collins 关于模糊/不变量测试与形式化方法的比较
  • Trail of Bits 关于审计中不变量的论述
  • Medium (BuildBear) 关于 Slither 和 Mythril 的使用
  • AuditGPT 结果（ERC 合规性）
  • Trail of Bits 关于 LLM (Codex/GPT-4) 局限性的论述
  • LLM-SmartAudit 与传统工具的性能比较
  • “Detection Made Easy” 关于 ChatGPT 准确性的研究
  • PromFuzz (LLM+模糊测试) 性能
  • Certora 开源公告（多链）
  • Move Prover 描述 (Aptos)
  • 静态分析背景（智能合约安全文献）
Share on Twitter