💻 computer science

RustyDL: A Program Logic for Rust

本文提出了名为 RustyDL 的 Rust 程序逻辑，旨在通过直接在源代码层面进行推理，克服现有工具依赖中间语言转换的局限，从而为 Rust 构建支持人机交互的演绎验证工具（如 KeY 的 Rust 原型）以证明复杂的功能属性。

原作者： Daniel Drodt, Reiner Hähnle

发布于 2026-02-26

📖 1 分钟阅读☕ 轻松阅读

原作者： Daniel Drodt, Reiner Hähnle

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

这篇论文介绍了一个名为 RustyDL 的新工具，它的目标是帮助人类像“侦探”一样，一步步地检查 Rust 语言编写的程序是否绝对正确。

为了让你轻松理解，我们可以把这篇论文的核心内容想象成给 Rust 语言设计的一套“超级说明书”和“检查手册”。

1. 背景：Rust 是个严格的“管家”，但我们需要更聪明的“审计员”

想象 Rust 是一个极其严格的房屋管家。

它的特长：它非常擅长防止“数据打架”（数据竞争）和“内存泄漏”（内存安全）。它有一套独特的规则（所有权系统），规定每个物品（数据）只能有一个主人。如果主人把物品借给别人（引用），它必须确保借出期间没人乱动，或者借出时只能借给一个人。
现状：以前，人们想验证 Rust 程序是否正确，通常是把 Rust 代码翻译成一种“中间语言”（就像把中文翻译成一种只有机器能懂的密码，再交给机器去检查）。
问题：这种“翻译法”有两个大毛病：
1. 信任链断裂：你得相信翻译过程没错，万一翻译错了，检查结果也没用。
2. 黑盒操作：如果机器说“错了”，你很难知道具体是哪一行代码、哪个逻辑出了问题，因为你看不到翻译后的“密码”。

这篇论文提出的 RustyDL，就是要把“翻译”扔掉，直接在 Rust 源代码上建立一套逻辑系统。 它让人类专家（就像高级审计员）能直接介入，和机器一起，一步步地证明代码是完美的。

2. 核心概念：RustyDL 是什么？

RustyDL 就像是为 Rust 量身定制的一套**“逻辑显微镜”**。

以前的工具：像是一个自动化的“扫雷器”，它自动扫描，告诉你哪里可能有雷，但你不能手动去排雷。
RustyDL：像是一个**“人机协作的排雷小组”**。它允许人类审计员在关键步骤说：“等等，这里逻辑有点复杂，让我手动推演一下这一步。”

3. Rust 的三大挑战与 RustyDL 的妙解

Rust 有三个让传统逻辑工具头疼的“怪脾气”，RustyDL 用非常聪明的比喻解决了它们：

A. 所有权与“移动” (Ownership & Move)

Rust 的怪脾气：在 Rust 里，如果你把一个变量赋值给另一个变量（比如 x = y），y 里的东西就被“搬走”了，y 变成了空壳，不能再用了。这就像你把家里的唯一一把钥匙给了朋友，你自己手里就没钥匙了，不能再开门。
RustyDL 的解法：它引入了**“匿名更新”**。当钥匙被搬走时，逻辑系统不会去追踪那个空壳里到底剩了什么（因为那是未知的），而是直接给那个位置贴个标签：“这里现在是个未知的秘密”。这样，逻辑系统就不会因为试图读取一个“已搬走”的变量而崩溃，完美模拟了 Rust 的“移动”语义。

B. 可变引用 (Mutable References)

Rust 的怪脾气：你可以把变量借给别人修改（&mut）。比如你借给朋友一把万能钥匙，朋友可以打开门改里面的东西，但你不能直接改，必须通过朋友。
RustyDL 的解法：它没有像以前那样去维护一个复杂的“借出清单”（这太麻烦了）。相反，它把“借出”看作一种**“指向关系的魔法”**。
- 当你写 x = &mut y 时，系统不记录“谁借了谁”，而是直接说：x 现在是一个**“指向 y 的魔法指针”**。
- 当你写 *x = 5（通过指针修改）时，系统直接把这个动作翻译成“修改 y 的值”。
- 比喻：以前是“登记借书卡”，现在直接是“拿着遥控器直接控制电视”。这样既简单又高效。

C. 数组与循环 (Arrays & Loops)

Rust 的怪脾气：数组访问可能会越界（导致程序崩溃），循环可能无限运行或中途跳出（break）。
RustyDL 的解法：
- 数组：它把数组想象成一个**“带索引的储物柜”**。访问 arr[i] 时，逻辑系统会先检查 i 是否在柜子范围内。如果在，就打开柜子；如果不在，就标记为“程序崩溃（Panic）”。
- 循环：它引入了一个叫**“循环作用域”（Loop Scope）的概念。想象循环是一个“时间胶囊”**。每次循环，系统都会问：“这次循环是怎么结束的？是正常结束，还是中途‘跳’出来的（break）？”它用一个特殊的变量记录这个“退出原因”，从而让逻辑系统能精准地处理那些中途跳出的复杂循环。

