💻 computer science

Cargo Sherlock: An SMT-Based Checker for Software Trust Costs

本文介绍了 Cargo Sherlock，这是一个基于 SMT 的框架，它通过将元数据驱动的人为因素与代码分析进行形式化结合，来量化软件信任度，从而检测 Rust 依赖项中的供应链攻击。

原作者： Muhammad Hassnain, Anirudh Basu, Ethan Ng, Caleb Stanford

发布于 2026-02-04

📖 1 分钟阅读☕ 轻松阅读

原作者： Muhammad Hassnain, Anirudh Basu, Ethan Ng, Caleb Stanford

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

想象一下你正在建造一座房子（你的软件项目）。为了完工，你需要从其他人那里购买砖块、窗户和门（第三方软件库）。大多数时候，你只是随手抓起最近的一个贴着“砖块”标签的箱子，并祈祷它的质量没问题。但如果有人把真正的砖块换成了装满炸药的假砖头怎么办？这就是供应链攻击。

这篇论文介绍了一个名为 Cargo Sherlock 的工具，它能帮助你在使用这些“砖块”之前判断它们是否安全。它不仅仅是在靠直觉猜测，而是像一位极其严谨的侦探一样，为每一件你想使用的软件计算出一个**“信任成本”（Trust Cost）**。

以下是其工作原理的拆解，通过简单的概念进行说明：

1. “信任成本”类比

把信任一段软件代码想象成申请贷款。

低信任成本： 你很容易信任这段软件。也许它来自一位著名的建筑师（知名的作者），或者它经过了认证检查员的检查（审计）。你愿意支付较低的“成本”来相信它是安全的。
高信任成本： 你必须竭力发挥想象力才能相信它是安全的。也许作者是个陌生人，或者该软件从未经过审计，或者它的下载量非常少。要相信它是安全的，你必须进行巨大的飞跃。这种“飞跃”的代价很高。

Cargo Sherlock 的任务是找到让你相信某段软件是安全的最便宜的方法。如果证明一段软件安全的最便宜方式仍然需要支付巨额费用（一个很高的数值），工具就会告诉你：“嘿，这很有风险。别用它。”

2. 侦探如何解开谜题

该工具使用一种数学逻辑引擎（称为 SMT）来解开谜题。想象你有一系列可以用来证明某个库是安全的线索（假设）：

线索 A： “它有 100 万次下载量。”（成本：低，因为受欢迎通常意味着安全）。
线索 B： “它经过了 Google 的审计。”（成本：极低，因为 Google 是受信任的）。
线索 C： “作者是一个没有任何历史记录的陌生人。”（成本：高，因为这是一个巨大的风险）。

该工具会查看所有的依赖项（软件自身的“原料”），并尝试构建一条逻辑链。它会询问：“哪种线索的组合成本最低，足以证明这段代码是安全的？”

场景 1（安全）： 一个受欢迎的库拥有 100 万次下载量。工具说：“好吧，线索 A 就足够了。总成本很低。结论：安全。”
场景 2（危险）： 一个可疑的库没有下载量、作者是新人且没有审计。工具试图寻找一个廉价的线索但失败了。要证明它是安全的唯一方法是假设“它毫无理由地就是安全的”，而这需要极高的成本。结论：严重风险。

3. “人为因素”

通常情况下，计算机只观察代码。但人类是基于声誉、下载量和审计来信任事物的。Cargo Sherlock 的特别之处在于它将数学与人类直觉结合在一起。

它允许你设定规则。你可以说：“我信任来自公司 X 的审计多于公司 Y，”或者“我不信任下载量过高的代码，因为那可能是机器人刷出来的。”
它让这些人类的感觉变得可审计。它不再是一个黑盒给出“信任度：85%”这样的结果，而是会说：“我们信任它，是因为它通过了 Google 的审计（成本：5）并且有大量下载（成本：10）。”

4. 工具发现了什么（研究结果）

作者在真实和虚假的场景下测试了 Cargo Sherlock：

