Page 196 - 《软件学报》2025年第8期

张卓若 等: 面向 Rust 语言的形式化验证方法研究综述 3619

序正确性推理系统, 自提出以来已成为所有程序验证系统的核心基础. 它基于霍尔三元组{P}C{Q}刻画程序行为,
C 是所验证的程序, P 和 Q 通常都是一阶逻辑里的公式, 用于描述程序 C 里的程序变量需满足的约束条件, 其中
P 称为前置条件 (precondition), Q 称为后置条件 (postcondition). 分离逻辑 (separation logic) 的目标是在霍尔逻辑的
基础上支持验证访问堆内存的程序. 它引入指向运算符 7→, x 7→ y 表示 x 的值对应的地址, 在堆上对应的值等于 y
的值. 而其难点在于同一个内存地址可以被多个指针所指向, 当一个指针指向的数据被修改时, 有关其他指向该地
址的指针的程序断言可能不再成立, 从而使证明难以进行. 分离逻辑的解决方法是在程序断言中引入分离合取
(separation conjunction), P1∗P2 来表示程序断言 P1 和 P2 各自描述了一块符合对应断言的内存, 且各自的内存地
址是没有重叠的. 如 x 7→ 1∗y 7→ 2 可以理解成两个指针 x 和 y 和各自指向的值为 1 和 2, 且 x 和 y 指向不同的地
址. 这样就避免了不同的断言之间有共享的地址, 在使用一部分断言和其对应的内存进行证明的时候, 程序对内存
的影响就不会改变其他断言的成立性. 基于此, 分离逻辑最大的优点之一就是可以很有效地支持局部推理, 得益于
该逻辑特有的框 (Frame) 规则.

Γ ⊢ {P}c{Q}
c不使用R中的变量和内存
.
Γ ⊢ {P∗R}c{Q∗R}
Frame 规则结论中的前后条件分别都分离合取了同一个断言 R, 如果程序 C 不会对 R 所描述的那部分程序状
态与内存进行修改, 那么证明 C 的过程中可以不使用断言 R, 因而其前提是一个前后条件为 P 和 Q 的霍尔三元组.
这样一种将不需要用到的内存的断言从霍尔三元组中暂时移除的方式, 既使得模块化的证明更为简洁, 又保证了
可以证明一个程序不会访问禁止其访问的内存. 如此, 在分析验证局部程序时只需考虑该局部程序所访问的内存
区域, 而不需要涉及全局状态.
然而, 分离逻辑对用户和工具都有较高的要求, 使得其在实际应用中的普及受到限制. 用户需要自定义丰富的
断言来描述程序的行为, 包括指向性谓词、分离合取等, 这要求用户有深入的理解才能编写出准确的规范, 导致这
些逻辑的应用主要局限于专家研究者的小圈子内. 此外, 在基于分离逻辑的证明过程中, 为了确保内存安全需要详
细追踪资源的使用情况和内存的状态, 这不仅增加了证明的复杂性, 也对自动化工具提出了更高的要求. 现代形式
化验证工具, 如 SMT (satisfiability modulo theories) 求解器 [47] , 已经在处理命题和一阶逻辑问题上取得了巨大进步.
相比之下分离逻辑的自动化验证仍处于起步阶段, 且面临更大的技术挑战, 因为分离逻辑通常涉及比普通逻辑更
复杂的计算复杂性类别. 在这一背景下, Rust 语言以其独特的类型系统和所有权规则, 为形式化验证提供了新的视
角. Rust 的所有权模型在语言层面上内置了分离逻辑的思想, 对指针别名实行了严格的规范. 例如, 在 Rust 中声明
两个类型相同的变量 x 和 y 时, Rust 所有权模型保证它们天然就是分离的. 此外, 指向堆分配内存的智能指针
Box<T> 提供了表达“指向”关系的谓词, 这在分离逻辑中是至关重要的. 从某种意义上说, Rust 的类型检查器在每
次编译时都执行一种分离逻辑证明. 因此, Rust 允许在验证时依赖 Rust 的类型系统来实现类似分离逻辑的精确推
理, 捕获关于内存位置的关键信息, 包括别名、副作用、Frame 规则和是否存在数据竞争等, 同时避免了繁琐和困
难的资源追踪过程. 如此, 设计和使用自动化工具时就可以将注意力集中在要证明的核心功能属性上, 例如功能正
确性. 这对于提高验证效率和准确性具有重要意义, 也使得用户体验更友好. 当然, 为了分析 Rust 程序, 还需要做
额外的扩展. 例如, 借用机制的引入尽管为 Rust 带来了灵活性, 但也为分离逻辑的 Frame 带来了挑战. 当创建一个
可变引用 x=&mut y 时, y 的值似乎可以通过两种方式访问, 这在分离逻辑中需要特别处理, 以避免别名问题对证
明过程的影响.
例如, 图 10 中包含可变借用的例子就展示了 Rust 类型系统所提供的安全保证简化了程序验证问题. 假设 p0
和 p1 是两个 Point 实例, 传入 align 函数中分别表示为 segm.0 和 segm.1. 为了证明 align 函数调用中的断言, 必须
确保几个关键属性得到满足: (1) 调用 shift_x 会将 p1 的 x 字段的值增加 s 值, 这是实现功能性正确性所需的后置
条件. (2) 这个调用不会影响 p0 的 x 字段, 因此调用结束后, p0.x 将等于 p1.x. (3) shift_x 的调用不会更改传入的
segm 元组, 这意味着调用后 p0 和 p1 仍然分别等于 segm.0 和 segm.1, 从而保证了 (*segm.0).x 与 (*segm.1).x 的值
相等. (4) 代码是无数据竞争的, 这确保了在整个执行过程中所有内存位置的值保持稳定. 而这些属性中的 (2)–(4)