软件学报

作者：徐家乐，王淑灵，李黎明，詹博华，吕毅，代艺博，崔舍承，吴鹏，谭宇，张学军，詹乃军

单位：徐家乐，基础软件与系统重点实验室 (中国科学院 软件研究所), 北京 100190;计算机科学国家重点实验室(中国科学院 软件研究所), 北京 100190;中国科学院大学, 北京 10004911,王淑灵，天基综合信息全国重点实验室(中国科学院 软件研究所), 北京 100190;中国科学院大学, 北京 10004902,李黎明，基础软件与系统重点实验室 (中国科学院 软件研究所), 北京 100190;计算机科学国家重点实验室(中国科学院 软件研究所), 北京 10019003,詹博华，华为技术有限公司, 北京 10008504,吕毅，基础软件与系统重点实验室 (中国科学院 软件研究所), 北京 100190;计算机科学国家重点实验室(中国科学院 软件研究所), 北京 100190;中国科学院大学, 北京 10004905,代艺博，基础软件与系统重点实验室 (中国科学院 软件研究所), 北京 100190;计算机科学国家重点实验室(中国科学院 软件研究所), 北京 100190;中国科学院大学, 北京 10004906,崔舍承，基础软件与系统重点实验室 (中国科学院 软件研究所), 北京 100190;计算机科学国家重点实验室(中国科学院 软件研究所), 北京 100190;中国科学院大学, 北京 10004907,吴鹏，基础软件与系统重点实验室 (中国科学院 软件研究所), 北京 100190;计算机科学国家重点实验室(中国科学院 软件研究所), 北京 100190;中国科学院大学, 北京 10004908,谭宇，北京控制与电子技术研究所, 北京 10003809,张学军，北京控制与电子技术研究所, 北京 100038010,詹乃军，北京大学 计算机学院, 北京 100091011

关键词：操作系统内核;形式验证;权能访问控制;并发精化分离逻辑

基金：国家重点研发计划(2022YFA1005103); 国家自然科学基金(62432005, 62032024)

操作系统内核是构建安全攸关系统软件的基础. 任何计算机系统的正确运行都依赖于底层操作系统实现的正确性, 因此, 对操作系统内核进行形式验证是很迫切的需求. 然而, 操作系统中存在的多任务并发、数据共享和竞争等行为, 给操作系统内核的验证带来很大的挑战. 近年来, 基于定理证明的方法广泛用于操作系统各功能模块的形式验证, 并取得多个成功应用. 微内核操作系统权能访问控制模块提供基于权能的细粒度访问控制, 旨在防止未经授权的用户访问系统内核资源和服务. 在权能访问控制模块实现中, 所有任务的权能空间构成多个树结构, 同时每个任务权能节点包含多种嵌套的复杂数据结构, 以及权能函数中广泛存在的对权能结构的访问、修改、(递归)删除等操作, 使得它的形式验证与操作系统其他功能模块相比更加困难. 将以并发精化程序逻辑CSL-R为基础, 通过证明权能应用程序接口函数(API函数)和其抽象规范之间的精化关系, 来验证航天嵌入式领域某微内核操作系统权能访问控制的功能正确性. 首先对权能数据结构进行形式建模, 并在此基础上定义全局不变式来保持权能空间的一致性; 然后定义反映功能正确性需求的内核函数的前后条件规范和API函数的抽象规范; 最终验证权能API函数C代码实现和抽象规范之间的精化关系. 以上所有的定义和验证均在Coq定理证明器中完成. 在验证过程中发现实现的错误, 并得到微内核操作系统设计方的确认和修改.

来源：2025年第8期

《软件学报》期刊编辑部

查看软件学报杂志2025年第8期