抢注域名/名称攻击（Typosquatting，假名攻击）： 攻击者经常创建名字看起来与真实库非常相似的伪造库（例如，用 serde_yml 代替 serde_yaml）。当工具检查这些伪造品时，由于作者知名度未知且下载量异常之低，“信任成本”骤增。工具准确地将其标记为危险。
AI 生成的代码： 他们测试了一个由 AI 维护、代码质量较低的库。由于“作者”发生了变化且代码质量下降，该工具给出的风险评分比原始的人类维护版本更高。
已知漏洞： 工具发现，即使是某些被其他数据库列为“有漏洞”的库，在 Cargo Sherlock 看来仍然显得“安全”，因为它们非常受欢迎。这是一个警告：受欢迎并不总是意味着安全。

5. 速度与规模

该工具有两种解题方式：

慢速方式： 尝试所有可能的组合。它适用于小型项目，但在处理大型项目时会卡住。
快速方式： 使用一种聪明的捷径（Horn Clauses），就像一位高效的侦探。它可以处理拥有数百个依赖项的库而不会崩溃，并在几分钟内给出结果。

总结

Cargo Sherlock 是一个面向软件开发者的工具，它将“这看起来安全吗？”这种模糊的感觉转化为了一个具体的数字。它计算出为了相信一段软件是安全的，你所必须支付的最小信任价格。如果这个价格太高，它就会发出警告，让你远离，从而在供应链攻击发生前进行拦截。

注：论文明确指出，该工具是针对 Rust 编程语言生态系统（被称为“crates”的库）设计的。

技术摘要：Cargo Sherlock

问题陈述

软件供应链攻击（如 SolarWinds 事件、XZ Utils 后门以及恶意 Rust 库 rustdecimal 和 faster_log）对开源生态系统构成了重大威胁。现有的检测方法分为两类：

形式化可检查工具： 静态分析、模糊测试和类型系统，它们提供具体的语法或语义保证，但通常局限于特定的程序属性。
以人为中心的信任： 依赖于启发式方法的行业实践，例如下载量、作者声誉和人工审计。虽然这些方法很实用，但缺乏形式化保证，难以理解信任假设是如何组合的，也难以对信任依赖项背后的推理过程进行形式化验证。

核心问题在于缺乏一个既能量化信任，又能以形式化可检查的方式纳入人类因素（例如元数据、审计历史）的框架。作者旨在创建一个具有特定性、可审计性、可配置性和可组合性的系统。

方法论

论文提出了 Cargo Sherlock，一种利用 可满足性模理论 (SMT) 来量化 Rust 库（crates）供应链信任度的工具。该方法基于 最小信任问题 (Minimum Trust Problem)。

最小信任问题

作者将信任形式化为一个逻辑优化问题：

输入： 关于软件依赖项的一组候选假设 ( $\Gamma$ )（例如，“如果该 crate 有许多下载量，则它是安全的”）、一个结论 ( $c$ ，例如“该 crate 是安全的”) 以及一个为每个假设分配成本的代价函数 ( $C$ )。
目标： 找到一个假设子集 $\Delta \subseteq \Gamma$ ，使得 $\Delta$ 在逻辑上蕴含 $c$ ( $\Delta \models c$ )，且 $\Delta$ 中的成本之和最小。
解释： 较低的“信任成本”意味着基于用户配置的假设，存在一个更强、更具合理性的安全论证。较高的成本则表示代码风险较高，需要更多的“信心”来建立信任。

算法

论文提出了两种算法来解决最小信任问题：

朴素算法 (Algorithm 1)： 使用命题变量上的量词和线性整数算术对问题进行编码。它递归地构建代表依赖树的公式，并使用 SMT 求解器来寻找最小成本。由于存在嵌套量词，这种方法虽然正确，但计算开销巨大。
Horn 子句算法 (Algorithm 2)： 将假设限制为无环确定性 Horn 子句 (acyclic definite Horn clauses)。它使用一种展开过程（类似于 SLD 解析）将问题转化为析取范式 (DNF) 公式。随后，它通过使用无量词 SMT 查询在成本空间内进行二分查找。虽然生成的公式在最坏情况下可能是指数级的，但在实践中这种方法显著提高了效率。

复杂度： 通用的最小信任问题被证明是 $\Sigma^P_2$ -hard。限制为 Horn 子句（HORN-MINTRUST）被证明是 NP-完全 (NP-complete) 的，这证明了使用 SMT 求解器的合理性。

