L4虚拟内存子系统的形式化验证.pdf
《L4虚拟内存子系统的形式化验证.pdf》由会员分享,可在线阅读,更多相关《L4虚拟内存子系统的形式化验证.pdf(22页珍藏版)》请在咨信网上搜索。
1、 软件学报 ISSN 1000-9825,CODEN RUXUEW E-mail: Journal of Software,2023,34(8):35273548 doi:10.13328/ki.jos.006869 http:/ 中国科学院软件研究所版权所有.Tel:+86-10-62562563 L4 虚拟内存子系统的形式化验证 章乐平1,赵永望2,3,王布阳1,李悦欣1,冯潇潇1 1(北京航空航天大学 计算机学院,北京 100191)2(浙江大学 网络空间安全学院,浙江 杭州 310007)3(浙江大学 移动终端安全技术浙江省工程研究中心,浙江 杭州 310007)通信作者:赵永望,E-
2、mail: 摘 要:第二代微内核 L4 在灵活度和性能方面极大地弥补了第一代微内核的不足,这引起学术界和工业界的关注.内核是实现操作系统的基础组件,一旦出现错误,可能导致整个系统瘫痪,进一步对用户造成损失.因此,提高内核的正确性和可靠性至关重要.虚拟内存子系统是实现 L4 内核的关键机制,聚焦于对该机制进行形式建模和验证.构建了 L4 虚拟内存子系统的形式模型,该模型涉及映射机制所有操作、地址空间所有管理操作以及带TLB 的 MMU 行为等;形式化了功能正确性、功能安全和信息安全三方面的属性;通过部分正确性、不变式以及展开条件的推理,在定理证明器 Isabelle/HOL 中证明了提出的形式模
3、型满足这些属性.在建模和验证过程中,发现源代码在功能正确性和信息安全方面共存在 3 点问题,给出了相应的解决方案或建议.关键词:L4;形式化验证;内存管理;映射;信息流安全;Isabelle/HOL 中图法分类号:TP311 中文引用格式:章乐平,赵永望,王布阳,李悦欣,冯潇潇.L4 虚拟内存子系统的形式化验证.软件学报,2023,34(8):3527 3548.http:/ 英文引用格式:Zhang LP,Zhao YW,Wang BY,Li YX,Feng XX.Formal Verification of Virtual Memory Subsystem in L4.Ruan Jian
4、Xue Bao/Journal of Software,2023,34(8):35273548(in Chinese).http:/ Formal Verification of Virtual Memory Subsystem in L4 ZHANG Le-Ping1,ZHAO Yong-Wang2,3,WANG Bu-Yang1,LI Yue-Xin1,FENG Xiao-Xiao1 1(School of Computer Science and Engineering,Beihang University,Beijing 100191,China)2(School of Cyber S
5、cience and Technology,Zhejiang University,Hangzhou 310007,China)3(Zhejiang Engineering Research Center of Mobile Terminal Security Technology,Zhejiang University,Hangzhou 310007,China)Abstract:L4,the second-generation of microkernel,greatly compensates for the shortcomings of the first-generation of
6、 microkernel in flexibility and performance,which has attracted the attention of academia and industry.The kernel is the basic component for implementing the operating system.Once it has errors,it may cause the breakdown of whole system,further causing losses to users.Therefore,it is very important
7、to improve the correctness and reliability of the kernel.Virtual memory subsystem is a key mechanism to implement L4 kernel.This study focuses on the formal modeling and verification of this mechanism.A formal model is presented,which involves all operations of mapping mechanism,all management opera
8、tions of address space,and MMU behavior with TLB.The properties of functional correctness,safety,and security are formalized.Through reasoning about partial correctness,invariants and unwinding conditions,it is shown that the proposed model satisfies these properties in the theorem prover Isabelle/H
9、OL.During modeling and verification,three problems are found related to functional correctness and security in source code.The corresponding solutions or suggestions are given in this study as well.Key words:L4;formal verification;memory management;mapping;information flow security;Isabelle/HOL 基金项目
10、:国家自然科学基金(62132014);浙江省尖兵计划(2022C01045)本文由“约束求解与定理证明”专题特约编辑蔡少伟研究员、陈振邦教授、王戟研究员、詹博华副研究员、赵永望教授推荐.收稿时间:2022-09-05;修改时间:2022-10-13;采用时间:2022-12-14;jos 在线出版时间:2022-12-30 3528 软件学报 2023 年第 34 卷第 8 期 微内核1是运行于操作系统特权模式下并遵循内核代码最小化原则的一类内核,它将操作系统必要服务例如线程管理和地址空间管理等置于内核层,其他服务如文件系统和设备驱动等置于用户层.这种设计使得系统中一个模块出现错误只会引起相
11、关的应用程序发生故障,而不会导致整个系统崩溃.L42,3是第二代微内核,它遵循微内核的最小化设计原则,仅提供了 3 个基本抽象(线程、地址空间和时间)和两个机制(映射和IPC),其设计目标是追求灵活性、可靠性以及高性能,整个内核的实现约一万行 C+代码.该内核在极大程度上解决了初代微内核4性能低下的问题,在学术界和工业界得到广泛应用58.L4 内核作为操作系统的核心组件,运行于特权模式下,能够绕过硬件保护机制.恶意软件可能利用该特点,通过内核代码潜在的漏洞例如隐蔽通道(covert channel,隐通道)来窃取机密数据,从而导致用户财产损失,甚至可能威胁到生命.为提高其正确性和可靠性,本文聚
12、焦于 L4 虚拟内存子系统这一关键机制,对实现该系统的地址空间和映射机制形式建模与验证.到目前为止,与本文相关的验证工作921存在 3 个问题:首先,经过形式化验证的虚拟内存模型中,虚拟页之间的关系大多数都是呈线性的,很少具备与 L4 类似的树状结构,因此在验证该类结构需要重新探索相关理论知识;其次,已有的关于 L4 虚拟内存子系统模型是不完整的,未考虑灵活页面数据结构、对页面的访问权限字段、对地址空间的操作以及带 TLB 的 MMU 行为等;此外,现有内存模型中验证的属性不够完善,通常都是单方面的,仅验证内存隔离或仅验证功能安全,尚未同时考虑功能正确性、功能安全和信息安全这 3 个方面性质的
13、验证.形式化建模和验证 L4 虚拟内存子系统时,主要面临 3 个方面的挑战.第一,实现 L4 地址空间的数据结构较复杂,采用灵活的页面类型 Fpage 来指定页面大小,操作大小不一致的页面会增加验证的复杂度;第二,L4 采用多级页表来维护虚拟地址和物理地址的关系,在此基础上,L4 映射机制采用映射数据库(mapping database,MDB)来维护地址空间之间页面和页面的关系.对于任意一个页面,它与其他地址空间的页面关系呈树形结构,在验证该模块时,由于路径的不确定性,导致验证工作量呈指数增长;第三,L4 为了防止多级页表带来深层次递归从而导致栈数据溢出等问题,使用非递归方式来实现页面映射操
14、作,同时调用了维护页面之间关系的处理函数,这使得页面映射算法相当复杂.以映射页面 Map_Fpage函数为例,该函数包括 3 层循环,约 560 行代码,占实现 L4 虚拟内存子系统总代码量的四分之一.内核开发人员注释该算法是整个内核中最复杂的算法.针对上述问题和挑战,本文提出了针对 L4 虚拟内存子系统的形式建模和验证方法.整个过程划分为该系统的建模和属性的验证两个阶段.在建模阶段,本文基于 pistachio0.4 版本的源代码22构建,所构建的模型以状态机为基础,定义了包括灵活页面类型 Fpage 的所有数据结构,建模了映射机制所有操作、地址空间管理操作和带 TLB 的MMU 行为;关于
15、待验证的属性,本文形式化了 3 类属性:功能正确性、功能安全(safety)和信息安全(security)相关属性.功能正确性保证所构建的形式模型正确定义了功能需求,同时能够检验功能需求是否合理或正确;功能安全指系统不会出现页面映射关系形成环、TLB 数据不一致等类似的错误;信息安全方面的性质基于信息流安全属性定义,这些属性能够有效防止恶意程序利用隐通道窃取内存中有价值的数据.在验证阶段,本文通过推理部分正确性、不变式和展开条件(unwinding conditions)的方法,证明了形式模型满足功能正确性、功能安全性以及部分信息流安全属性.所有工作在定理证明器 Isabelle/HOL23中
16、完成,对建模和验证过程发现的问题进行分析,并给出相应的解决办法或建议.本文具体贡献如下:1)提出了针对 L4 虚拟内存子系统的形式模型.该模型完整建模了系统中所有功能,包括对页面的操作、带有 TLB 的硬件机制 MMU 的行为以及地址空间的管理,其中,在对页面的操作中拓展了复杂数据结构以及访问权限字段的建模,并解决了已有模型9不完整问题;章乐平 等:L4 虚拟内存子系统的形式化验证 3529 2)形式化了 L4 虚拟内存子系统的功能正确性、功能安全性和信息流安全属性:功能正确性依据 L4 内核开发手册3和部分源代码构建;功能安全性覆盖了已提出的所有不变式9,并拓展了更多不变式,提高了功能安全性
17、质完整度;信息流安全属性考虑无干扰(noninterference)和无泄漏(nonleakage),两者基于本文提出的传递性类型的信息流策略定义;3)使用 Isabelle/HOL 完成了 3 个方面属性的证明.其中:功能正确性被表示为霍尔三元组形式的引理,利用各功能的自身性质以及 Isabelle/HOL 理论库和策略证明这些引理成立;功能安全相关属性被表示为一系列不变式,通过归纳方法完成不变式的证明;信息流安全属性的证明依赖于展开条件,本文完成了对无泄漏的全部证明和对无干扰的部分证明;4)发现了 L4 虚拟内存子系统的设计和源代码中共存在 3 个问题,这些问题导致该子系统不满足功能正确性
18、和无干扰属性.针对这些问题,本文提出了相应的解决方案或建议.本文第 1 节介绍技术背景和相关工作.第 2 节详细阐述 L4 虚拟内存子系统形式模型的构建过程:首先,定义相关数据结构和状态;其次,建模该子系统中的所有行为,包括映射机制中页面操作、带 TLB 的 MMU行为、地址空间管理操作.第 35 节分别描述关于 L4 虚拟内存子系统的功能正确性、功能安全和信息安全相关性质的定义和证明.第 6 节分析和评估验证结果,指出发现的问题并给出建议.最后总结全文.1 技术背景与相关工作 本节介绍与本文研究相关的技术背景和相关工作:首先介绍了 L4 虚拟内存子系统的技术实现和已存在的验证情况,其次阐述了
19、内存管理机制的相关工作,最后介绍了信息流安全的背景知识和相关验证案例.1.1 L4虚拟内存子系统 L4 虚拟内存子系统包括地址空间和映射等机制.地址空间是一个逻辑的概念,它表示一个线程能够访问的虚拟地址范围.对 32 位机器来说,它的覆盖范围是 04 G.每个地址空间中包含一个页表,实现了虚拟地址到物理地址的转换,同时是实现内存隔离的一种方式.L4 对地址空间的管理操作包括创建地址空间、初始化地址空间和删除地址空间;映射机制是 L4 内核的特色之一,该机制除了维护页表数据,还维护不同地址空间中页面的相互关系.系统刚开机时,会创建一个特权空间 Sigma0Space,同时将物理内存一一映射到该空
20、间,因此它占据所有的物理内存并拥有处理物理内存的最高权限.之后,Sigma0Space 中的唯一线程 sigma0 作为一个分页器(pager),会管理物理内存的分配.具体操作是:将自身空间的页面映射到其他地址空间,获得页面的地址空间,能够进一步地将该页面映射到其他地址空间.在此过程中,采用多级页表记录地址空间中被映射页面与物理页的转换关系以及访问权限.如图 1(a)所示:通过多级页表获取物理页面,由于 L4 支持灵活的页面映射,所获得的页面大小是可变的.页面成功被映射到其他地址空间后,需要使用MDB来记录每个物理页与地址空间的关系,任何一个物理页与地址空间的关系在逻辑上呈树形结构,MDB 采
21、用双向链表实现该结构,并且构建双向链表的方式是前序遍历.如图 1(b)所示:MDB 中包括 mapnode,rootnode 和 dualnode 这 3 类节点.其中,mapnode 代表了页面实际的映射.例如,A:1表示指定页面映射到地址空间 A 中,所在深度处于第 1层,即最开始被映射到 A 中.在图 1(b)简单情况中(上图),A:1 的相邻节点 B:2 表示页面被 A 映射至 B,进一步被映射至 C和 D 中.对于较复杂的情况(下图),MDB 结构中包括 rootnode 和 dualnode 节点:前者是一个数组,在映射一个大页面分割成的小页面时构建,rootnode 中每个元素与
22、 mapnode 连接;后者包含一个 rootnode 和一个mapnode,用于处理页面既被分割为小页面被映射又被直接映射的情况.由于 L4 使用数据结构 Fpage 来指定不同大小的页面,在允许的条件下,只需执行一次映射操作即可将大页面映射到指定空间,从而提高页面映射的效率,进而提高了性能.然而,该方式大幅度增加了页面映射函数的算法复杂度.在页面映射函数中,约 95%的代码用于实现对页面大小的调整,调整原因包括两个方面:映射方和被映射方所提供的页面大小不一致;在一次操作中,L4 能够处理的页面大小与映射方或被映射方的大小不一致.L4 采用多级页表来实现对虚拟页和物理页关系的维护,并使用非递
23、归算法替代递归算 3530 软件学报 2023 年第 34 卷第 8 期 法实现从大页面到小页面的深层次遍历,这导致在该函数中调整页面大小的算法十分复杂,实际维护页面关系和页表数据的代码仅 30 行左右.16 KB001000001B:2mapnoderootnodedualnodeA:1C:3D:3E:4F:44 KB4 KBA:1B:2C:2D:3(a)多级页表 (b)MDB 图 1 虚拟内存子系统数据结构 目前,关于 L4 虚拟内存子系统的相关建模和验证工作较少,仅包括 Klein 等人9提出的关于 L4 虚拟内存子系统的抽象模型,该抽象模型定义了页面操作、页表查询函数以及地址空间管理中
24、的创建地址空间操作,但是存在的不足是未考虑页表包含的访问权限、TLB、特权空间以及地址空间删除操作.本文对这些未考虑的组件或功能进行了补充.在 Klein 等人的抽象模型中,每次仅对一个页面进行操作,然而 L4 定义了灵活页面类型 Fpage,用于提供大小不同的页面,在页面映射时将其拆分为小页面然后循环处理.对此,本文补充了 Fpage 类型的定义,并实现了处理不同大小页面的函数.由于该部分内容的拓展大幅度增加了验证复杂度,所以本文大部分工作是在完成此函数关于不变式的验证.关于属性,Klein 等人的抽象模型提供了 3 个不变式,本文依据新构建的模型对三者进行重新定义,同时拓展了更多的不变式.
25、后续 Klein 等人在上述模型基础上拓展了精化模型10,精化模型的建模粒度更接近于代码实现,但仍未处理上述存在的问题.1.2 内存管理机制 内存管理机制是指操作系统对内存进行合理地划分和有效地动态分配,目前在形式化领域对该机制完成的工作包括内存模型的构建1116、内存管理机制的验证1721,24,25以及内存分配算法的形式化开发2631等.例如:Saraswat 等人形式化了将程序和内存读写操作分离的弱内存模型11,并保证顺序执行的程序不会产生竞争;Leroy 等人使用定理证明器 Coq 构建了低级命令式语言实现的内存模型12,该模型支持带指针的程序语义以及对此类程序的转换进行推理.部分模型
- 配套讲稿:
如PPT文件的首页显示word图标,表示该PPT已包含配套word讲稿。双击word图标可打开word文档。
- 特殊限制:
部分文档作品中含有的国旗、国徽等图片,仅作为作品整体效果示例展示,禁止商用。设计者仅对作品中独创性部分享有著作权。
- 关 键 词:
- L4 虚拟内存 子系统 形式化 验证
1、咨信平台为文档C2C交易模式,即用户上传的文档直接被用户下载,收益归上传人(含作者)所有;本站仅是提供信息存储空间和展示预览,仅对用户上传内容的表现方式做保护处理,对上载内容不做任何修改或编辑。所展示的作品文档包括内容和图片全部来源于网络用户和作者上传投稿,我们不确定上传用户享有完全著作权,根据《信息网络传播权保护条例》,如果侵犯了您的版权、权益或隐私,请联系我们,核实后会尽快下架及时删除,并可随时和客服了解处理情况,尊重保护知识产权我们共同努力。
2、文档的总页数、文档格式和文档大小以系统显示为准(内容中显示的页数不一定正确),网站客服只以系统显示的页数、文件格式、文档大小作为仲裁依据,平台无法对文档的真实性、完整性、权威性、准确性、专业性及其观点立场做任何保证或承诺,下载前须认真查看,确认无误后再购买,务必慎重购买;若有违法违纪将进行移交司法处理,若涉侵权平台将进行基本处罚并下架。
3、本站所有内容均由用户上传,付费前请自行鉴别,如您付费,意味着您已接受本站规则且自行承担风险,本站不进行额外附加服务,虚拟产品一经售出概不退款(未进行购买下载可退充值款),文档一经付费(服务费)、不意味着购买了该文档的版权,仅供个人/单位学习、研究之用,不得用于商业用途,未经授权,严禁复制、发行、汇编、翻译或者网络传播等,侵权必究。
4、如你看到网页展示的文档有www.zixin.com.cn水印,是因预览和防盗链等技术需要对页面进行转换压缩成图而已,我们并不对上传的文档进行任何编辑或修改,文档下载后都不会有水印标识(原文档上传前个别存留的除外),下载后原文更清晰;试题试卷类文档,如果标题没有明确说明有答案则都视为没有答案,请知晓;PPT和DOC文档可被视为“模板”,允许上传人保留章节、目录结构的情况下删减部份的内容;PDF文档不管是原文档转换或图片扫描而得,本站不作要求视为允许,下载前自行私信或留言给上传者【自信****多点】。
5、本文档所展示的图片、画像、字体、音乐的版权可能需版权方额外授权,请谨慎使用;网站提供的党政主题相关内容(国旗、国徽、党徽--等)目的在于配合国家政策宣传,仅限个人学习分享使用,禁止用于任何广告和商用目的。
6、文档遇到问题,请及时私信或留言给本站上传会员【自信****多点】,需本站解决可联系【 微信客服】、【 QQ客服】,若有其他问题请点击或扫码反馈【 服务填表】;文档侵犯商业秘密、侵犯著作权、侵犯人身权等,请点击“【 版权申诉】”(推荐),意见反馈和侵权处理邮箱:1219186828@qq.com;也可以拔打客服电话:4008-655-100;投诉/维权电话:4009-655-100。