Codex（及GPT-4）在智能合约审计中无法超越人类 - The Trail of Bits博客

Artem Dinaburg, Josselin Feist, Riccardo Schirone
2023年3月22日
区块链, 机器学习

人工智能（AI）能否驱动软件安全审计？在过去四个月中，我们试点了一个名为Toucan的项目来寻找答案。Toucan旨在将OpenAI的Codex集成到我们的Solidity审计工作流中。这个实验远不止在提示中写“漏洞在哪里？”并期望得到完整结果。

我们的多功能团队（包括审计员、开发人员和机器学习专家）在提示工程上投入了大量工作，并开发了一个自定义提示框架，以应对当前大型语言模型（LLM）工具的一些挫折和限制，例如处理不正确和不一致的结果、处理速率限制以及创建复杂的模板化提示链。在每个步骤中，我们都评估了Toucan的有效性，以及它是否会提高审计员的效率或因误报而减慢他们的速度。

该技术尚未准备好用于安全审计，主要有三个原因：

1. 模型无法很好地推理某些高级概念，例如合约所有权、重入和费用分配。
2. 将大型语言模型与传统软件集成的软件生态系统过于粗糙，一切都很繁琐；几乎没有面向开发者的工具、库和类型系统来处理不确定性。
3. 缺乏用于提示创建开发和调试工具。要开发将核心LLM技术与传统软件集成的库、语言功能和工具，需要更多资源。

成功创建开发者喜爱的LLM集成体验的人将为他们的平台创造巨大的护城河。

上述批评同样适用于GPT-4。尽管它在此博客文章发布前几天才发布，但我们通过ChatGPT界面手动运行了一些实验。我们得出结论，GPT-4在分析Solidity代码方面有渐进式改进。虽然GPT-4在分析Solidity方面比GPT-3.5（ChatGPT）好得多，但它仍然缺少关键功能，例如推理跨函数重入和函数间关系的能力。与Codex相比，它还存在一些能力退化，例如变量识别、算术表达式和理解整数溢出。通过适当的提示和上下文，GPT-4最终可能能够推理这些概念。我们期待在大型上下文GPT-4模型的API访问发布后进行更多实验。

我们仍然对Codex和类似LLM所能提供的功能感到兴奋：可以用相对较少的努力引导的分析能力。虽然它无法与优秀算法工具的保真度相匹配，但在没有代码分析工具的情况下，不完美的东西可能比什么都没有好得多。

Toucan是我们使用LLM进行软件安全的首次实验之一。我们将继续研究基于AI的工具，将其集成到我们的工作流中，例如为审计中的智能合约自动生成文档。基于AI的能力在不断改进，我们渴望尝试更新、更强大的技术。

我们也想要AI工具

由于我们喜欢研究变革性和颠覆性技术，我们评估了OpenAI的Codex用于一些内部分析和转换任务，并对其能力印象深刻。例如，最近一位实习生将Codex集成到Ghidra中，将其用作反编译器。这启发了我们，鉴于我们在工具开发和智能合约评估方面的专业知识，看看Codex是否可以应用于审计Solidity智能合约。

审计区块链代码是一项需要时间培养的技能（这就是我们提供学徒制的原因）。一个好的审计员必须综合来自不同领域的多个见解，包括金融、语言、虚拟机内部、ABI的细微差别、常用库以及与价格预言机等复杂交互。他们还必须现实的时间限制下工作，因此效率是关键。

我们希望Toucan通过增加人类审计员可以调查的代码量和分析深度来使他们更好。我们特别兴奋，因为基于AI的工具有可能从根本上优于传统的基于算法的工具：可以学习不可判定问题到任意高精度，而程序分析总是遇到不可判定性。

我们最初想看看Codex是否可以分析代码中的高级问题，这些问题无法通过静态分析检查。不幸的是，Codex没有提供令人满意的结果，因为它无法推理高级概念，尽管它可以用文字解释和描述它们。

然后我们转向另一个问题：我们能否使用Codex来降低静态分析工具的误报率？毕竟，LLM与我们现有工具 fundamentally不同。也许它们提供了足够的信号来创建以前由于不可接受的误报而无法实现的新分析。再次，答案是否定的，因为即使在平均大小的代码中，失败的数量也很高，而且这些失败难以预测和表征。

