语义同构：将Solidity转化为语言用于AI安全分析

将代码转化为语言：一种使用AI进行智能合约安全的新方法

论点（Thesis）

大型语言模型（LLMs）主要通过语言进行训练，而非形式化的编程语义。然而，目前大多数AI审计方法仍要求它们直接对原始Solidity代码进行推理。

我的论点很简单：将智能合约语义转化为结构化的自然语言表示，可以使LLMs更容易检测到漏洞。

我们不再要求LLM对语法繁重的Solidity代码进行推理，而是将代码转换为语义叙述，明确捕捉以下内容：

• 行为者（actors）
• 状态变化（state changes）
• 授权谓词（authorization predicates）
• 外部交互（external interactions）
• 顺序关系（ordering relationships）
• 攻击者可控窗口（attacker-controlled windows）

然后，我们要求模型分析该表示，以发现矛盾、缺失的前提和不安全行为。

关键假设是，当程序语义以LLMs训练的领域——即语言——表达时，它们的推理更为可靠。

启发（Inspiration）

概念上的灵感来源于道格拉斯·霍夫施塔特（Douglas Hofstadter）的《哥德尔、埃舍尔、巴赫》（Gödel, Escher, Bach）。书中反复出现的一个主题是同构性（isomorphism）：两个系统即使看起来完全不同，也可以共享相同的底层结构。

书中的例子包括：

• 音乐与数学
• 埃舍尔的画作与递归
• 形式逻辑与算术

不同的表示，相同的结构。

这个想法引出了一个问题：如果智能合约代码能够被翻译成另一种符号系统——语言——同时保留其语义，那会怎样？

换句话说，Solidity程序和结构化的自然语言系统描述可以是相同底层逻辑的同构表示。如果这种映射足够忠实，那么程序中的错误就应该表现为叙述中的逻辑不一致。

方法（The Method）

我实验的方法大致是：

Solidity → 语义提取 → 结构化英语表示 → LLM推理 → 潜在漏洞。

这种结构化表示不仅仅是文档。它明确描述了：

• 守卫条件（guards，执行所需的条件）
• 状态读取（state reads）
• 状态写入（state writes）
• 外部交互（external interactions）
• 执行顺序（execution ordering）
• 重入窗口（reentrancy windows）
• 行为者关系（actor relationships）

例如，一段Solidity代码序列：

token.transfer(msg.sender, amount);
balances[msg.sender] -= amount;

可以被翻译成语义表示，例如：

• 交互（Interaction）：合约将代币转账给调用者。
• 效果（Effect）：调用者的记录余额减少。
• 顺序（Ordering）：转移发生在余额更新之前。
• 控制转移（Control transfer）：外部代码可能在转移期间执行。

在这种形式下，模型无需从语法中推断语义。因果关系已经明确。

为什么这可能有效（Why This Might Work）

大多数智能合约漏洞并非语法错误。它们是语义不一致，例如：

• 授权谓词应用于错误的执行者
• 状态更新发生在攻击者可控的交互之后
• 记账变量与实际余额不符
• 预言机数值被假定为最新，但可能已过时
• 生命周期转换发生在无效阶段

这些本质上都是对逻辑规则的违反。

LLMs非常擅长检测矛盾、缺失的假设、因果不一致和叙述上的不连贯。

因此，与其要求模型解析Solidity语法并自行恢复语义，不如直接以语言形式呈现语义。

早期实验（Early Experiments）

为了快速验证这个想法，我进行了一个非常简单的实验。

设置：

• 模型：GPT-5.4
• 提示：一个简单的“查找漏洞”提示
• 比较：原始Solidity代码与相同代码的结构化英语表示。

测试案例（Test Case）

我在Code4rena Thor Wallet代码库上进行了测试，该代码库有公开记录的发现。

在相同的提示下：

• 原始代码分析检测到3个已确认的HM（高危）问题中的1个，以及1个已确认的low（低危）问题。
• 结构化英语分析检测到3个已确认的HM问题中的3个，以及许多已确认的low/qa（低危/质量保证）问题。

在包含义务规则的其他测试中，两种表示都能检测到问题，但英语版本产生了更清晰的因果解释。

这些仍然是小型实验，但结果表明表示方式的改变可能确实很重要。

为什么表示方式很重要（Why the Representation Matters）

原始Solidity代码包含大量的语法噪音。模型必须恢复语义关系，例如：

• 哪个状态变量代表授权
• 该授权何时被消耗
• 哪些交互将控制权转移给不受信任的代码
• 哪些假设在攻击者可控窗口中持续存在

结构化英语消除了这种负担，直接暴露了语义。

这种差异类似于比较机器码和源代码。计算是相同的，但一种表示方式更容易推理。

影响（Implications）

如果这个想法能够扩展，它将预示着AI审计工具的不同架构。

我们不再将LLM直接与原始代码结合，而是可以构建一个包含以下管道的系统：

代码 → 语义图 → 受控自然语言表示 → LLM推理 → 验证器循环。

在这种设计中，LLM成为语义推理引擎，而非代码解析器。

潜在的好处包括：

• 改进语义漏洞的检测
• 更清晰的漏洞解释
• 更好的推理可追溯性
• 更容易与不变式检查工具集成

下一步（What’s Next）

目前的原型仍处于非常早期阶段。接下来的步骤包括：

更大规模的评估（Larger Evaluation）

在CodeHawks First Flights（由于合约规模小，更适合小代币预算）、Code4rena竞赛和ScaBench/其他基准测试等数据集上进行测试，以验证表示优势是否适用于更多合约。

更好的语义表示（Better Semantic Representation）

当前版本仍然有些描述性。更强大的版本将包括：

• 显式谓词（explicit predicates）
• 状态快照（state snapshots）
• 授权解除语义（authorization discharge semantics）
• 攻击者可控窗口（attacker-controlled windows）
• 形式化义务规则（formal obligation rules）

这将使系统更接近逻辑风格的语义语言。

义务层（Obligation Layer）

漏洞通常只有在代码与明确的规则（例如：授权必须主导特权写入、可变权限必须在外部调用前被消耗、记账不变式必须保持一致）进行比较时才变得明显。编码这些义务允许模型检测规则违反，而不仅仅是可疑模式。

验证循环（Verification Loop）

最终，发现的结果应被编译回不变式、模糊测试或符号执行查询，以确认漏洞是否真实存在。

局限性（Limitations）

这种方法可能最适用于语义漏洞，例如：

• 重入（reentrancy）
• 授权错误（authorization errors）
• 记账不一致（accounting inconsistencies）
• 生命周期违规（lifecycle violations）
• 预言机滥用（oracle misuse）

它可能对以下方面帮助不大：

• 低级EVM边缘情况
• Gas优化
• 存储槽冲突
• 编译器怪癖

但语义错误代表了真实DeFi漏洞的很大一部分。

结论（Conclusion）

核心思想很简单：智能合约漏洞通常是逻辑不一致。如果我们把代码翻译成一种表示形式，让这些不一致成为语言上的矛盾，那么语言模型可能会更有效地对其进行推理。

早期实验表明，与原始Solidity分析相比，结构化英语表示有时可以提高漏洞检测能力。

该项目仍处于起步阶段，但它提出了一个有趣的可能性：语言可能不仅仅是解释程序的一种方式，它也可能是AI推理程序的一种更好方式。

• 原文链接： x.com/arniesec/status/20...
• 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～