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

马智 等:面向 SPARC 处理器架构的操作系统异常管理验证 1645

代码 3. 定理 2 在 Coq 中的证明.
Theorem Normal_Exce_Proof:forall(ex:Exce)(sw:Flags),

{mac_Status_pre(ex)∧(sw=0)}
f0:exce_design_code
{mac_Status_post(ex)}.

Proof.
…
Qed.
Table 1 Coq code line statistics
表 1 Coq 代码行数统计

功能描述 代码行数
数据类型定义 536
异常向量表 218
上下文保护 462
ESR 跳转 571
上下文恢复 1 183
异常退出 347
定理验证 2 674
总计 5 964
代码运行时间 58.24s
5 总 结

本文提出了一种基于 Hoare-logic 的验证框架,用于证明面向 SPARC 处理器架构的实时嵌入式操作系统异
常管理功能的正确性.首先,对操作系统异常控制流进行了介绍,并且总结出了 3 种实时操作系统所面临的异常
情况:基本异常、异常嵌套、伴随任务切换的异常;然后,使用结构化的操作语义搭建异常管理验证框架,将其划
分为 5 个阶段:异常向量表处理、上下文保护、ESR 跳转、上下文恢复、异常退出,并对每个阶段的建模过程
进行了详细的介绍;最后,使用此形式化框架对应用在北斗三号航天器系统上的 SpaceOS 操作系统进行验证,在
Coq 定理证明工具的帮助下,验证了 SpaceOS 异常管理的正确性.
目前,关于 SpaceOS 的形式化工作都是分模块展开的.在今后的工作中,我们将尝试把任务管理、内存管理
和异常管理的正确性证明工作形式化的集成起来,形成系统整体安全性和正确性的证明.

References:
[1] Wang J, Zhan NJ, Feng XY, Liu ZM. Overview of formal methods. Ruan Jian Xue Bao/Journal of Software, 2019,30(1):33−61 (in
Chinese with English abstract). http://www.jos.org.cn/1000-9825/5652.htm [doi: 10.13328/j.cnki.jos.005652]
[2] Klein G, Elphinstone K, Heiser G, Andronick J, Cock D, Derrin P, Elkaduwe D, Engerlhardt K, Kolanski R, Norrish M, Sewell T.
seL4: Formal verification of an OS kernel. In: Proc. of the ACM SIGOPS 22nd Symp. on Operating Systems Principles. 2009.
207−220.
[3] Chen H, Wu XN, Shao Z, Lockerman J, Gu RH. Toward compositional verification of interruptible OS kernels and device drivers.
In: Proc. of the 37th ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI 2016). New York:
Association for Computing Machinery, 2016. 431−447.
[4] Gu RH, Shao Z, Chen H, Wu XN, Kim J, Sjöberg V, Costanzo D. CertiKOS: An extensible architecture for building certified
concurrent OS kernels. In: Proc. of the 12th USENIX Conf. on Operating Systems Design and Implementation (OSDI 2016).
USENIX Association, 2016. 653−669.
[5] Feng XY, Shao Z, Dong Y, Guo Y. Certifying low-level programs with hardware interrupts and preemptive threads. In: Proc. of the
29th ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI 2008). New York: Association for
Computing Machinery, 2008. 170−182.
[6] Feng XF, Shao Z, Guo Y, Dong Y. Combining domain-specific and foundational logics to verify complete software systems. In:
Proc. of the VSTTE 2008. 2008. 54−69.
[7] Qiao L, Yang MF, Tan YL, Pu GG, Yang H. Formal verification of memory management system in spacecraft using Event-B. Ruan
Jian Xue Bao/Journal of Software, 2017,28(5):1204−1220 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/
5218.htm [doi: 10.13328/j.cnki.jos.005218]