下面我们将讨论我们实际构建的内容以及如何评估Toucan的能力。

这值得我们的时间吗？

我们的评估不符合科学研究的严谨性，不应被视为如此。我们试图在评估中经验性和数据驱动，但我们的目标是决定Toucan是否值得进一步开发努力——而不是科学发表。

在Toucan开发的每个阶段，我们都试图评估我们是否在正确的轨道上。在开始开发之前，我们手动使用Codex来识别人类在特定开源合约中发现的漏洞——通过足够的提示工程，Codex可以做到。

在我们有能力尝试小例子后，我们专注于三个似乎 within Codex能力理解的主要概念：所有权、重入和整数溢出。（给精明读者的快速说明：Solidity 0.8修复了大多数整数溢出问题；开发溢出检查是评估Codex对过去代码能力的一项练习。）我们可以相当成功地识别小规模、专门制作的例子中这些概念的漏洞。

最后，当我们创建了足够的工具来自动化对多个较大合约的提问时，我们开始看到误报和幻觉率变得太高。尽管我们通过更复杂的提示取得了一些成功，但这仍然不足以使Toucan可行。

以下是我们经验中的一些关键要点。

• Codex没有完全掌握我们想询问的高级概念，通过复杂的提示工程解释它们并不总是有效或产生可靠的结果。我们最初打算询问关于高级概念的问题，如所有权、重入、费用分配、价格预言机的使用，甚至自动做市商（AMMs）。Codex没有完全理解许多这些抽象概念，询问它们在初始评估阶段失败了。它 somewhat理解最简单的概念——所有权——但即使如此，它 often无法总是将“owner”变量的变化与所有权概念关联起来。Codex似乎没有掌握重入攻击作为一个概念，尽管它可以用自然语言句子描述它们。
• 通过p-hacking一个适用于一个或几个例子的提示来欺骗自己非常容易。获得一个在多个、多样化输入上泛化得很好的提示 extremely困难。例如，当测试Toucan是否可以推理所有权时，我们最初尝试了七个小（<50 LOC）例子，从中我们可以确定基线。经过 thorough提示工程努力，Toucan可以通过七分之六的测试，唯一失败的测试需要复杂逻辑来诱导所有权变化。然后我们在八个较大程序（> 300 LOC）上尝试了相同的提示，其中Toucan识别了15个潜在的所有权变化，有四个误报——包括完全幻觉。然而，当我们尝试原始小测试的轻微排列时，我们通常可以使提示在输入相对较小的变化下失败。类似地，对于整数溢出测试，我们可以让Toucan成功识别11个小例子中的10个溢出，有一个误报——但一组较大的五个合约产生了12个阳性——其中六个是假的，包括四个完全幻觉或无法遵循指示的实例。
• Codex很容易被语法的微小变化误导。Codex不如现有静态分析工具精确。它很容易被注释、变量名和小的语法变化混淆。一个特别的痛点是推理条件（例如==, !=, <, >），Codex似乎会忽略它们，而是根据函数和变量名创建结论。
• Codex擅长难以算法定义的抽象任务， especially如果输出中的错误是可接受的。例如，Codex将擅长查询如“此合约中哪些函数操作全局状态？”而无需定义“全局状态”或“操作”。结果可能不精确，但它们通常足够好以实验新的分析想法。虽然可以算法定义这样的查询，但用普通语言询问 infinitely更容易。
• Codex的失败模式不容易预测，但它们与Slither和 likely基于传统算法的类似静态分析工具不同。

图1：Slither、Toucan和两者在一些简单重入测试中发现的真阳性（绿色）和假阳性（红色）。Toucan的结果不令人鼓舞。

我们尝试查看Slither和Toucan的真/假阳性集，发现每个工具都有不同的假阳性/假阴性集，有一些重叠（图1）。Codex无法有效降低原型Slither整数溢出检测器的误报率。总体而言，我们注意到一种 tendency肯定地回答我们的问题，增加了Toucan发现的阳性数量。

