Derek Dreyer：用 RustBelt 和 Iris 证明 Rust 的安全性

过去几年，我们在 Max Planck Institute for Software Systems 一直从事 RustBelt 项目。令人兴奋的是，我们把多年发展起来的逻辑基础——类型系统、理论和证明——应用到 Rust 这门仍在积极发展的真实编程语言上。

我会介绍 Rust 的有趣之处、建立其安全保证所面临的问题，以及我们为此开发的技术。更大的问题是：能否同时拥有高层次的安全性和系统编程所需的底层控制能力？

高级语言提供有用的抽象和自动内存管理；系统应用往往需要更精细地控制资源，传统上会使用 C 或 C++ 等语言。Rust 试图跨越这一鸿沟：既提供底层控制，又提供强类型安全、内存安全和数据竞争自由，并得到工业界支持。

底层代码的一个主要问题来源，是不受限制的修改与别名同时存在。多个引用可能指向同一对象，其中一个引用可以修改、释放或重新分配它，从而产生悬空指针、释放后使用错误、数据竞争和迭代器失效。

Rust 使用所有权类型系统约束这种组合。简化地说，对象可以是可修改的，也可以有多个活动别名，但不能同时满足两者。拥有一个值意味着控制其资源；没有其他活动访问时，所有者可以修改或释放它。

仅有所有权会过于严格，因此 Rust 还允许借用。共享引用可以复制并形成别名，但通常不能通过它修改对象。唯一的可变借用允许修改，同时保证该访问是唯一的活动别名。

看一个简单例子：创建 vector，push 42，然后遍历元素。这可以正常运行。但如果将 push 移入循环，类似的 C++ 程序就有迭代器失效的风险：vector 扩容可能重新分配存储，使迭代器指向已释放的内存。

Rust 会拒绝修改后的程序。遍历创建了不可变的共享借用；调用 push 则需要可变借用。迭代器仍持有共享访问，而 push 会修改 vector，因此编译器报告冲突。

把 push 移到循环之后，共享借用就已经结束。此时可以重新获得可变访问，程序也能编译。这个例子展示的静态分析能防止真实的一类错误，而不仅仅是语法限制。

这种标准解释很有用，但并不完整。有时实现确实需要同时使用修改和别名：双向链表、锁、通道和引用计数都涉及修改多方共享的状态。

Rust 通过 API 支持这种行为。Mutex 通过锁提供对对象的同步访问；Arc，即原子引用计数指针，使用引用计数管理生命周期，让多个线程安全共享这个 mutex。

在一个小例子中，我们创建 10 个线程，并为每个线程显式 clone 一个 Arc。每个副本的所有权移入对应线程；线程取得 mutex 后，可以修改底层对象。线程会竞争获取锁，但客户端代码仍是普通的安全 Rust。

这些库扩展了安全客户端能够表达的行为。它们的内部实现不能全部遵守核心安全约束：它们使用 unsafe 代码，包括解引用原始指针等操作，而类型系统并不追踪这些指针的别名。

这些不安全的细节承诺由安全接口封装。使用安全语言子集编写的客户端，不应通过这些 API 观察到未定义行为。这是一个强而有价值的承诺，但也为隐蔽的 bug 留下空间。

大约在 2015 年，Aaron Turon 介绍无畏并发，并重点展示一个 scoped-threads API，让新建线程借用父线程栈帧中的数据。这个 API 内部使用 unsafe 代码。文章发布前后发现了一个 bug，当时距离 Rust 1.0 发布大约只有两周。

问题涉及它与引用计数 API Rc 的交互：虽然每个 API 单独看似乎安全，组合使用却可能导致释放后使用。scoped-threads API 因此被弃用，后来又开发了其他方案。我们怎样才能确信这类健全性 bug 不会出现？

RustBelt 旨在为 Rust 核心语言建立逻辑基础，验证其类型系统和重要库，并为开发者提供评估未来 API 的方法。目标是在语言持续发展的同时，保持对其安全性的信心。

安全证明意味着什么？传统的语法方法通常称为进展与保持，它把良类型的概念从程序推广到机器状态，并证明执行过程会保持这一性质。如果程序符合固定的一组类型规则，这种方法可以简单地证明行为有定义。

对于这里描述的 Rust，这种方法还不够：库实现可能有意包含安全类型规则之外的代码。RustBelt 转而使用语义安全。非正式地说，如果没有任何良类型客户端能利用一个库产生未定义行为，这个库就是安全的。

什么算未定义行为，本身仍是活跃的研究问题。在这项工作中，模型包括不访问未分配的内存，以及按照某个操作性定义避免数据竞争等条件。确切保证取决于证明所使用的形式语义。

团队定义了一个名为 LambdaRust 的核心演算，以 Rust 的中级中间表示为蓝本。它的操作语义可能卡在不良状态；安全定理表明，在这个模型中，适当的良类型程序不会到达这种状态。

