L4虚拟内存子系统的形式化验证

摘要：

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

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

所属期刊栏目：34

分类号：TP311(计算技术、计算机技术)

资助基金：国家自然科学基金;浙江省尖兵计划

在线出版日期：2023-08-15（万方平台首次上网日期，不代表论文的发表时间）

页数：共22页

页码：3527-3548