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

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

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

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

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

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

成功创建开发者喜爱的LLM集成体验的人将为他们的平台创造一道不可思议的护城河。

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

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

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

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

我们如何构建框架

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

提示框架

如果今天我们制作Toucan，我们可能只会使用LangChain。但当时，LangChain没有我们需要的功能。令人沮丧的是，OpenAI和Microsoft都没有提供官方的、第一方的提示框架。这导致我们开发了一个自定义框架，目标是审计员可以创建新提示而无需修改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端点来妥协客户数据。我们有一个严格的政策，只对GitHub上的开源项目（这些项目可能已经被Codex索引）运行Toucan，并带有已发布的报告，如我们出版物页面上的那些。

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

缺失的工具

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

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

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

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

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

总体而言，工具生态系统缺乏，令人惊讶的是，该领域最大的名字没有发布任何实质性内容来改善LLM采用和集成到人们使用的真实软件项目中。然而，我们兴奋地看到开源社区正在挺身而出，推出了像LangChain和LlamaIndex这样非常酷的项目。

人类仍然至高无上

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

尽管Codex（和GPT-4）目前无法与成熟的基于算法的工具相匹配，但基于LLM的工具——即使是质量较低的工具——可能具有有趣的用途。对于没有分析工具的语言，开发者可以相对快速地