一位听众问，能否把经过验证的原语加入语法证明。难点在于找到一种可扩展的方法，使新增 API 时不必修改所有已有证明。语义安全允许我们针对共享模型独立证明一个新 API。

语义模型将类型或 API 接口映射到安全契约，即实现必须满足的验证条件。我们为类型系统统一定义这种解释，它告诉我们：实现能够安全地与其他代码链接之前，必须证明什么。

我们证明一个一般定理：完全处于安全子集中的实现，按照构造就满足相应契约。使用 unsafe 特性的实现则需要额外的手工证明，表明它满足契约。证明可能很困难，但至少验证义务是明确的。

我们的工作重点是这个框架、Rust 的一个有意义的子集和若干广泛使用的 API，而不是完全自动化。未来的验证工具可能让证明更系统化。在工作过程中，我们确实发现了几个 bug，包括 Mutex 中的一个问题，以及 Arc 中与弱内存有关的一个问题。

共享语义模型使各个库的证明可以相互独立。对于前面提到的 Rc 和 scoped-threads 交互，其中一个实现在选定模型下会验证失败。我们在模型中考虑并验证了 Rc；有问题的 scoped-threads API 则无法通过该证明。

结果始终以我们定义的内存模型为前提。最初的模型相对简单，并不完全符合现实。忠实的模型既要考虑 Rust 开发者的意图，也要考虑如何安全编译到 LLVM；这仍是一个开放问题。

我们还在研究一个更丰富的模型，它允许更多未定义行为，以支持编译器优化。但在本次演讲时，RustBelt 尚未适配这个模型。理解形式化安全结果的适用范围时，这一区别很重要。

语义模型具有灵活性。一些更大胆的新 API 可能无法在当前解释下得到验证，因此框架必须持续演进。这些证明在 Coq 中经机器检查：修改模型仍需工作，但 Coq 会指出已有证明中需要调整的地方。

整个项目有多个可调整的参数：语言及其语义、类型的解释、所验证的 API 和内存模型。我们的论文使用了具有顺序一致并发语义的 Rust 核心片段；让各部分更贴近现实仍是持续的工作。

接下来的问题是：用哪种逻辑表达这些契约？我们使用分离逻辑的一个衍生版本。Hoare 逻辑通过前置条件、后置条件和不变量推理代码；分离逻辑对它进行扩展，以便有效推理操作指针的程序。

它与 Rust 的契合点是所有权。在分离逻辑中，断言描述对资源的所有权，这与 Rust 类型系统的核心思想相呼应。不过，对于并发语言，我们需要逻辑的并发扩展，而这样的扩展有很多种。

一篇 2010 年的论文指出一个令人不安的趋势：每出现一个新库或并发原语，似乎就需要一种新的分离逻辑。如果每个新 API 都要求替换底层逻辑，一个所谓通用的语义模型就无法扩展。我们希望有一个框架，可以从中推导更强的推理原则。

第二个挑战是内存模型。早期许多并发分离逻辑假设顺序一致性，仿佛线程轮流修改全局状态，每次修改都会立即可见。实际并发和 C++ 风格的原子操作允许更复杂的弱内存行为。

我们的工作沿着两条路线展开：一条是统一并发分离逻辑的 Iris 框架，另一条是考虑弱内存的逻辑。后续工作也将一系列弱内存逻辑编码进 Iris。这个框架在 Coq 中实现，并能适用于不止一种语言或内存模型。

快速介绍 Hoare 逻辑：一个三元组包括命令 C、前置条件 P 和后置条件 Q。如果 P 在初始状态成立，C 就能安全执行；如果它终止并返回值，结果就满足 Q。这是部分正确性陈述，不保证每个命令都会终止。

分离逻辑改变了断言的含义。断言 x 指向 v 表示当前线程拥有这个位置，且其中存放 v。所有权意味着线程可以在不受其他链接线程干扰的情况下，推理并修改该位置。

分离合取 P * Q 表示两个断言分别作用于互不重叠的状态。对物理内存而言，x 指向 v * y 指向 w 描述不同的位置：x 和 y 不是别名。这明确划出了两个线程资源之间的边界。

不相交并发规则指出：如果两个并行命令各自操作自己的资源，我们就可以独立验证它们，再用分离合取组合前置条件和后置条件。如果初始断言确立了独立所有权，一个线程修改 x、另一个线程修改 y，就不会相互覆盖。

共享状态需要另一条规则：不变量。我们为共享状态建立性质 R，允许原子命令临时访问它，但操作后必须恢复 R。不变量在操作开始时是一个假设，在结束时则是一项保证。

原子性很重要，因为其他线程不能在不变量暂时失效时观察它。如果一个多步操作先把偶数变成奇数，再改回偶数，另一个线程可能在中途介入，发现原先假设的性质已经不成立。

在简化的 mutex 中，我们用一个位置表示锁：未锁定时值为 0，锁定时为 1。lock 方法循环执行原子比较并交换，直到将 0 改为 1；unlock 则把该位置设回 0。

