用Verus进行Rust程序的形式化验证

用Verus进行Rust程序的形式化验证

形式化验证（Formal Verification），是用形式化语言描述一个对象，通过严格的数学方法，证明该对象具有某种性质（安全性、正确性、稳定性等）。
这篇文章将通过Verus验证的例子，介绍‘定理证明’这个技术分支。Verus是一个专为Rust设计的形式化验证工具，2023年出现，其相关论文发表在OOPSLA’23。在接下来的2年内得到大量关注，OSDI’24会议有2篇best paper都使用了Verus验证。Verus的主要目标是验证Rust代码的正确性。

一个简单的例子

让我们从Verus Tutorial中的第一个例子getting_started.rs着手，理解Verus的证明原理。

use vstd::prelude::*;
verus! {
    spec fn min(x: int, y: int) -> int {
        if x <= y { x } else { y }
    }
    fn main() {
        assert(min(10, 20) == 10);
        assert(min(-10, -20) == -20);
        assert(forall|i: int, j: int| min(i, j) <= i && min(i, j) <= j);
        assert(forall|i: int, j: int| min(i, j) == i || min(i, j) == j);
        assert(forall|i: int, j: int| min(i, j) == min(j, i));
    }
} // verus!

在这个例子中：

• 对象：要验证的对象是min()这个函数。
• 形式化语言：就是Rust语言。第5~11行，用Rust这种“形式化语言”描述了min()函数的功能。
• 性质：证明这个对象具有的性质，是第14到18行的一系列assert。比如这一句断言：

  assert(forall|i: int, j: int| min(i, j) <= i && min(i, j) <= j);
  

  它的意思是，对所有整数i和j，min(i,j)一定小于等于i，且小于等于j。这属于一种“功能正确性”。

这个例子可以直接在Verus Playground里运行。

在assert中，forall|i: int, j: int，意思是所有的任意的整数i和j，后面的性质都成立。通常做法是写几个测试用例，而Verus是如何证明，对所有可能的i和j，min()这个函数都是正确的呢？

Verus的做法是，把程序转换成SMT-LIB的表示，然后给Z3求解器求解，最终得到性质‘满足’或者‘不满足’的结论。以代码中的交换律性质为例：

;;;>>> QUERY
(push)
(declare-const no%param Int)
(declare-const tmp%1 Bool)
(assertfuel_defaults)
(declare-const %%location_label%%0 Bool)
(assert(not (=>(= tmp%1 (forall ((i$ Poly) (j$ Poly)) (!(=>(and(has_type i$ INT)(has_type j$ INT))(= (getting_started_02!min.? i$ j$) (getting_started_02!min.? j$ i$))):pattern ((getting_started_02!min.? i$ j$)):pattern ((getting_started_02!min.? j$ i$)):qid user_getting_started_02__main_0:skolemid skolem_user_getting_started_02__main_0)))(=>%%location_label%%0tmp%1))))
(get-info :version)
;;;<<<
;;;>>> RESPONSE
(:version "4.12.5")
;;;<<<
;;;>>> QUERY
(set-option :rlimit 30000000)
(check-sat)
;;;<<<
;;;>>> RESPONSE
unsat
;;;<<<

从assert部分开始，是需要Z3证明的断言。它的意思是：对于所有类型为Poly的变量i和j，i和j的类型都是INT，那么 (getting_started_02!min.? i$ j$) 等于 (getting_started_02!min.? j$ i$)，也就是交换律成立，min(i,j) = min(j,i)。注意：整个断言外面包裹了一个 not，表示否定。意思是，交换律不成立。把这个断言交给Z3，请它check-sat。Z3的RESPONSE是unsat，不满足，也就是不存在满足‘交换律不成立’这个命题的解。因此原命题‘交换律’是成立的。

用Verus验证Asterinas OS中的内存管理模块

接下来看一个比较复杂的例子。Asterinas是一个开源项目，用Rust写操作系统，它有一个设计亮点是，frame kernel。我们与CertiK合作，试图对Asterinas做形式化验证，确保它是一个memory safe的操作系统。

我们首先从mm模块（memory management）开始验证，从大的验证目标，拆分到很多个小的验证目标（formal verification target）。这部分预览代码已公开，展示的是target10和target11这两个针对cursor功能正确性验证的代码。

• 对象：要验证的对象是，cursor模块。
• 形式化语言：用Rust语言描述了cursor模块的功能，model.rs文件就是cursor的模型描述，称为ConcreteCursor。
• 性质：证明cursor模块的功能是正确的，体现在mod.rs文件中的一系列asserts。

验证代码通过relate这个方法，把模型和实现连接在一起，确保模型与实现是一致的。例如下面这段代码：

#[rustc_allow_incoherent_impl]
pub open spec fn relate(self, model: ConcreteCursor) -> bool
recommends
model.inv(),
{
    &&& self.level == NR_LEVELS() - model.path.len()
    &&& self.va == model.path.vaddr()
    &&& self.relate_locked_region(model)
}

self.va == model.path.vaddr() 表示实现过程中virtual address总是与mode的vaddr保持一致。证明过程中，人工添加了很多引理，使得Verus能够完成最终的证明，这属于‘定理证明’的方法。

Verus的特点

最后简单总结一下Verus这个验证工具的特点:

• Verus直接用Rust作为描述specification的语言，因此对开发者非常友好。开发者不需要再学习另一种形式化语言，比如Coq和Isabelle之类的，大大降低了形式化验证的门槛。
• Verus深度集成了Rust的linear type和borrow checking能力，能够直接验证与内存安全相关的属性。这使得它在验证Rust程序时更加自然和高效。
• Verus基于SMT求解器（如Z3），提供了比较高效的自动化验证能力，相比一些传统的交互式定理证明工具，它减少了验证工程师的工作量。
• Verus支持对unsafe rust code做验证，而很多rust验证工具不支持，这是Verus很突出的亮点之一。