💻 computer science

Chiral Analysis of Smart Contracts: Detecting Vulnerabilities from Relational Inconsistencies Across Business Paths

本文介绍了“手性分析”（chiral analysis），这是一种通过 ChiralDetector 工具实现的关联静态分析模型，它通过识别语义成对业务路径之间的不一致性来检测智能合约漏洞，从而有效地发现传统单函数分析器所遗漏的复杂逻辑漏洞。

原作者： Yue Xue

发布于 2026-07-21

📖 1 分钟阅读☕ 轻松阅读

CC BY 4.0

原作者： Yue Xue

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

侦探的困境：当代码因“遗漏”而撒谎

想象你是一名正在繁华都市中破解谜团的侦探。通常情况下，你会寻找“冒烟的枪口”：破碎的窗户、泥泞的脚印或可疑的便条。在计算机代码的世界里，特别是运行在区块链上的“智能合约”中，传统的安全工具就像这样的侦探。它们逐行扫描代码，寻找明显的错误，比如门上没锁，或者计算中的数学错误。这些工具擅长发现“局部”漏洞——即那些发生在单个房间内的错误。

但如果罪案根本不在房间里呢？如果谜团在于：前门锁好了，但后门却大开着，而这两扇门本应属于同一个安全系统？在计算机科学中，这被称为“关系型”问题。这不在于某个损坏的零件，而在于两个本应匹配却不匹配的零件。本文探讨了一种捕捉这类隐蔽漏洞的新方法：通过比较成对的代码路径，将它们视为必须反映相同真相的镜像。如果一条路径说“停止”，而另一条路径说“前进”，那么系统就是破碎的，即便“停止”和“前进”本身看起来都完全无误。

论文：手性分析与镜像测试

这篇论文介绍了一种聪明的新方法，称为手性分析（Chiral Analysis）。“手性（Chiral）”一词源于化学，描述的是那些互为镜像但无法完美重叠的对象（例如你的左手和右手）。在智能合约的世界里，作者提出许多业务操作都是成对出现的：例如“单笔”交易与“批量”交易、“买入”与“卖出”、或是价格的“预览”与价格的“执行”。这些配对构成了代码中的“手性双生子”。

其核心思想简单而强大：将这些配对视为正在互相检查对方作业的过程。如果用户购买了一件物品，代码应该收取费用。如果同一用户稍后卖出该物品，代码处理资金的方式应当与最初的购买逻辑相符。如果“买入”路径按美元收费，而“卖出”路径却错误地以另一种货币进行退款；或者“批量”版本忘记了退还“单笔”版本会退还的资金，那么漏洞就产生了。作者认为，这些漏洞在标准扫描器面前是隐形的，因为每一行代码单独看都是正确的。只有当你把两条路径举到镜子前，发现它们并不匹配时，错误才会显现。

为了发现这些隐形错误，作者构建了一个名为 ChiralDetector 的原型工具。你可以把它想象成一个拥有明确工作职责的超级聪明实习生。首先，它读取整个代码库，并绘制出每一种可能的“业务路径”（就像追踪顾客在商店里的每条路线一样）。然后，它使用一个“静态排序器（static ranker）”——一套简单的规则——来猜测哪些路径可能是手性的双生子。例如，它可能会寻找一个名为 buy 的函数和一个名为 sell 的函数，且两者都涉及同一个银行账户。

一旦确定了潜在的双生子列表，它就会请出“重量级选手”：大语言模型（LLM），一种能够理解人类语言和代码的 AI。这个 AI 不仅仅是在寻找错误，它更像是一个逻辑学家。它会追问：“如果这两条路径应该是镜像，它们应该遵循什么规则？”它会检查七个特定的维度：

防护（Guards）： 两条路径是否检查了相同的密码或权限？
参与者（Actors）： 在两条路径中，是否都是同一个人在支付和接收资金？
状态（State）： 两条路径是否以同样的方式更新数据库？
数值（Value）： 它们处理费用和退款是否保持一致？
顺序（Order）： 它们的执行顺序是否一致？
失败（Failure）： 如果出现问题，两条路径是否以同样的方式崩溃或恢复？
外部（External）： 它们是否信任相同的外部来源？

如果 AI 发现了不匹配，它不会立即大喊“有 Bug！”。它会将发现的结果传递给一个“严格验证器（strict validator）”。这个验证器就像一个持怀疑态度的编辑，试图证明 AI 是错的。它会问：“这真的是一个 Bug，还是仅仅是一种设计选择？”最后，该工具会将相似的发现归为一类，这样它报告的就不是 100 个微小的错误，而是那一个重大的根源问题。

