Page 147 - 《软件学报》2025年第8期
P. 147

软件学报 ISSN 1000-9825, CODEN RUXUEW                                        E-mail: jos@iscas.ac.cn
                 2025,36(8):3570−3586 [doi: 10.13328/j.cnki.jos.007351] [CSTR: 32375.14.jos.007351]  http://www.jos.org.cn
                 ©中国科学院软件研究所版权所有.                                                          Tel: +86-10-62562563



                                                                 *
                 操作系统内核权能访问控制的形式验证

                 徐家乐  1,2,4 ,    王淑灵  3,4 ,    李黎明  1,2 ,    詹博华  5 ,    吕    毅  1,2,4 ,    代艺博  1,2,4 ,    崔舍承  1,2,4 ,    吴    鹏  1,2,4 ,    谭    宇  6 ,
                 张学军  6 ,    詹乃军  7


                 1
                  (基础软件与系统重点实验室 (中国科学院 软件研究所), 北京 100190)
                  (计算机科学国家重点实验室       (中国科学院 软件研究所), 北京 100190)
                 2
                  (天基综合信息全国重点实验室       (中国科学院 软件研究所), 北京 100190)
                 3
                 4
                  (中国科学院大学, 北京 100049)
                 5
                  (华为技术有限公司, 北京 100085)
                 6
                  (北京控制与电子技术研究所, 北京 100038)
                 7
                  (北京大学 计算机学院, 北京 100091)
                 通信作者: 王淑灵, E-mail: wangsl@ios.ac.cn
                 摘 要: 操作系统内核是构建安全攸关系统软件的基础. 任何计算机系统的正确运行都依赖于底层操作系统实现
                 的正确性, 因此, 对操作系统内核进行形式验证是很迫切的需求. 然而, 操作系统中存在的多任务并发、数据共享
                 和竞争等行为, 给操作系统内核的验证带来很大的挑战. 近年来, 基于定理证明的方法广泛用于操作系统各功能模
                 块的形式验证, 并取得多个成功应用. 微内核操作系统权能访问控制模块提供基于权能的细粒度访问控制, 旨在防
                 止未经授权的用户访问系统内核资源和服务. 在权能访问控制模块实现中, 所有任务的权能空间构成多个树结构,
                 同时每个任务权能节点包含多种嵌套的复杂数据结构, 以及权能函数中广泛存在的对权能结构的访问、修改、(递
                 归) 删除等操作, 使得它的形式验证与操作系统其他功能模块相比更加困难. 将以并发精化程序逻辑                               CSL-R  为基
                 础, 通过证明权能应用程序接口函数            (API 函数) 和其抽象规范之间的精化关系, 来验证航天嵌入式领域某微内核
                 操作系统权能访问控制的功能正确性. 首先对权能数据结构进行形式建模, 并在此基础上定义全局不变式来保持
                 权能空间的一致性; 然后定义反映功能正确性需求的内核函数的前后条件规范和                           API 函数的抽象规范; 最终验证
                 权能  API 函数  C  代码实现和抽象规范之间的精化关系. 以上所有的定义和验证均在                    Coq  定理证明器中完成. 在验
                 证过程中发现实现的错误, 并得到微内核操作系统设计方的确认和修改.
                 关键词: 操作系统内核; 形式验证; 权能访问控制; 并发精化分离逻辑
                 中图法分类号: TP311

                 中文引用格式: 徐家乐, 王淑灵, 李黎明, 詹博华, 吕毅, 代艺博, 崔舍承, 吴鹏, 谭宇, 张学军, 詹乃军. 操作系统内核权能访问控制
                 的形式验证. 软件学报, 2025, 36(8): 3570–3586. http://www.jos.org.cn/1000-9825/7351.htm
                 英文引用格式: Xu JL, Wang SL, Li LM, Zhan BH, Lyu Y, Dai YB, Cui SC, Wu P, Tan Y, Zhang XJ, Zhan NJ. Formal Verification of
                 Capability-based  Access  Control  in  Operating  System  Kernel.  Ruan  Jian  Xue  Bao/Journal  of  Software,  2025, 36(8): 3570–3586  (in
                 Chinese). http://www.jos.org.cn/1000-9825/7351.htm

                 Formal Verification of Capability-based Access Control in Operating System Kernel

                                                    1,2
                                         3,4
                                                                  5
                 XU  Jia-Le 1,2,4 ,  WANG  Shu-Ling ,  LI  Li-Ming ,  ZHAN  Bo-Hua ,  LYU  Yi 1,2,4 ,  DAI  Yi-Bo 1,2,4 ,  CUI  She-Cheng 1,2,4 ,
                                 6
                                                6
                 WU Peng 1,2,4 , TAN Yu , ZHANG Xue-Jun , ZHAN Nai-Jun 7


                 *    基金项目: 国家重点研发计划  (2022YFA1005103); 国家自然科学基金  (62432005, 62032024)
                  本文由“形式化方法与应用”专题特约编辑陈明帅研究员、田聪教授、熊英飞副教授推荐.
                  收稿时间: 2024-08-26; 修改时间: 2024-10-14; 采用时间: 2024-11-27; jos 在线出版时间: 2024-12-10
                  CNKI 网络首发时间: 2025-04-03
   142   143   144   145   146   147   148   149   150   151   152