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

3574 软件学报 2025 年第 36 卷第 8 期

表示 P 是 s 的精化时 P 一步执行的情况, 当 P 执行一步操作时, 存在 s 的多步执行 (包括 0 步执行) 与其对应, 它
们的状态之间满足不变式 Inv.

1
P, σ P′, σ′

Inv Inv Inv Inv

1 1 *
s, Σ s1, Σ1 s2, Σ2 sk, Σk
E
E
图 1 精化一致性关系 E

CSL-R 已经在 Coq 定理证明器中实现, 并用于带中断和抢占的操作系统内核 µC/OS-II 核心功能模块的验
证 [7,9] . 我们下面从建模、断言规范、推理规则这 3 个方面来简单介绍 CSL-R. CSL-R 提供类 C 语言和汇编原语
对底层 C 语言内嵌汇编的内核实现进行建模, 可以很方便地将 C 代码逐行翻译到 CSL-R 语法. 同时, 它提供高层
抽象规范语言, 建立 API 函数的抽象规范. 抽象规范语言中最基本的抽象操作形式为 γ(vl), 其中 γ 为名字, 参数 vl
为值列表, 表示高层状态到返回值和高层状态的原子转换; end v 表示当前 API 函数执行结束并返回值 v; s1??s2 和
s1;; s2 分别表示不确定选择和顺序执行等. CSL-R 使用分离逻辑来定义断言, 本文中用到的断言主要有以下几种
(这里使用 CSL-R 在 Coq 中的实现形式).
,
t
● G&x@t == l L&x@t == l, 分别表示全局变量或局部变量 x 类型为 且它们的地址值为 l;
t
● PV l@t| → v, 表示地址 l 处存储的值类型为 且值等于 v;
● < ||op|| >, 其中 op 是一个抽象规范语句, 表示高层还未执行的剩余代码为 op. CSL-R 允许在断言中表示高
层抽象规范执行的情况, 对应底层实现的执行, 这是验证底层实现和高层规范之间精化关系的关键;
● [|P|], 表示 P 是一个与状态无关的纯逻辑公式;
● P∗∗Q 以及其他的一阶逻辑复合公式. 其中, 分离合取 P∗∗Q 表示, 内存可以分为两个不相交的部分, P 和 Q
分别在这两部分上成立.
基于以上断言语法, CSL-R 定义了结构体、数组和链表的数据结构断言. 在本文中, 我们将对其进行扩展, 对
权能的复杂数据结构进行建模.
CSL-R 中操作系统内核的正确性归结为, API 函数的实现是其抽象规范的精化, 而抽象规范需要足够表达内
核设计的正确性需求. API 函数调用内部函数来实现功能, 相应地, API 函数的正确性依赖于内部函数的正确性.
针对内部函数的验证, 由于它有权限访问全局共享资源, 因此, 内部函数的前后条件规范分别描述局部资源和全局
资源在函数执行前的初始情况和函数执行后修改的情况, 以及参数、局部变量和返回值的情况. 针对 API 函数的
验证, 它没有权限访问全局共享资源, 因此它的前后条件中包括参数、局部变量和返回值的情况以及实现所需要
精化的高层抽象规范执行的情况, 具有如下的形式:

{OS [ ¯ 0,1,nil,nil]∗∗Init(¯v)∗∗EX(lv)∗∗[|ω(¯v)|]}
s
⌢
⌢
{λv.OS [ ¯ 0,1,nil,nil]∗∗EX (lv)∗∗[|endv|]},
′
其中, OS 断言表示 API 调用时, 中断处于打开状态, 且该调用不位于任何中断处理程序内或者临界区内. ¯ v, lv 分
别表示函数的参数和局部变量. 函数调用前, 参数和局部变量分别满足初始条件 Init 和 EX, 待执行的抽象规范为
⌢
ω, 与底层函数调用具有同样的参数值; 底层函数调用结束后, 返回值为 v, 同时高层规范执行完毕, 返回同样的值.

3 权能访问控制的设计

本文中所考虑的权能访问控制, 是通过在航天嵌入式领域某微内核操作系统上提供插桩式模块实现的. 它提