形式化验证（Formal Verification），是用形式化语言描述一个对象，通过严格的数学方法，证明该对象具有某种性质（安全性、正确性、稳定性等）。

这篇文章，我打算用Verus验证的例子，来讲一下‘定理证明’这个技术分支。Verus[1]这个项目，是一个很年轻的形式化验证工具，2023年出现的，论文[3]发表在OOPSLA’23。在接下来的2年内得到大量关注，OSDI’24会议有2篇best paper都使用了Verus验证。Verus是专为Rust设计的，’verifying the correctness of code written in Rust’。

一个简单的例子

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

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
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!

回顾文章开头的那句话：形式化验证（Formal Verification），是用形式化语言描述一个对象，通过严格的数学方法，证明该对象具有某种性质（安全性、正确性、稳定性等）。在这个例子中，

  • 对象：要验证的对象是，min()这个函数。
  • 形式化语言：就是Rust语言。第5~11行，用Rust这种“形式化语言”描述了min()函数的功能。
  • 性质：证明这个对象具有的性质，是第14到18行的一系列assert。大家一般把assert翻译为“断言”。比如这一句断言，assert(forall|i: int, j: int| min(i, j) <= i && min(i, j) <= j); 它的意思是，对所有整数i和j，min(i,j)一定小于等于i，且小于等于j。这属于一种“功能正确性”。这个验证的目的是，确保min()这个函数的功能实现是正确的。

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

在assert中，forall|i: int, j: int，意思是所有的任意的整数i和j，后面的性质都成立。咱们平时做测试的时候，一般做法是，写几个测试用例，就像第14、15行的做法一样，只要这几个测试用例结果是正确的，这个函数测试就算通过了。那么，Verus是如何证明，对所有可能的i和j，min()这个函数都是正确的呢？

Verus的做法是，把程序转换成SMT-LIB的表示，然后给Z3求解器[4]求解，最终得到性质‘满足’或者‘不满足’的结论。以代码中的交换律性质为例，也就是以下这句断言，
assert(forall|i: int, j: int| min(i, j) == min(j, i));
它的意思是，对所有的i和j，min(i,j) 总是等于 min(j,i)。Verus是如何证明这一点的呢？
如果在命令行中运行Verus工具，验证getting_started.rs，并加上–log-all参数，就可以在.verus-log目录下，看到很多中间过程的日志文件。root.smt_transcript这个文件中有SMT求解器输入和输出日志。以下截取了其中关键的一部分。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
;;;>>> QUERY
(push)
(declare-const no%param Int)
(declare-const tmp%1 Bool)
(assert
  fuel_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%%0
     tmp%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求解找到一组解，使得min(i,j)不等于min(j,i)。Z3的RESPONSE是unsat，不满足，也就是不存在满足‘交换律不成立’这个命题的解。因此原命题‘交换律’是成立的。

求解器算法本身是一个很大的技术分支，微软研究院开发的Z3是最流行的求解器，在此就不展开了。Verus只需要用Z3就可以。Verus的作用是，把Rust代码实现（getting_started.rs这个例子缺少了可执行的代码实现部分），和用Rust表示的specification和property，转换成Z3求解器能处理的形式。

当Z3求解器解不出来的时候，Verus还能通过增加中间的引理(proof code)，使得最终能够完成证明，增加这些中间的proof代码，是需要专家人工参与的。这部分功能是基于定理证明的。因此Verus不是一种纯粹的‘定理证明’类工具，而是一种基于Z3做了部分证明自动化的，定理证明工具。

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

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

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

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

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

1
2
3
4
5
6
7
8
9
#[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很突出的亮点之一。

参考文献

  1. Verus，https://github.com/verus-lang/verus
  2. Verus Playground，https://play.verus-lang.org
  3. Verus: Verifying Rust Programs using Linear Ghost Types, https://www.andrew.cmu.edu/user/bparno/papers/verus-ghost.pdf
  4. Z3Prover, https://github.com/Z3Prover/z3
  5. Asterinas，https://github.com/asterinas/asterinas
  6. Formal Verification of Asterinas with Verus，https://github.com/asterinas/asterinas-fv-preview

PS: 今天是除夕，顺祝新春快乐！蛇年大吉！:)