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

徐家乐 等: 操作系统内核权能访问控制的形式验证 3573

持并行组合和并发上下文精化关系的验证. 在此基础上, Xu 等人提出了以分离逻辑为基础的并发精化程序逻辑
CSL-R, 并用该逻辑验证了带中断和抢占的商业化实时嵌入式操作系统内核µC/OS-II 的核心功能模块 [7,9] . Sanán
等人提出了一个基于依赖保证 (rely-guarantee) 的验证框架 [8] , 用于验证事件触发的并发系统, 使用该框架验证了
Zephyr 实时操作系统的内存管理模块 [18] . 最近的工作中, 他们在 Isabelle/HOL 中验证了 L4 微内核 API 的功能正
确性 [19] . 以上工作都没有专门针对权能访问控制的形式建模和验证.

2 基础知识

本文的形式验证基于并发精化分离逻辑 CSL-R, 在 Coq 定理证明器中进行. 下面就这两方面的基本知识进行介绍.

2.1 Coq 定理证明
应用交互式定理证明进行形式验证的基本思路是: 首先, 在定理证明器中建立程序语言的语法、语义和推理
系统, 建立形式模型; 然后, 对待验证系统实现的正确性和安全性质进行逻辑刻画, 定义形式规范; 最后, 基于推理
系统验证形式模型满足对应的形式规范. 常见的定理证明器有 Isabelle [20] , Coq [21] , PVS [22] , Lean [23] 等. 定理证明器的
可信性源于形式化证明是可以机械检查的 (machine checked), 而用于公理的元逻辑系统本身规模很小, 构成了形
式验证所依赖的最小信任基. 在应用过程中, 不推荐用户直接加入公理, 用户直接定义程序的语法和语义, 而推理
规则的有效性则是基于元逻辑证明系统, 证明推理规则和语义的一致性来得到. 本文所使用的 Coq 是主流的定理
证明工具之一, 基于归纳构造演算 (calculus of inductive constructions, CIC) 类型理论而实现. Coq 采用可计算函数
逻辑 LCF (logic for computable functions) 方法, 利用“命题即类型、证明即项”的思想, 使类型化的项既可以表示逻
辑定理, 又可以表示证明, 并通过依赖类型、多态等特性实现推理与证明. Coq 不仅被用于形式化验证数学定理,
如著名的四色定理, 而且还成功地应用于系统可靠性验证, 包括操作系统和编译器等 [3,4,7] .
Coq 证明系统中主要使用 Inductive 关键字定义数据类型, Definition 关键字定义标识符和函数, 支持的验证策
略包括 destruct, simpl, auto, eauto 等. 其中 destruct 是分类规约, 将待证明命题中的变量分成多种基本情况进行讨
论. simpl 可以将目标或者前提进行简化, 但需要注意的是, 当命题中存在复杂定义的时候, simpl 可能会展开该定
义, 反而增加了命题复杂度和证明难度. discriminate 是矛盾规约, 假设前件中的多个前提存在矛盾的情况, 根据蕴
含关系 p 为假则命题为真, 可以直接得到待证命题为真. 而 auto 策略是一种自动化证明策略, 它可以重复若干适
用于该命题的定理, 从而对于命题的多个子目标采用统一的策略进行证明, 大大降低了命题证明的难度; eauto 会
在 auto 功能之上尝试对目标中的存在变量进行赋值. 除此之外, Coq 中还可以自定义 Ltac 策略, 对相似的证明目
标进行自动化验证处理.

2.2 并发精化程序逻辑 CSL-R
并发精化程序逻辑 CSL-R (concurrent separation logic with refinement) 由 Xu 等人 [7,9] 提出, 用于对带并发和中
断的操作系统内核的功能正确性验证. 它对并发分离逻辑 [10,11] 进行扩展, 加入并发程序模拟关系 RGSim [16,17] 中对
共享资源的依赖保证条件和上下文精化关系的概念, 同时实现并发程序的可组合和精化关系的验证.
CSL-R 基于临界区机制管理并发程序之间共享的资源, 实现任务对共享资源的互斥访问. 它沿用并发分离逻
辑 [11] 的以下规则, 对并发程序语句 ENTER_CRITICAL; c; EXIT_CRITICAL 进行验证:
{P∗ Inv}c{Q∗ Inv}
,
{P}ENTER_CRITICAL;c;EXIT_CRITICAL{Q}
其中, P、Q 和 Inv 均为分离逻辑公式 [10] , P 和 Q 分别表示 c 所在线程局部资源满足的前后条件, Inv 表示全局共享
资源满足的不变式. 分离合取*表示局部资源和共享资源是不相交的. 以上规则表示, 进入临界区后, c 拿到全局资
源 Inv 的唯一使用权, 当 c 执行完成后, 需要重新建立起全局资源不变式 Inv, 并在退出临界区后返还. 全局不变式
Inv 一般用于刻画共享资源的良构性质以及不同资源之间的关系. CSL-R 用于验证操作系统内核实现和抽象规范
之间的精化关系, 它的不变式 Inv 同时描述底层实现和高层抽象规范所对应的共享资源以及它们之间满足的一致
关系, 该关系在临界区外总是保持成立, 可以看作 RGSim 中所提出的环境和系统的依赖保证关系的特殊情况. 图 1