结果：寻找隐藏的故障

作者在名为 Phi protocol 的真实项目中测试了这个系统。结果表明，这种方法是有效的，尽管仍处于开发阶段。

以下是他们在实验中观察到的情况：

工具首先寻找了 3,217 对代码路径。
在过滤掉明显不相关的路径后，保留了 1,643 对进行深入调查。
AI 检测器发现了 201 个潜在问题（包括“可疑”和“已确认”的候选对象）。
在对相似报告进行分组并去除重复项后，这一数字缩减至 101 组。
严格验证器进一步将其削减至 44 个确认的正例。
最后，经过人类专家对根源问题的审查，团队确定了 13 个独特的、有效的议题。

这 13 个问题正是标准工具会错过的类型。例如：

“证明”混淆： 系统允许将所有权的证明重用于其他物品，因为“买入”和“领取”路径未能将证明与特定物品正确绑定。
费用混乱： 系统的一部分按“基点”（百分比单位）计算费用，而另一部分却将同一个数字视为“wei”（极小的货币单位），导致巨大的财务错误。
退款陷阱： 当用户超额支付时，“单笔”交易路径将钱退还给了用户，但“批量”交易路径却意外地将退款发送到了中间合约，导致用户空手而归。

作者指出，这种方法特别擅长捕捉“业务逻辑”漏洞——即关于系统如何“思考”金钱和规则的错误——而非简单的拼写错误。他们注意到，该过程并非完美；它产生了很多“噪音”（误报）需要清理，并且依赖于 AI 是否足够聪明以识别出这种关系。然而，它能发现 13 个其他工具错过的独特且高影响力的议题，这一事实表明，通过“手性配对”的视角来审视代码是一个充满前景的新方向。

论文总结道，虽然这并不是解决所有安全问题的万灵药，但它提供了一种结构化的方式，去寻找那些隐藏在代码行之间的漏洞。通过将代码路径视为镜像，我们终于能够看到当倒影与本体不符时所产生的裂痕。

技术摘要：智能合约的手性分析（Chiral Analysis）

1. 问题陈述

智能合约的漏洞通常并非源于孤立的不安全语句，而是源于在语义上成对但语法上不同的业务路径之间的关系不一致性（relational inconsistencies）。常见的例子包括：

单次入口与批量入口之间的差异。
直接流与适配器流（adapter-based flows）之间的差异。
报价（预览）路径与执行路径之间的差异。
逆向操作（例如：买入 vs. 卖出，铸造 vs. 销毁）。

现有的静态分析工具擅长检测局部语法模式、污点式依赖和单函数漏洞（如重入、未检查调用）。然而，它们缺乏检测“关系型漏洞”的“预言机（oracle）”：它们无法判断两个对应的路径是否保持了相同的守卫条件（guards）、状态转换、数值流或失败行为。这类漏洞通常需要通过对比包装器（wrapper）与核心函数、或批量分发器与单次操作路径之间的逻辑来发现。

2. 方法论：手性分析（Chiral Analysis）

本文引入了手性分析，这是一种关系模型，将语义成对的业务路径视为彼此的隐式规范。术语“手性（chiral）”捕捉了那些镜像式、替代性或生命周期相关的操作（例如：单次/批量、包装器/核心），而无需要求语法上的同一性。

2.1 手性漏洞模型

作者将手性关系（ $R_\chi$ ）形式化为一种静态的蜕变关系（metamorphic relation）模拟。它由两个路径（ $p, q$ ）、一个关系类型（ $\tau$ ）以及一组**关系诱导义务（relation-induced obligations）**组成。这些义务是对跨越七个语义维度预期行为的近似描述：

守卫（Guard）： 修饰符、前提条件和资格检查。
参与者（Actor）： 调用者、签名者、付款人和退款接收者的身份。
状态（State）： 读/写集、标志位、计数器和状态增量。
数值（Value）： 单位、费用、奖励、转账和退款处理。
顺序（Order）： 检查-效果-交互（check-effect-interaction）序列和结算时机。
失败（Failure）： Revert 行为、部分成功语义和事件发射。
外部（External）： 预言机使用、回调和跨合约依赖。

手性漏洞被定义为违反上述义务并导致可行的安全或协议影响（例如：资金损失、未经授权的状态变更或会计错误）的行为。

2.2 ChiralDetector 流水线

