将 Solidity语义转化为结构化自然语言，而非直接分析代码，可能会是 AI 智能合约审计更好的方式。
论点（Thesis）
大型语言模型（LLMs）的训练基础主要是自然语言，而非形式化的编程语义。然而，目前大多数AI审计方法仍要求它们直接对原始Solidity代码进行推理。
这里提出一个简单的论点：将智能合约的语义转化为结构化的自然语言表示，可以使大型语言模型更容易检测到漏洞。
我们不再要求LLM去理解语法繁重的Solidity代码，而是将代码转换为一种语义叙述，明确地捕捉以下要素：
- 行为者（actors）
- 状态变化（state changes）
- 授权谓词（authorization predicates）
- 外部交互（external interactions）
- 顺序关系（ordering relationships）
- 攻击者可控窗口（attacker-controlled windows）
然后，我们要求模型分析这种表示，以发现其中的逻辑矛盾、缺失的前提条件以及不安全的行为。
其关键假设在于，当程序的语义以LLMs最熟悉的领域——即自然语言——来表达时，它们的推理会更可靠。
启发（Inspiration）
这个概念上的灵感，来源于道格拉斯·霍夫施塔特（Douglas Hofstadter）的《哥德尔、埃舍尔、巴赫》。书中反复出现的一个主题是“同构性”：两个系统即使看起来完全不同，也可以共享相同的底层结构。
书中的例子包括：
不同的表现形式，相同的核心结构。
这引出了一个有趣的问题：如果智能合约代码能够被翻译成另一种符号系统——自然语言——同时完全保留其语义，会怎样？
换句话说，Solidity程序和结构化的自然语言系统描述，可以成为相同底层逻辑的同构表示。如果这种映射足够准确，那么程序中的错误就应该表现为叙述中的逻辑不一致。
方法（The Method）
我所实验的方法大致遵循以下流程：
Solidity → 语义提取 → 结构化英语表示 → LLM推理 → 潜在漏洞。
这种结构化表示不仅仅是注释文档。它明确地描述了：
- 守卫条件（执行所需的条件）
- 状态读取（state reads）
- 状态写入（state writes）
- 外部交互（external interactions）
- 执行顺序（execution ordering）
- 重入窗口（reentrancy windows）
- 行为者关系（actor relationships）
例如，一段Solidity代码序列：
token.transfer(msg.sender, amount);
balances[msg.sender] -= amount;
可以被翻译成语义表示，例如：
- 交互：合约将代币转账给调用者。
- 效果：调用者的记录余额减少。
- 顺序：转移发生在余额更新之前。
- 控制转移：外部代码可能在转移期间执行。
在这种形式下，模型无需从复杂的语法中推断语义。因果关系已经一目了然。
为什么这可能有效（Why This Might Work）
大多数智能合约漏洞并非语法错误。它们是语义上的不一致，例如：
- 授权谓词应用于错误的执行者
- 状态更新发生在攻击者可控的交互之后
- 记账变量与实际余额不符
- 预言机数值被假定为最新，但可能已过时
- 生命周期转换发生在无效阶段
这些本质上都是对逻辑规则的违反。
而LLMs非常擅长检测矛盾、缺失的假设、因果不一致和叙述上的不连贯。因此，与其要求模型先解析Solidity语法再自行恢复语义，不如直接以它们擅长的语言形式呈现语义。
早期实验（Early Experiments）
为了快速验证这个想法，我进行了一个非常简单的实验。
设置：
- 模型：GPT-4o
- 提示：一个简单的“查找漏洞”提示
- 比较：原始Solidity代码 与 相同代码的结构化英语表示。
测试案例（Test Case）
我在Code4rena Thor Wallet代码库上进行了测试，该代码库有公开记录的发现。
在相同的提示下：
- 原始代码分析检测到3个已确认的高危问题中的1个，以及1个已确认的低危问题。
- 结构化英语分析检测到3个已确认的高危问题中的3个，以及许多已确认的低危/质量问题。
在包含义务规则的其他测试中，两种表示都能检测到问题，但英语版本产生了更清晰的因果解释。
这些仍然是小型实验，但结果表明表示方式的改变可能确实很重要。
为什么表示方式很重要（Why the Representation Matters）
原始Solidity代码包含大量的语法噪音。模型必须费力地从中恢复语义关系，例如：
- 哪个状态变量代表授权？
- 该授权何时被消耗？
- 哪些交互将控制权转移给不受信任的代码？
- 哪些假设在攻击者可控窗口中持续存在？
结构化英语直接消除了这种负担，将语义关系暴露在表面。这种差异类似于比较机器码和源代码。底层计算是相同的，但一种表示方式显然更易于人类（以及在此场景下的AI）进行推理。这本质上是一个信息呈现的优化问题。
影响（Implications）
如果这个想法能够扩展，它将预示着AI审计工具架构的一种新思路。
我们不再将LLM直接与原始代码耦合，而是可以构建一个包含以下管道的系统：
代码 → 语义图 → 受控自然语言表示 → LLM推理 → 验证器循环。
在这种设计中，LLM成为纯粹的语义推理引擎，而非兼任代码解析器。
潜在的好处包括：
- 改进对语义漏洞的检测
- 生成更清晰的漏洞解释
- 更好的推理过程可追溯性
- 更容易与形式化验证、不变式检查等工具集成
下一步（What’s Next）
目前的原型仍处于非常早期阶段。接下来的步骤包括：
更大规模的评估（Larger Evaluation）
在CodeHawks First Flights、Code4rena竞赛以及ScaBench等基准数据集上进行测试，以验证这种表示方法的优势是否适用于更多样、更复杂的合约。
更好的语义表示（Better Semantic Representation）
当前版本仍然偏向描述性。更强大的版本将包括：
- 显式谓词
- 状态快照
- 授权解除语义
- 攻击者可控窗口的明确标记
- 形式化的义务规则
这将使系统更接近一种用于表达程序逻辑的语义语言。
义务层（Obligation Layer）
漏洞通常只有在代码与明确的规则进行比较时才变得明显。例如：“授权必须主导特权写入”、“可变权限必须在外部调用前被消耗”、“记账不变式必须保持一致”。编码这些“义务”允许模型检测规则违反，而不仅仅是寻找可疑的模式。
验证循环（Verification Loop）
最终，AI发现的可疑点应能被编译回具体的不变式、模糊测试或符号执行查询，以自动化地确认漏洞是否真实存在，减少误报。
局限性（Limitations）
这种方法可能最适用于语义层面的漏洞，例如：
- 重入
- 授权错误
- 记账不一致
- 生命周期违规
- 预言机滥用
它可能对以下方面的帮助不大：
- 低级EVM边缘情况
- Gas优化
- 存储槽冲突
- 编译器怪癖
但值得注意的是，语义错误恰恰代表了真实世界中DeFi漏洞的很大一部分。
结论（Conclusion）
核心思想很简单：智能合约漏洞通常是逻辑上的不一致。如果我们把代码“翻译”成一种让这些不一致表现为语言矛盾的表示形式，那么擅长处理语言的模型可能会更有效地进行推理。
早期实验表明，与直接分析原始Solidity代码相比，结构化的自然语言表示有时可以提高漏洞检测的召回率。
该项目仍处于起步阶段，但它提出了一个有趣的可能性：语言可能不仅仅是向人类解释程序的一种方式，它也可能是AI推理程序逻辑的一种更优的媒介。
本文探讨了如何通过语义转换提升AI的代码分析能力，这种将程序逻辑转化为更易理解的形式的思路，在计算机基础 领域的编译原理中也有体现。对智能合约开发与安全感兴趣的开发者，欢迎在 云栈社区 交流分享更多实战经验。
发表于 6 小时前
|
查看: 4|
回复: 0
