软件学报

作者：章乐平，赵永望，王布阳，李悦欣，冯潇潇

单位：章乐平，北京航空航天大学 计算机学院, 北京 10019111,赵永望，浙江大学 网络空间安全学院, 浙江 杭州 310007;浙江大学 移动终端安全技术浙江省工程研究中心, 浙江 杭州 31000702,王布阳，北京航空航天大学 计算机学院, 北京 10019103,李悦欣，北京航空航天大学 计算机学院, 北京 10019104,冯潇潇，北京航空航天大学 计算机学院, 北京 10019105

关键词：L4;形式化验证;内存管理;映射;信息流安全;Isabelle/HOL

基金：国家自然科学基金（62132014）；浙江省尖兵计划（2022C01045）

第二代微内核L4在灵活度和性能方面极大地弥补了第一代微内核的不足，这引起学术界和工业界的关注.内核是实现操作系统的基础组件，一旦出现错误，可能导致整个系统瘫痪，进一步对用户造成损失.因此，提高内核的正确性和可靠性至关重要.虚拟内存子系统是实现L4内核的关键机制，聚焦于对该机制进行形式建模和验证.构建了L4虚拟内存子系统的形式模型，该模型涉及映射机制所有操作、地址空间所有管理操作以及带TLB的MMU行为等；形式化了功能正确性、功能安全和信息安全三方面的属性；通过部分正确性、不变式以及展开条件的推理，在定理证明器Isabelle/HOL中证明了提出的形式模型满足这些属性.在建模和验证过程中，发现源代码在功能正确性和信息安全方面共存在3点问题，给出了相应的解决方案或建议.

来源：2023年第8期

《软件学报》期刊编辑部

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