4. 实际效果：KeY 工具的原型

作者基于著名的验证工具 KeY（原本用于验证 Java 代码），做了一个 Rust 版本的原型机，叫 Rusty KeY。

成果：他们成功用它验证了一些复杂的 Rust 函数，比如二分查找算法。
速度：在 2.1 秒内，生成了 4000 多条逻辑推理步骤，证明了代码是正确的。
意义：这证明了“人机协作”的模式在 Rust 上是可行的。以前没人敢想能在 Rust 源代码层面做这么细致的逻辑证明。

5. 总结：这为什么重要？

想象一下，如果你要建造一座核电站（安全关键系统），你希望：

完全自动化：机器自动检查，但机器可能会漏掉一些极其复杂的逻辑漏洞。
完全人工：人眼检查，但人太累了，容易出错。

RustyDL 提供的是“第三条路”：
它让机器处理繁琐的数学计算和基础规则，而让人类专家在关键时刻介入，处理那些机器搞不定的复杂逻辑（比如复杂的借用关系、循环跳出）。

一句话总结：
这篇论文发明了一套**“人类与机器并肩作战的说明书”**，让我们能直接在 Rust 源代码上，像解数学题一样，一步步推导出代码是绝对安全的，而不需要把代码翻译成别人看不懂的“密码”。这对于未来在操作系统、自动驾驶等关键领域使用 Rust 来说，是一个巨大的进步。

RustyDL：Rust 程序逻辑技术总结

本文介绍了 RustyDL，一种专为 Rust 编程语言设计的程序逻辑（Program Logic），旨在为 Rust 提供基于源代码的自动交互式演绎验证（Human-in-the-Loop, HIL）基础。作者 Daniel Drodt 和 Reiner Hähnle 来自德国达姆施塔特工业大学，他们提出了一种直接在源代码级别进行推理的方法，以解决现有验证工具依赖中间语言翻译所带来的局限性。

1. 研究背景与问题 (Problem)

1.1 Rust 的验证挑战

Rust 以其强大的类型系统（所有权、借用、生命周期）保证了内存安全和无数据竞争，无需垃圾回收。然而，在安全关键领域（如 Linux 内核），形式化验证至关重要。

1.2 现有工具的局限性

目前大多数 Rust 验证工具（如 Creusot, Prusti, Aeneas）采用翻译方法：

将 Rust 代码和规格说明翻译成中间语言（如 Viper 或 Why3）。
生成一阶逻辑验证条件（VCs），并使用 SMT 求解器进行自动化处理。
缺点：
1. 信任问题：必须信任从 Rust 到中间语言的复杂翻译过程。
2. 缺乏交互性：当验证失败时，工程师难以将 SMT 求解器的输出与原始代码直接关联，无法手动干预证明步骤或处理高度复杂的函数属性。
3. 自动化与控制的权衡：现有工具倾向于全自动化，缺乏像 KeY 或 KIV 那样提供显式证明对象、允许用户逐步检查证明的“人在回路”（HIL）能力。

核心问题：能否将 HIL 风格的源代码级演绎验证引入 Rust 世界？如何在其程序逻辑中建模 Rust 独特的所有权、借用和引用机制？

2. 方法论 (Methodology)

2.1 RustyDL 逻辑框架

RustyDL 是基于**动态逻辑（Dynamic Logic, DL）**的扩展，类似于 JavaDL，但针对 Rust 进行了定制。

基础：扩展了类型化一阶逻辑。
核心机制：
- 模态算子：使用 $\langle p \rangle \phi$ （总正确性）和 $[p] \phi$ （部分正确性）描述程序行为。
- 更新（Updates）：引入细粒度的状态转换机制，将程序执行分解为一系列确定性的状态变化，而非直接执行整个程序片段。
- Kripke 结构：形式化定义状态转换，假设 Rust 程序是确定性的。

2.2 核心挑战与解决方案

RustyDL 针对 Rust 的五个核心特性设计了专门的演算规则：

(1) 所有权与移动语义 (Ownership & Move Semantics)

挑战：Rust 中非 Copy 类型的赋值会导致值被“移动”（Move），原变量不再可用。
方案：使用匿名化更新（Anonymizing Update）。当变量 $y$ 被移动到 $x$ 时，逻辑规则将 $y$ 更新为一个新鲜常量 $c$ 。这表示 $y$ 仍有值，但具体值未知（不可预测），从而避免了引入未初始化值的复杂性，同时保证了逻辑的简洁性。