作者在 ChiralDetector 中实现了这一模型，这是一个旨在平衡召回率与精确度，同时管理大语言模型（LLM）成本的四阶段流水线：

路径提取与摘要：
- 从 Solidity 源代码构建项目级调用图。
- 提取“业务路径”（单函数、入口到叶子节点的链、以及分支段）。
- 为每个路径生成语义事实摘要（ $\Phi(p)$ ），捕捉存储读写、数值转账、修饰符和外部调用。这种抽象是特意经过损耗处理的，但侧重于面向关系。
候选对缩减：
- 通过静态排序器避免 $O(n^2)$ 的穷举比较。
- 根据共享存储足迹、重叠的外部调用、命名提示（如 "claim" 与 "batchClaim"）以及参与者/数值流的相似性对路径对进行评分。
- 优先考虑可能构成手性关系的路径对，同时不删除可能存在高召回信号的不确定项。
语义过滤与检测（基于 LLM）：
- 语义过滤器： 确定一对路径是否合理地构成了手性关系，并分配关系类型（例如：逆向关系、包装器/核心关系）。其指令允许接受路径长度不同或经济方向相反的路径对。
- 关系感知检测器： 在确认关系后，LLM 识别具体的违规义务，提供源码证据，并构建影响论证。提示词采用“契约”结构，以强制进行显式推理而非给出模糊结论。
严格验证与去重：
- 严格验证器尝试通过检查关系是否合理、是否存在证据以及是否存在使影响失效的替代代码路径来证伪发现。
- 根因去重合并具有相同底层缺陷和可能修复方案的多个报告，区分路径层面的噪声与根源层面的问题。

3. 核心贡献

手性分析模型： 一种关系型漏洞框架，将对应的业务路径视为隐式规范，超越了单函数分析。
形式化： 将手性关系定义为静态蜕变关系的模拟，并推导出七个具体的义务维度。
ChiralDetector 实现： 一个集成了静态分析、静态路径排序、基于 LLM 的语义检测、严格证伪验证和根因去重的原型流水线。
经验证据： 在 Phi 协议上的初步评估，展示了检测难以用单函数规则表达的业务逻辑不一致性的能力。

4. 评估结果

作者在 Phi 协议上对 ChiralDetector 进行了评估，该协议包含多种关系形态（claim/batch, adapter/factory, quote/execution）。

漏斗指标：
- 从 3,217 个静态排序的候选对开始。
- 减少至 1,643 个用于语义检测的路径对。
- 产生 201 个清洗后的发现/可疑候选者。
- 压缩至 101 个本地去重后的组。
- 44 个组在严格验证中幸存。
- 最终人工根因去重得出 13 个有效的唯一问题。
代表性发现：
- M10： 跨资产 Merkle 证明重用（相似流/守卫违规）。
- M13： 费用单位不匹配（基点 vs. wei）（数值/单位违规）。
- M12： 公共追踪辅助函数破坏策展人状态（状态/访问违规）。
- M05/M02/M04： 退款传播缺口以及单次与批量路径之间的守卫不对称（包装器/核心以及单次/批量数值流违规）。
成本分析：
- 完整运行成本约为 212.70 元人民币（不含人工时间）。
- 主要成本在于 LLM 推理（语义过滤、检测和验证），而非静态分析。
- 严格验证器显著降低了噪声，拒绝了 101 个本地去重组中的 57 个。

5. 重要性与声明

论文声称手性分析揭示了一类漏洞——关系不一致性——这类漏洞在自然状态下很难用单函数规则来表达，但对协议安全至关重要。

洞察： 许多业务逻辑漏洞的存在是因为两个相关的路径在如何处理共享业务对象（例如：退款接收者或费用计算）时存在分歧，而不是因为单个函数本身在局部是不安全的。
结构化 LLM 使用： 论文认为，在结构化流水线（静态缩减 $\to$ 语义过滤 $\to$ 严格验证）中使用 LLM，比“直接代理审计（direct agent auditing）”（无限制地阅读代码）更有效且更具成本效益。该流水线将中间决策（路径对、关系、义务）外部化，使得分析过程是可检查且可调试的。
谦逊态度： 作者明确指出，目前的评估是针对单一协议的初步案例研究。他们尚未建立通用的召回率或精确度指标。他们也承认了局限性，包括 Solidity 语义在路径提取中的近似处理、LLM 幻觉的可能性，以及缺乏自动化的证明生成（可执行的 PoC 交易）。

这项工作旨在将业务逻辑推理过程变得显式且可重复，为描述为何特定不一致性至关重要提供了一套专业词汇。