实现与设计

Cargo Sherlock 是一个基于 Python 的工具，集成了以下功能：

数据收集： 聚合来自 crates.io（下载量、星数、作者）、GitHub、RustSec（漏洞）以及静态分析工具（Miri、Cargo Scan）的元数据。
关系模型： 将数据组织为实体（Crates、Authors、Audits、Dependencies、Tool Results）。
假设类型：
- 正向 (Positive)： 安全性的证明（例如：受信任的作者、通过审计、无副作用）。
- 负向 (Negative)： 不信任的证明（例如：存在于 RustSec 中、被 Miri 标记）。
- 参数化 (Parameterized)： 基于元数据的连续变化的成本（例如：下载数量）。
输出： 计算 信任成本 (Trust Cost) 和 不信任成本 (Distrust Cost)（0–100 标度）。两者结合产生严重程度标签（安全、低/中/高严重性、关键）。

核心贡献

形式化模型： 将供应链信任问题形式化为可通过 SMT 求解的最小信任问题，满足了特定性、可审计性、可配置性和可组合性的要求。
算法： 提出了两种求解问题的算法，包括一种优化的基于 Horn 子句的方法，该方法比朴素的基于量词的方法能更有效地处理大型依赖树。
工具实现： 一个可运行的 Rust 原型工具（Cargo Sherlock），它整合了现实世界的元数据和程序分析结果来计算信任成本。
评估： 通过实证研究展示了该工具检测合成及真实世界供应链攻击的能力，及其可扩展性。

评估结果

作者通过四个研究问题对 Cargo Sherlock 进行了评估：

RQ1 (合成拼写劫持)： 在针对前 100 个 Rust crate 的合成拼写劫持变体进行测试时，该工具分配了显著更高的信任成本和严重性标签（通常为“关键”），相比之下，原始的安全 crate 则表现不同。大多数原始 crate 被标记为“安全”，而拼写劫持版本由于下载量较低且作者不可信，被标记为高风险。
RQ2 (真实世界事件)：
- faster_log： fast_log 的一个恶意拼写劫持版本。Cargo Sherlock 正确地将其分配为“关键”标签（信任：75，不信任：80），而原始版本的标签为“中等严重性”（信任：37，不信任：73），其差异主要源于不可信的作者和副作用。
- serde_yml： serde_yaml 的一个 AI 维护的分支。尽管不信任成本相似，但该工具对该分支分配了“低严重性”标签（相比之下，原始版本为“安全”），这主要是由于作者身份的变化。
RQ3 (已知漏洞)： 在针对 RustSec 数据库中列出的 592 个 crate 进行测试时（禁用了 RustSec 特定的假设），许多 crate 仍被标记为“安全”或“低严重性”。这表明，在信任模型中，流行度（高下载量）可能会掩盖已知的漏洞，这意味着如果用户仅依赖流行度指标，可能会认为有漏洞的 crate 是安全的。
RQ4 (可扩展性)：
- 算法 1： 无法扩展，在处理超过约 10 个依赖项的 crate 时会出现超时或崩溃。
- 算法 2： 成功评估了拥有高达 150 个依赖项的 crate，且在 10 分钟窗口内完成，展示了在大多数现实场景中的实际可扩展性。

重要性与主张

论文声称 Cargo Sherlock 提供了一个可形式化检查的框架，用于量化软件信任，从而弥合了严谨的形式化方法与行业开发者基于启发式的实践之间的鸿沟。

特定性： 与黑盒机器学习方法不同，Cargo Sherlock 能生成一组具体的假设（例如：“受 Alice 信任”、“高下载量”）来解释信任成本，使推理过程具有可审计性。
可配置性： 用户可以调整假设的成本（例如：惩罚 AI 维护的代码或奖励特定的审计员），以符合其风险承受能力。
可组合性： 该模型允许在依赖树中组合信任成本，从而实现对供应链风险的整体视图。

作者总结道，虽然该工具能有效识别风险依赖项（如拼写劫持和不可信的分支），但它同时也揭示了当前信任指标的局限性：如果特定的漏洞没有在假设中被明确建模，那么拥有高下载量的热门 crate 仍可能被分类为“安全”。该工具是开源的，可用于 Rust 开发工作流中。