Codex可以执行基本的静态分析任务，但失败率太高而无法有用，且太难以表征。这种成功进行分析的能力，即使在短程序片段上，也非常令人印象深刻，不应被低估！对于Codex理解但没有合适工具的语言，这种能力可能 extremely有价值——毕竟，一些分析可能比什么都没有好得多。但Solidity的基准不是什么都没有；我们已经有了 existing静态分析工具，工作得很好。

我们如何构建框架

在Toucan开发期间，我们创建了一个自定义提示框架、一个基于Web的前端以及基本的调试和测试工具来评估提示并帮助单元和集成测试。其中最重要的是提示框架。

提示框架

如果我们今天制作Toucan，我们可能会 just使用LangChain。但当时，LangChain没有我们需要的功能。令人沮丧的是，OpenAI和Microsoft都没有提供官方的、第一方提示框架。这导致我们开发了一个自定义框架，目标是审计员可以创建新提示而无需 ever修改Toucan的代码。

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29

requires = [“emit-ownership-doc”, “emit-target-contract”,]
name = “Contract Ownership”
scope = “contract”
instantiation_condition = “any(‘admin’ in s.name.lower() or ‘owner’ in s.name.lower() for s in contract.state_variables)”

[[questions]]
name = “can-change”
query = “Is it possible to change the `{{ contract | owner_variable }}` variable by calling a function in the `{{ contract.name }}` contract without aborting the transaction? Think through it step by step, and answer as ‘Yes’, ‘No’, or ‘Unknown’. If ‘Yes’, please specify the function.”
is_decision = true

[[questions]]
name = “who-can-call”
runtime_condition = “questions[‘can-change’].is_affirmative()”
query = “””
To reason about ownership:
1) First, carefully consider the code of the function
2) Second, reason step by step about the question.
Who can call the function successfully, that is, without aborting or revering the transaction?
“””
answer_start = “””
1) First, carefully consider the code of the function:
“””

[[questions]]
name = “can-non-owner-call”
runtime_condition = “questions[‘can-change’].is_affirmative()”
query = “Can any sender who is not the current owner call the function without reverting or aborting?”
is_decision = true
finding_condition = “question.is_affirmative()”

图2：询问合约所有权的示例问题链。在问题发出之前，提示框架还发出关于所有权含义的具体解释，包括示例和目标合约信息。

我们的框架支持将多个问题链接在一起以支持思维链和类似提示技术（图2）。由于像Codex这样的GPT模型是多 shot学习者，我们的框架还支持在形成提示之前添加背景信息和示例。

框架还支持按问题过滤，因为可能有些问题仅与特定类型的合约相关（例如，仅ERC-20代币），而其他问题可能有特定范围（例如，合约、函数或文件范围）。最后，每个问题可以可选地路由到不同的模型。

提示框架还尽力遵守OpenAI的API限制，包括将问题批处理到一个API调用中，并跟踪令牌计数和API调用速率限制。我们经常遇到这些限制，并非常感激Codex模型在测试期间是免费的。

测试数据

我们的开发目标之一是我们永远不会通过将客户数据发送到OpenAI API端点来 compromise客户数据。我们有一个严格的政策，只对GitHub上的开源项目（这些项目可能已经被Codex索引）运行Toucan，并带有已发布的报告，例如我们出版物页面上的那些。

我们还能够使用Slither附带的相当广泛的测试集，以及我们的“构建安全合约”参考资料作为 additional测试数据。需要注意的是，其中一些测试和参考资料可能是Codex训练集的一部分，这解释了为什么我们在较小的测试用例上看到了非常好的结果。

缺失的工具

OpenAI和Microsoft都缺乏工具，这 extremely令人失望，尽管这看起来正在改变：Microsoft有一个提示库，OpenAI最近发布了OpenAI Evals。我们希望能看到的工具类型包括提示调试器；提示和响应中令牌的树图可视化，带有每个令牌的logprobs；用于针对大规模数据集测试提示以评估质量的工具；询问相同问题并结合反例结果的方法；以及一些常见单元测试框架的插件。肯定有人在为开发者着想并制作这些工具？