用 P 描述 mutex 保护的资源。任何人都可以在一个无实质限制的前置条件下调用 lock；lock 终止后，调用者获得 P。要 unlock，调用者必须归还 P，此后不再拥有它。这个规范与 P 代表的具体资源无关。

两个线程都可以分别获取锁，在临界区使用 P，恢复它后解锁。每个线程的证明都可以独立进行。mutex 的共享不变量将锁的物理状态与受保护资源的所有权联系起来。

不变量有两种情况：x 指向 0 时，锁空闲，不变量持有 P；x 指向 1 时，锁已被持有，P 已转移给某个线程，该线程在持锁期间可以暂时修改受保护状态。

要证明成功获取锁，可以在未锁定的情况下打开不变量，暂时取得 x 指向 0 以及 P。原子比较并交换将 0 改成 1。随后用 x 指向 1 恢复不变量，并把 P 保留为后置条件。

这个简化介绍省略了重要细节，但展示了证明模式。在 Coq 中，这种证明是交互式的：将针对独立资源的规则与访问、恢复共享不变量的规则组合起来。

基本的并发分离逻辑很强大，却不能方便地表达我们需要的所有性质。共享计数器只增不减，是关于状态如何演化的陈述，而不只是单个状态的性质。协议还可能要求说明特定时刻哪个线程有权修改某项内容。

高级逻辑使用权限、令牌或能力等逻辑状态，描述参与者可以承担的角色。许多此类扩展不断出现，原始规则也越来越复杂。每种逻辑往往有独立的健全性模型，因此很难组合在不同逻辑中证明的结果。

Iris 试图建立更基础的共同框架。它的核心要素是不变量和用户定义的逻辑状态，也叫幽灵状态。通过这些要素，我们可以推导复杂并发逻辑的规则，并针对具体应用开发新的推理原则。

在 RustBelt 中，我们需要一个借用命题，表示在某个生命周期内临时拥有资源，之后原所有者重新取得控制权。我们没有另造一套逻辑，而是在 Iris 中把它编码为逻辑 API，证明其健全性，再用它构建 Rust 的语义模型。

回到 Arc：一个简化对象包含数据和引用计数。clone 以原子方式增加计数并返回别名；print 访问数据；drop 减少计数，如果这是最后一个引用，就释放对象。这个例子用于说明原理，并非 Rust 的 Arc 的精确实现。

RustBelt 为每个类型关联一个谓词，描述拥有该类型值的含义。这里的 Arc(x) 表示通过句柄 x 访问共享数据的权限。每个方法都以该权限开始：clone 返回 Arc(x) * Arc(y)，print 保留 Arc(x)，而 drop 消耗该权限。

clone 的规范看起来有些奇怪。返回的 y 是 x 的别名，所以两个谓词指向同一个物理对象。分离合取怎么还能适用？答案是，这些谓词描述的是逻辑上彼此独立的权限，而不是对不同物理内存的独占所有权。

每个 Arc 权限都是可计数的权利，可以传给一个线程而不干扰另一份权限。这类权利的数量必须与对象的引用计数一致。另一个逻辑谓词 Count(x, n) 记录当前有多少份 Arc 权限。

如果 Count(x, n) 和一份独立的 Arc(x) 同时成立，n 必须大于 0：后者证明至少存在一份权限。一次逻辑更新可以将计数从 n 增至 n + 1，同时创建一份权限；也可以消耗一份权限并减少计数。

不变量将逻辑状态与物理状态联系起来。对于某个 n，逻辑计数为 n；要么 n 为 0，要么对象仍已分配且物理计数为 n。n 为 0 时，对象已经释放。不变量使两种描述保持一致。

每个方法都以 Arc(x) 开始。将它与不变量中的 Count(x, n) 结合，就可推知 n 至少为 1，因此对象仍已分配，方法可以访问 x。以 clone 为例，它执行一次原子读取并递增操作。

为原子操作打开不变量。举个具体例子，假设当前计数为 2。证明过程暂时取得物理状态的所有权，并将计数改为 3。随后需要恢复不变量，但逻辑计数仍然是 2。

使用逻辑更新将计数也改为 3，同时生成另一份 Arc 权限。物理状态和逻辑状态现在一致，可以恢复不变量。新权限保留在后置条件中，正好满足 clone 规范的要求。

这遵循熟悉的并发分离逻辑模式：打开不变量、操作状态，再恢复不变量。新增的一步是同时操作逻辑状态。证明依赖关于该状态的规则，因此这些规则本身也需要得到论证。

Iris 提供一个框架，用于论证特定应用的逻辑状态规则。一种称为偏交换幺半群的通用代数结构可以表示选定的逻辑状态。从少量原始证明规则出发，可以推导出示例中高层公理的健全性。

RustBelt 利用这些思想对 Rust 类型建模，验证由 unsafe 内部实现构建出的安全抽象。Iris 提供灵活的现代分离逻辑，用来表达语义模型，并在形式模型的范围内将推理扩展到现实的 Rust 代码。