Page 86 - 《软件学报》2025年第8期
P. 86

何韬 等: GhostFunc: 一种针对  Rust 操作系统内核的验证方法                                         3509


                    在本文的形式化模型中, 定义了一系列关键的不变式, 如                 thread_state_invariant 和 irq_state_invariant, 这些不变
                 式通过模型的操作函数得到了严格的维护. 这些不变式不仅确保了模型中各个操作的正确性, 同时也为代码实现
                 提供了可靠的理论基础.
                    特别是通过对      GhostFunc 的引入, 我们能够将    unsafe 代码中的复杂操作抽象出来, 并通过安全接口与              safe 代
                 码结合. 这种方法确保了中断处理和线程状态管理在                 safe 和  unsafe 代码之间的一致性, 从而保证了系统整体行为
                 的正确性. 虽然尚未完成代码的精化验证, 但基于模型中不变式的维护, 可以推断代码实现能够在很大程度上保持
                 与模型一致. 在实际验证中, 由于工作重点在于检验               GhostFunc 验证方案在实际工程中的有效性, 我们在一些边缘
                 情况验证和较复杂的情况做了一部分的简化假设. 尽管本文模型验证覆盖了大部分系统行为, 但在某些情况下可
                 能存在偏差. 以下是识别出的潜在不一致性. 由于在构建抽象模型时, 我们对系统的一些行为进行了简化:
                    (1) 忽略内存分配失败: 在高层模型中, 假设每次            alloc() 调用都能成功. 然而, 在实际实现中, 可能会因为内存
                 不足而导致分配失败, 这种情况没有在模型中完全覆盖. 未来工作中, 我们计划扩展模型以捕捉内存不足的场景,
                 并通过状态转移图模拟不同内存状态下的系统行为.
                    (2) 中断与异常嵌套的简化: 模型中对中断和异常的处理采用了顺序执行的假设, 但在实际系统中, 可能会发
                 生中断嵌套或多级异常的情况. 将通过引入状态机模型模拟中断优先级管理, 并在实现代码的关键路径上进行不
                 变量检查. 这些情况可能在实际内核运行中产生验证结果和实际不一致的情况.
                    此外, 为了测试一致性的情况, 我们专门设计了一些测试场景如表                    2, 以测试模型和实际代码的一致性情况.

                                                      表 2 测试场景

                    TestCase         初始状态                    输入条件                     模型预期输出
                     TC-001        state = unlocked          调用 lock()                state = locked
                     TC-002      所有寄存器保存完成                 任务切换指令                    reg_saved = true
                     TC-003       mem_available = true      调用 alloc()             alloc_result = success
                     TC-004       mem_available =false      调用 alloc()              alloc_result = failure
                     TC-005          文件不存在                syscall_open(“test”)    syscall_result = error(404)
                     TC-006      当前处理中断级别为2                  嵌套中断               nested_interrupt_handled = true
                     TC-007          state = valid     GhostFunc调用unsafe函数             state = valid
                     TC-008          input = −1          GhostFunc 输入非法值            error = invalid input

                    在表  2  中的各类场景设计中, 预期输出和一致性的检查均通过, 但是上述例如内存不足场景我们用变量来控
                 制, 但是实际中操作系统可能无法检测到实际的内存大小. 构造, 其次是当中断嵌套到                          3  级以上的时候, 场景构建
                 会会变得十分复杂, 不易构建. 在二级中断中, 我们顺序执行的中断处理方式仍然可以保持一致性.
                    本文提出的方法在设计时特别考虑了其可拓展性, 以便能够适应操作系统和应用环境中不断变化和发展的需
                 求. 通过模块化的设计和抽象化的接口定义, 本文方法能够灵活地适应不同的系统配置和特性. 例如, GhostFunc
                 模块的引入, 使得复杂的 unsafe 操作可以被抽象为安全接口, 并且这些接口可以根据具体需求进行扩展或替换, 以
                 支持特定的硬件中断处理或优化的线程调度算法.
                    此外, 由于某内核正处于高速开发迭代中, 当系统引入新功能或新特性                      (如多级缓存管理、虚拟化支持等) 时,
                 现有方法能够通过扩展接口或增加新的模块来进行无缝集成, 而无需对核心模型进行大幅修改. 这种设计不仅保
                 证了当前系统的稳定性和安全性, 还为未来的功能扩展提供了良好的基础, 确保方法在面对新挑战时的适应性.

                 5   总 结

                    本文以某    Rust 构建的内核作为验证目标, 提出了         GhostFunc 的  safe 代码块和  unsafe 代码块组合验证思路. 重
                 点介绍了适应于内核验证的          unsafe 代码形式化语法和语义模型、GhostFunc 的形式化规范. 并以某内核任务管理
                 与调度模块的验证作为实例进行分析, 将             unsafe 和  safe 代码段从不同层级进行抽象, 详细验证了任务管理与调度
                 模块的安全属性包括: (1) 无常见内存错误如缓冲区溢出、整型溢出、野指针; (2) 代码的功能符合设计目标; (3) 上
                 下文的切换返回地址正确.
   81   82   83   84   85   86   87   88   89   90   91