当前编程语言缺乏与神经架构计算机（如LLM或类似模型）接口的设施。一个核心问题是缺乏处理非确定性和不确定性的能力。当使用LLM时，每个答案都有一些内置的不确定性：输出本质上是概率性的，不是离散量。这种不确定性应该在类型系统级别处理，以便在必要时才必须显式处理概率。Microsoft Research的一个开创性项目Infer.NET为基于.NET的语言做到了这一点，但似乎很少有具体例子和没有真正的工具将其与LLM结合。

提示工程和 surrounding工具仍处于起步阶段。最大的问题是你永远不知道何时完成：即使现在，我们总是可能只差一两个提示就能使Toucan成功。但在某个时刻，你必须在成本和时间表面前放弃。考虑到这一点，30万美元的薪水给一个 fantastic提示工程师似乎并不荒谬：如果成功LLM部署和失败之间的唯一区别是几个提示，这份工作很快就能收回成本。但 fundamentally，这反映了缺乏评估提示质量和评估响应的工具。

没有特别好的方法来确定一个提示是否比另一个更好，或者你是否在正确的轨道上。类似地，当提示对输入失败时， frustratingly难以找出原因，并以编程方式确定哪些提示 merely返回错误结果 versus完全幻觉和行为不当。

单元测试也有问题；结果不能保证在运行之间相同， newer模型可能不提供与先前模型相同的结果。肯定有解决方案，但 again，开发者期望的工具 just不存在。OpenAI Evals likely将改善这种情况。

总体而言，工具生态系统缺乏，且 surprisingly，该领域最大的名字没有发布任何实质性内容来改善LLM采用和集成到人们使用的真实软件项目中。然而，我们兴奋地看到开源社区正在 stepping up with really酷的项目，如LangChain和LlamaIndex。

人类仍然至高无上

OpenAI的Codex尚未准备好接管软件安全审计员的工作。它缺乏推理适当概念的能力，并在审计任务中产生太多误报以供实际使用。然而， clearly有一个 nascent能力来执行有趣的分析任务， underlying模型应该 quickly变得更 capable。我们非常兴奋地继续使用该技术，随着它的改进。例如，GPT-4的新 larger上下文窗口可能允许我们提供足够的上下文和方向来处理复杂任务。

尽管Codex（和GPT-4）目前无法与成熟的基于算法的工具相匹配，基于LLM的工具——即使是质量较低的工具——可能有有趣的用途。对于没有分析工具的语言，开发者可以相对 quickly从LLM引导一些东西。在以前没有分析的地方提供一些合理分析的能力可能 considerably比什么都没有好。

我们希望将语言模型集成到现有程序中的能力 quickly改善，因为目前严重缺乏语言、库、类型系统和其他工具用于将LLM集成到传统软件中。令人失望的是，发布LLM的主要组织没有发布太多工具来启用它们的使用。幸运的是，开源项目正在填补空白。仍然有巨大的工作要做， whoever能制作出与LLM合作的 wonderful开发者体验 stands to capture开发者心智份额。

LLM能力正在 rapidly改善，如果继续，下一代LLM可能作为安全审计员的有能力助手。在开发Toucan之前，我们使用Codex参加了一个内部区块链评估，偶尔用于招聘。它没有通过——但如果它是一个候选人，我们会要求它花一些时间发展技能并在几个月后返回。它确实返回了——我们让GPT-4参加相同的评估——它仍然没有通过，尽管它做得更好。也许具有适当提示的大型上下文窗口版本可以通过我们的评估。我们非常渴望找出答案！

如果你喜欢这篇文章，分享它： Twitter LinkedIn GitHub Mastodon Hacker News

页面内容 我们也想要AI工具 这值得我们的时间吗？ 我们如何构建框架 提示框架 测试数据 缺失的工具 人类仍然至高无上 最近的帖子 构建安全消息传递很难：对Bitchat安全辩论的 nuanced看法 用Deptective调查你的依赖项 系好安全带，Buttercup，AIxCC的评分回合正在进行中！ 使你的智能合约成熟 beyond私钥风险 Go解析器中意外的安全陷阱 © 2025 Trail of Bits。 使用Hugo和Mainroad主题生成。