(2) 可变引用 (Mutable References)

挑战：可变引用（&mut）允许修改借用者的值，且借用者本身不存储值，而是存储“出借位置”（Place）。
方案：引入突变更新（Mutating Updates），记为 $t_1 \ast \to t_2$ $t_{1} * \to t_{2}$ 。
- 当执行 *x = val 时，逻辑上不是更新 $x$ 的值，而是更新 $x$ 所指向的“位置”（Place）。
- 引入 Place 类型和 mref 函数来建模借用关系。
- 这种方法避免了显式维护“活跃借用集合（Active Loans）”的复杂状态，直接利用 Rust 编译器的借用检查器保证作为前提。

(3) 共享引用 (Shared References)

方案：共享引用（&）被视为对值的只读访问。逻辑上将其建模为 sref(y)，并在解引用时直接还原为原值，因为共享引用期间原值不可变。

(4) 整数溢出 (Integer Overflow)

挑战：Rust 在 Debug 模式下溢出会 Panic，Release 模式下会回绕。验证通常关注 Debug 语义（安全性）。
方案：在演算规则中（如 assignAddU32）显式拆分情况：
- 如果加法结果在类型范围内，生成更新。
- 如果溢出，生成 panic!() 状态，从而在验证过程中强制证明无溢出。

(5) 循环与复杂控制流 (Loops & Control Flow)

挑战：Rust 的循环是表达式，可能通过 break、panic 或 return 提前终止，且 break 可带返回值。
方案：引入**循环作用域（Loop Scope）**概念（ $\loop x \ p \ \loop$ $\loopx p \loop$ ）。
- 使用辅助变量 $x$ 记录循环退出的原因（如 break 设为 true，继续设为 false）。
- 循环不变量规则通过符号执行一次通用迭代，并根据 $x$ 的值分支处理退出条件或继续循环，从而统一处理标准循环和带 break 的循环。

2.3 实现

原型：基于著名的演绎验证工具 KeY 构建。
语言：使用 KeY 的领域特定语言 Taclets 实现演算规则。
输入：基于 Rust 编译器的高层中间表示（HIR），经过简化和规范化。

3. 关键贡献 (Key Contributions)

RustyDL 程序逻辑：提出了首个针对 Rust 源代码的 HIL 风格程序逻辑，能够直接处理所有权、借用和可变引用，而无需翻译到中间语言。
突变更新（Mutating Updates）：创新性地设计了突变更新机制，优雅地解决了 Rust 可变引用的建模难题，避免了显式内存模型或借用集合的复杂性。
循环作用域规则：设计了能够处理 break、panic 和带值退出的复杂循环的归纳规则，解决了 Rust 循环作为表达式的验证难题。
KeY 集成与原型实现：成功将 RustyDL 集成到 KeY 系统中，实现了名为 Rusty KeY 的原型工具。
验证案例：展示了包括二进制搜索（生成 4260 条规则应用）、数组操作、借用和循环在内的多个验证示例。

4. 结果 (Results)

可行性验证：原型工具成功验证了包含复杂特性（如借用、循环、数组、元组）的 Rust 函数。
性能：在二进制搜索验证案例中，系统在 2.1 秒内完成了 4260 条规则应用的证明，展示了该方法的效率。
交互性：证明了在 Rust 验证中实现“人在回路”是可行的，用户可以在证明过程中手动干预步骤，这对于处理 SMT 求解器无法自动解决的复杂属性至关重要。

5. 意义与未来工作 (Significance & Future Work)

5.1 意义

填补空白：填补了 Rust 领域缺乏源代码级 HIL 验证工具的空白。
信任链缩短：通过直接在源代码级别推理，消除了对中间语言翻译的信任需求，提高了验证的可信度。
复杂属性验证：为验证高度复杂的函数属性（如并发程序、复杂数据结构）提供了可能，这是基于 SMT 的自动化翻译方法难以企及的。

5.2 未来工作

扩展 Rust 子集：支持 Traits、迭代器、模式匹配和泛型函数。
Unsafe Rust 验证：探索如何将逻辑扩展到 unsafe Rust，可能需要更显式的内存模型，但目标是保持最小化。
工具完善：完善规范语言（类似 JML），开发图形用户界面（GUI），并提高自动化程度以进行更全面的评估。

总结：RustyDL 证明了将成熟的演绎验证方法（如 KeY）应用于 Rust 是可行的。通过创新的逻辑设计（特别是突变更新和循环作用域），它克服了 Rust 所有权系统的建模难点，为构建高可信度 Rust 软件提供了新的验证范式。