(19)国家知识产权局 (12)发明 专利申请 (10)申请公布号 (43)申请公布日 (21)申请 号 202210552736.4 (22)申请日 2022.05.19 (71)申请人 浙江大学 地址 310058 浙江省杭州市西湖区余杭塘 路866号 (72)发明人 王竟亦　孙欢　王文海　刘艾明　 (74)专利代理 机构 杭州求是专利事务所有限公 司 33200 专利代理师 刘静 (51)Int.Cl. G06F 21/44(2013.01) G06F 9/50(2006.01) G06F 9/54(2006.01) (54)发明名称 基于依赖保证机制的操作系统内存管理机 制验证方法 (57)摘要 本发明公开了一种基于依赖保证机制的操 作系统内存 管理机制验证方法。 该方法将操作系 统建模为一个并发事件模型， 并利用并行程序验 证框架提供的程序语义和记号建模内存申请和 释放函数。 设计内存安全并将其转化为程序验证 框架语义下的安全规约， 并依据安全规约， 设计 相应的验证条件， 并利用行程序验证框架的依 赖‑保证证明系统， 自动检查验证条件的相容性， 最后通过交互式定理证明器检查证明的正确性。 本发明利用形式化验证和机器证明技术， 严格地 验证了内存 管理系统的安全性， 保证了操作系统 安全可靠运行， 防患于未然。 权利要求书1页 说明书5页 附图1页 CN 115033866 A 2022.09.09 CN 115033866 A 1.一种基于依赖保证机制的操作系统内存管理机制验证方法， 其特征在于， 包含以下 步骤： (1)操作系统语义设计： 将实时操作系统建模为内存管理模型， 所述内存管理模型采用 并发事件模型， 所述内存管理模型中包含一个调度事件系统和若干线程事件系统， 还包含 针对实时操作系统通用的系统安全规约和依赖保证条件； (2)内存管理规约建模： 利用并行程序验证框架提供的程序语义和记号， 对操作系统内 存管理机制的系统初始化状态、 系统运行状态以及内存申请和内存释放 函数进行建模； (3)设计安全规约： 提取与操作系统内存安全高度相关的性质， 并结合内存管理机制和 内存组数据结构， 使用并行程序验证框架提供的语义接口将安全性质转化为形式化的内存 安全规约； (4)设计验证条件： 根据 步骤(1)建立的内存管理模型和系统安全规约， 以及步骤(3)设 计的内存安全规约， 设计每个事件系统的依赖、 保证条件； 依据操作系统内存管理模块的任 务代码、 步骤(1)建立的系统安全规约以及步骤(3)设计的内存安全规约， 设计每个事件系 统的前置、 后置条件； (5)验证内存管理模型： 编写验证单独事件系 统符合依赖、 保证条件和前置、 后置条件 的证明脚本， 并通过交互式定理证明器检验所述证明脚本的正确 性， 从而对单独事件系统 的正确性进行形式化验证； 利用并行程序验证框架 提供的事件验证接口检验不同事件系统 之间的依赖、 保证条件和前置、 后置条件是否相容； 利用并行程序验证框架 提供的事件系统 验证接口对内存管理模型进行 形式化验证。 2.根据权利要求1所述的一种基于依赖保证机制的操作系统内存管理机制验证方法， 其特征在于， 所述步骤(1)中， 所述并发事件模型由一组定义准确的输入事件系统组成， 并 发事件模型通过对每个事件系统执行关联的处理程序对这些事件系统进 行处理； 在并发环 境中， 每个事件系统的处 理程序都可以与其 他事件系统的处 理程序进行交 互。 3.根据权利要求1所述的一种基于依赖保证机制的操作系统内存管理机制验证方法， 其特征在于， 所述步骤(1)中， 构建的内存管理模型， 包含一个高度抽象的调度事件系统进 行事件调度和线程控制， 可以支持其它操作系统的建模。 4.根据权利要求1所述的一种基于依赖保证机制的操作系统内存管理机制验证方法， 其特征在于， 所述步骤(3)中， 需要提取保障内存管理机制安全可靠运行强相关的安全性 质， 包括内存泄露、 内存块重叠、 空闲内存块链表定义错误、 内存池数据结构错误， 并将这些 安全性质转 化为形式化的内存安全规约， 并使用并行程序验证框架提供的语义进行表示。 5.根据权利要求1所述的一种基于依赖保证机制的操作系统内存管理机制验证方法， 其特征在于， 所述步骤(4)中， 基于 设计的前置、 后置条件， 进 行循环不变量设计， 使 得前置、 后置条件以及循环不变量与事 件系统相容。 6.根据权利要求1所述的一种基于依赖保证机制的操作系统内存管理机制验证方法， 其特征在于， 所述并行程序验证框架采用PiCore和HOL ‑Hoare_Parallel， 所述交互式定理 证明器采用Isabel le。权　利　要　求　书 1/1 页 2 CN 115033866 A 2基于依赖保证机制的操作系统内存管理 机制验证方 法 技术领域 [0001]本发明属于形式化验证领域， 涉及一种基于依赖 ‑保证机制的操作系统内存管理 机制验证方法。 背景技术 [0002]操作系统(OS)是关键系统的基本组件。 因此， 系统的正确性和可靠性在很大程度 上取决于系统的底层操作系统。 内存管理是操作系统的基本功能， 它提供了一种方法， 可以 根据程序 的请求动态地将部分内存分配给程序， 并在没有内存的情况下释放内存以供重 用。 由于程序变量和数据存储在分配的内存中， 因此不正确的内存管理规范和实现可能导 致系统崩溃或对整个系统的可利用攻击 。 [0003]seL4是第一个被验证的可以实际应用的通用操作系统内核， seL4首先在Haskeell 中实现内核原型， 然后使用Isab elle定理证明器形成经由形式化验证的执行规范， 通过建 立执行规范和C实现代码之间的精 华关系保证实现的正确性。 seL4内核包含8700行C代码和 600行汇编代码， 使用超过20 0000行Isabel le代码对其 正确性进行验证。 [0004]尽管seL4对其内存管理机制进行了验证， 但存在以下两点缺陷： (1)只在串行操作 系统上进行验证， 没有考虑操作系统的并行性。 (2)验证的内存管理系统比较简单， 只考虑 了内存虚拟映射， 没有考虑动态地分配和释放内存块， 也没有考虑空闲内存链表等复杂的 数据结构。 [0005]依赖‑保证验证框架是一种 常用的并行程序验证框架。 通过对Hoare逻辑 的扩展， 增加了依赖条件和保证条件分别记录环境和线程本身对系统状态造成的影响。 首先对单独 的线程进行验证。 再通过检查不同线程之间的依赖 ‑保证条件是否相容检查独立线程验证 结果的可组合 性， 从而对整个并行系统进行验证。 [0006]传统的基于依赖 ‑保证的验证框架难以直接应用于抢占式实时操作系统的验证， 存在以下两点困难： (1)没有提供一种直接的方法针对抢占式实时操作系统验证时序上 的 安全性质。 传统的基于依赖保证的验证框架只关注命令式程序， 很难在依赖和保证关系中 捕获与可能无限序列的事件处理程序的交互， 以及事件处理程序的输入参数。 (2)依赖 ‑保 证必须针对每个变量状态是否更新进 行检查， 即使其它进程的行为很明显不会对该变量造 成影响。 因此， 有必 要扩展现有的依赖 ‑保证框架， 使其适应抢占式实时操作系统并行、 无限 相应服务的特点。 同时， 需要针对复杂的并行内存管理机制进行合理的建模并提取合适的 安全规约， 从而实现对操作系统内存管理机制的形式化验证。 发明内容 [0007]本发明的目的在于针对现有技术的不足， 提供一种基于依赖保证机制的操作系统 内存管理机制验证方法。 [0008]本发明的目的是通过以下技术方案实现的： 一种基于依赖保证机制的操作系统内 存管理机制验证方法， 该 方法包含以下步骤：说　明　书 1/5 页 3 CN 115033866 A 3