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

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

1
(Key Laboratory of System Software (Institute of Software, Chinese Academy of Sciences), Beijing 100190, China)
2
(State Key Laboratory of Computer Science (Institute of Software, Chinese Academy of Sciences), Beijing 100190, China)
3
(National Key Laboratory of Space Integrated Information System (Institute of Software, Chinese Academy of Sciences), Beijing 100190,
China)
4
(University of Chinese Academy of Sciences, Beijing 100049, China)
5
(Huawei Technologies Co. Ltd., Beijing 100085, China)
6
(Beijing Institute of Control and Electronic Technology, Beijing 100038, China)
7
(School of Computer Science, Peking University, Beijing 100091, China)
Abstract: Operating system (OS) kernels serve as the foundation for designing safety-critical software systems. The correct functioning of
computer system depends on the correctness of the underlying OS kernels, making their formal verification a critical task. However,
behaviors such as multi-task concurrency, data sharing, and race conditions inherent in OS kernels pose significant challenges for formal
verification. In recent years, theorem-proving methods have been widely applied to verify the functionality of OS kernel modules,
achieving notable successes. The capability-based access control module in OS kernels provides fine-grained access control, designed to
prevent unauthorized users from accessing kernel resources and services. Its implementation involves capability spaces for tasks, which
form a set of tree structures. Each capability node includes nested, complex data structures and capability functions frequently perform
operations such as access, modification, and recursive deletion of capability spaces. These factors make the formal verification of capability-
based access control significantly more challenging compared to other OS modules. This study employs concurrent separation logic with
refinement (CSL-R) to verify the functional correctness of a capability-based access control module in the aerospace embedded domain.
The verification establishes refinement between the API functions of the capability module and their abstract specifications. First, the
capability data structure is formally molded, followed by the definition of a global invariant to ensure the consistency of capability spaces.
Next, the preconditions and postconditions for internal functions and the abstract specifications for API functions are defined to reflect
functional correctness. Finally, the refinement between the C implementation of the API functions and their abstract specifications is
rigorously proven. All definitions and verification steps are formalized using the Coq theorem prover. During the verification process,
errors are identified in the C implementation, which are subsequently confirmed and corrected by the OS kernel designers.
Key words: operating system kernel; formal verification; capability-based access control; concurrent separation logic with refinement (CSL-R)

软件系统是现代信息社会的基础设施, 其安全可靠性是安全攸关领域计算机系统设计的首要需求. 而计算机软
件在操作系统的基础上运行, 这些软件能否正确地提供服务不仅依赖于软件本身的正确性, 还依赖于底层操作系统
的正确性. 操作系统内核提供操作系统最基本的功能, 任何一个小的错误都可能造成整个上层软件系统的崩塌. 形
式化建模与验证方法广泛应用于计算机软硬件系统的正确性保障, 被认为是开发高可靠软件系统的有效方法 [1,2] .
近年来, 基于交互式定理证明的形式验证方法被成功应用于操作系统内核的正确性验证中 [3–8] . 操作系统内核提
供给应用软件层一系列 API (application programming interface, 应用程序接口) 函数, 应用层通过调用 API 函数来控
制程序的运行, 而不触及操作系统内核实现的具体细节. 在文献 [3–8] 中, 操作系统的正确性被定义为 API 函数的具
体实现和抽象规范之间的精化关系, 而 API 函数的抽象规范反映操作系统设计时要求的功能正确需求. 与一般软件
系统相比, 操作系统的正确性验证面临更大的挑战, 主要原因包括: 操作系统含有中断等引起的复杂的多任务并发行
为; 操作系统内核资源包含指针、链表、结构体等复杂数据结构, 这加剧了并发所造成的数据竞争和共享问题. 因
此, 操作系统正确性的验证需要同时处理并发、精化、数据共享和竞争, 这一直是学术界形式验证的难题. 并发精化
程序逻辑 CSL-R [7,9] 解决了以上所提出的问题, 它将并发分离逻辑 [10,11] 进行扩展, 加入资源不变式和上下文精化关系
的概念, 实现了包含可变共享资源的并发程序的可组合和精化关系的验证. 本文将使用 CSL-R 作为验证逻辑, 对航
天嵌入式领域某微内核操作系统的权能访问控制模块进行形式建模和验证, 保证其实现的功能正确性.
访问控制作为操作系统信息安全的基础机制, 旨在防止未经授权的用户或进程访问系统内核资源. 传统的访
问控制机制包括自主访问控制 (DAC) 和强制访问控制 (MAC), 但随着安全需求的不断增加, 这些传统方法显得不
够灵活和精细. 权能访问控制 (capability-based access control) 是一种细粒度的访问控制机制, 它将访问权限直接与
对象和操作绑定, 能够更精确地控制权限的分配和使用. 权能访问控制模块管理全部的内核服务以及对相关内核
资源的访问. 每个权能是一个特权对象, 包含对特定资源的访问权限, 并且精细地定义了可以进行哪些操作, 如读
取、写入或执行特定功能. 权能访问控制模块的正确性验证非常关键. 然而, 与操作系统其他功能模块例如任务管