Page 58 - 《软件学报》2021年第6期

1632 Journal of Software 软件学报 Vol.32, No.6, June 2021

prove the correctness of exception management for SPARC processor architecture operating systems. Especially for multi-task
concurrency and frequent interruption of real-time operating system exception nesting and task switching in exceptions, the exception
management is divided into five stages for comprehensive formal modeling, and this framework is implemented in the Coq proving
theorem assistant tool. Based on this framework, the correctness of the exception management function of the spacecraft embedded real-
time operating system SpaceOS, which is actually used by China’s Beidou-3, is verified.
Key words: operating system; exception management; exception nesting; task switching; formal verification

如今,计算机系统已经被广泛应用于航天、国防、医疗、金融等安全攸关领域,这类系统一旦发生错误,将
会造成严重后果.建立高可信的计算机系统,在安全攸关领域是极其重要的.而操作系统作为计算机系统中最基
础的底层软件,是构建高可信度计算机系统的关键.异常管理作为操作系统最底层的功能,负责引导系统控制流
的突变来响应处理器状态中的某些变化.异常管理的正确性,是整个操作系统正确性的基础.传统的软件测试方
法只能发现程序的执行结果是否正确,而不能证明程序本身有无错误.传统的测试方法无法保证程序正确性的
百分百覆盖,在一些极端苛刻的环境之下,程序可能出现错误.为了解决这个问题,形式化验证方法逐渐成为研
究的热点.形式化验证方法是一种确保软硬件系统可靠性和安全性的有效方法,它是基于严格数学基础的、对
计算机软件系统进行形式规约、开发和验证的技术.其中,形式规约使用形式语言构建所开发软件系统的规约,
它们对应于软件生命周期不同阶段的制品,刻画系统不同抽象层次的模型和性质,例如需求模型、设计模型甚
至代码和代码的执行模型等.通过形式验证,证明不同形式规约之间的逻辑关系,这些逻辑关系反映了在软件开
发不同阶段软件制品之间需要满足的各类正确性需求.例如,形式验证给出“系统设计模型满足若干特定性质”
[1]
的证明构造 .
1 相关工作

至今为止,国内外的相关研究已经对操作系统内核开展了大量的形式化验证工作,包括 NICTA 团队对 seL4
[3]
的验证 、Gerwin Klein 等人利用 Isabelle/HOL 对 seL4 内核进行模型层和代码层的形式化验证.内核模块的验
证主要包含内存管理、并发管理、IO 管理等,同时证明了模型层与代码层的一致性.耶鲁大学的 Shao 团队提出
了一个可扩展的体系结构 CertiKOS,用于构建经过形式化验证的并发 OS 内核 [3,4] ,并发允许跨越不同的抽象层
交错执行内核或用户模块,每一层都具有一组不同的可观察事件.作者采用分层组合的方法,以适合的抽象级别
对每一层的可观察事件进行了形式化建模与验证.Feng 团队对 uC/OS-II 的验证 [5,6] 主要针对整个复杂软件系统
整体的可靠性展开验证,考虑到 OS 内核不同功能模块的实现逻辑各不相同,作者针对各个模块的特点分别使
用特定的验证方法来证明模块的可靠性,最后将这些模块连接在一起,验证整个系统的可靠性.BICE 的 Qiao 团
队对 SpaceOS [7,8] 进行了验证:在文献[7]中,Qiao 等人使用 Rodin 建模工具和 Event-B 数理抽象方法对 SpaceOS
内存管理的正确性进行了验证;文献[8]中,Jiang 等人使用 Coq 对 SpaceOS 操作系统任务管理功能的需求层提出
了 4 条安全性质,并对其进行了建模与验证.
[9]
一个经典的实时嵌入式操作系统功能架构 如图 1 所示.
API接口
内核
任务管理 文件系统 网络管理

时间管理 IO管理
异常管理 内存管理
HAL接口
Fig.1 Classic real-time embedded operating system architecture
图 1 经典实时嵌入式操作系统架构

异常管理是操作系统最底层的功能,它的正确性决定了整个操作系统是否能够安全可靠地运行,因而被给