| 引用本文: | 徐家乐,王淑灵,李黎明,詹博华,吕毅,代艺博,崔舍承,吴鹏,谭宇,张学军,詹乃军.操作系统内核权能访问控制的形式验证.软件学报,2025,36(8):3570-3586 |
| |
|
| |
|
|
| 本文已被：浏览 1727次 下载 1669次 |
码上扫一扫！ |
|
|
| 操作系统内核权能访问控制的形式验证 |
|
徐家乐1,2,3, 王淑灵4,3, 李黎明1,2, 詹博华5, 吕毅1,2,3, 代艺博1,2,3, 崔舍承1,2,3, 吴鹏1,2,3, 谭宇6, 张学军6, 詹乃军7
|
|
1.基础软件与系统重点实验室 (中国科学院 软件研究所), 北京 100190;2.计算机科学国家重点实验室(中国科学院 软件研究所), 北京 100190;3.中国科学院大学, 北京 100049;4.天基综合信息全国重点实验室(中国科学院 软件研究所), 北京 100190;5.华为技术有限公司, 北京 100085;6.北京控制与电子技术研究所, 北京 100038;7.北京大学 计算机学院, 北京 100091
|
|
| 摘要: |
| 操作系统内核是构建安全攸关系统软件的基础. 任何计算机系统的正确运行都依赖于底层操作系统实现的正确性, 因此, 对操作系统内核进行形式验证是很迫切的需求. 然而, 操作系统中存在的多任务并发、数据共享和竞争等行为, 给操作系统内核的验证带来很大的挑战. 近年来, 基于定理证明的方法广泛用于操作系统各功能模块的形式验证, 并取得多个成功应用. 微内核操作系统权能访问控制模块提供基于权能的细粒度访问控制, 旨在防止未经授权的用户访问系统内核资源和服务. 在权能访问控制模块实现中, 所有任务的权能空间构成多个树结构, 同时每个任务权能节点包含多种嵌套的复杂数据结构, 以及权能函数中广泛存在的对权能结构的访问、修改、(递归)删除等操作, 使得它的形式验证与操作系统其他功能模块相比更加困难. 将以并发精化程序逻辑CSL-R为基础, 通过证明权能应用程序接口函数(API函数)和其抽象规范之间的精化关系, 来验证航天嵌入式领域某微内核操作系统权能访问控制的功能正确性. 首先对权能数据结构进行形式建模, 并在此基础上定义全局不变式来保持权能空间的一致性; 然后定义反映功能正确性需求的内核函数的前后条件规范和API函数的抽象规范; 最终验证权能API函数C代码实现和抽象规范之间的精化关系. 以上所有的定义和验证均在Coq定理证明器中完成. 在验证过程中发现实现的错误, 并得到微内核操作系统设计方的确认和修改. |
| 关键词: 操作系统内核 形式验证 权能访问控制 并发精化分离逻辑 |
| DOI：10.13328/j.cnki.jos.007351 |
| 分类号: |
| 基金项目:国家重点研发计划(2022YFA1005103); 国家自然科学基金(62432005, 62032024) |
|
| Formal Verification of Capability-based Access Control in Operating System Kernel |
|
XU Jia-Le1,2,3, WANG Shu-Ling4,3, LI Li-Ming1,2, ZHAN Bo-Hua5, LYU Yi1,2,3, DAI Yi-Bo1,2,3, CUI She-Cheng1,2,3, WU Peng1,2,3, TAN Yu6, ZHANG Xue-Jun6, ZHAN Nai-Jun7
|
|
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.University of Chinese Academy of Sciences, Beijing 100049, China;4.National Key Laboratory of Space Integrated Information System (Institute of Software, Chinese Academy of Sciences), Beijing 100190, 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) |
|
|
|
|
