软件学报ISSN1000-9825,CODENRUXUEWE-mail:jos@iscas.ac.cnJournalofSoftware,2023,34(8):3527−3548[doi:10.13328/j.cnki.jos.006869]http://www.jos.org.cn©中国科学院软件研究所版权所有.Tel:+86-10-62562563L4虚拟内存子系统的形式化验证∗章乐平1,赵永望2,3,王布阳1,李悦欣1,冯潇潇11(北京航空航天大学计算机学院,北京100191)2(浙江大学网络空间安全学院,浙江杭州310007)3(浙江大学移动终端安全技术浙江省工程研究中心,浙江杭州310007)通信作者:赵永望,E-mail:zhaoyw@zju.edu.cn摘要:第二代微内核L4在灵活度和性能方面极大地弥补了第一代微内核的不足,这引起学术界和工业界的关注.内核是实现操作系统的基础组件,一旦出现错误,可能导致整个系统瘫痪,进一步对用户造成损失.因此,提高内核的正确性和可靠性至关重要.虚拟内存子系统是实现L4内核的关键机制,聚焦于对该机制进行形式建模和验证.构建了L4虚拟内存子系统的形式模型,该模型涉及映射机制所有操作、地址空间所有管理操作以及带TLB的MMU行为等;形式化了功能正确性、功能安全和信息安全三方面的属性;通过部分正确性、不变式以及展开条件的推理,在定理证明器Isabelle/HOL中证明了提出的形式模型满足这些属性.在建模和验证过程中,发现源代码在功能正确性和信息安全方面共存在3点问题,给出了相应的解决方案或建议.关键词:L4;形式化验证;内存管理;映射;信息流安全;Isabelle/HOL中图法分类号:TP311中文引用格式:章乐平,赵永望,王布阳,李悦欣,冯潇潇.L4虚拟内存子系统的形式化验证.软件学报,2023,34(8):3527–3548.http://www.jos.org.cn/1000-9825/6869.htm英文引用格式:ZhangLP,ZhaoYW,WangBY,LiYX,FengXX.FormalVerificationofVirtualMemorySubsysteminL4.RuanJianXueBao/JournalofSoftware,2023,34(8):3527−3548(inChinese).http://www.jos.org.cn/1000-9825/6869.htmFormalVerificationofVirtualMemorySubsysteminL4ZHANGLe-Ping1,ZHAOYong-Wang2,3,WANGBu-Yang1,LIYue-Xin1,FENGXiao-Xiao11(SchoolofComputerScienceandEngineering,BeihangUniversity,Beijing100191,China)2(SchoolofCyberScienceandTechnology,ZhejiangUniversity,Hangzhou310007,China)3(ZhejiangEngineeringResearchCenterofMobileTerminalSecurityTechnology,ZhejiangUniversity,Hangzhou310007,China)Abstract:L4,thesecond-generationofmicrokernel,greatlycompensatesfortheshortcomingsofthefirst-generationofmic...
