Page 162 - 《软件学报》2025年第8期

徐家乐 等: 操作系统内核权能访问控制的形式验证 3585

6 总 结

本文介绍了航天嵌入式领域某微内核操作系统权能访问控制模块功能正确性的形式建模和验证工作. 我们
以 CSL-R 验证框架为基础, 定义了权能复杂的数据结构断言和全局不变式, 对权能内部函数和 API 函数进行了形
式建模, 并根据设计要求对每个函数定义了形式规范, 证明了权能 API 函数的代码实现与其抽象规范满足精化关
系, 从而验证了权能访问控制的功能正确性. 在验证过程中, 我们发现了权能访问控制代码实现中存在的问题并得
到设计方的确认和修改, 完成了修改后代码的验证, 对该微内核操作系统的权能访问控制的正确性提供了充分的
保障. 接下来, 我们将根据本工作验证中取得的经验, 考虑部分验证代码的自动化, 提供更加通用的自动化接口, 以
便在其他操作系统验证中复用, 提升验证效率.

References:
[1] Woodcock J, Larsen PG, Bicarregui J, Fitzgerald J. Formal methods: Practice and experience. ACM Computing Surveys, 2009, 41(4): 19.
[doi: 10.1145/1592434.1592436]
[2] Gleirshcer M, Foster S, Woodcock J. New opportunities for integrated formal methods. ACM Computing Surveys, 2020, 52(6): 117. [doi:
10.1145/3357231]
[3] Klein G, Elphinstone K, Heiser G, Andronick J, Cock D, Derrin P, Elkaduwe D, Engelhardt K, Kolanski R, Norrish M, Sewell T, Tuch H,
Winwood S. seL4: Formal verification of an OS kernel. In: Proc. of the 22nd ACM SIGOPS Symp. on Operating Systems Principles. Big
Sky: ACM, 2009. 207–220. [doi: 10.1145/1629575.1629596]
[4] Gu L, Vaynberg A, Ford B, Shao Z, Costanzo D. CertiKOS: A certified kernel for secure cloud computing. In: Proc. of the 2nd Asia-
Pacific Workshop on Systems. Shanghai: ACM, 2011. 3. [doi: 10.1145/2103799.2103803]
[5] Chen H, Wu X, 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. Santa Barbara: ACM, 2016. 431–447. [doi:
10.1145/2908080.2908101]
[6] Gu RH, Shao Z, Kim J, Wu X, Koenig J, Sjöberg V, Chen H, Costanzo D, Ramananandro T. Certified concurrent abstraction layers. In:
Proc. of the 39th ACM SIGPLAN Conf. on Programming Language Design and Implementation. Philadelphia: ACM, 2018. 646–661.
[doi: 10.1145/3192366.3192381]
[7] Xu FW, Fu M, Feng XY, Zhang XR, Zhang H, Li ZH. A practical verification framework for preemptive OS kernels. In: Proc. of the 28th
Int’l Conf. on Computer Aided Verification. Toronto: Springer, 2016. 59–79. [doi: 10.1007/978-3-319-41540-6_4]
[8] Sanán D, Zhao YW, Hou Z, Zhang FY, Tiu A, Liu Y. CSimpl: A rely-guarantee-based framework for verifying concurrent programs. In:
Proc. of the 23rd Int’l Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Uppsala: Springer, 2017. 481–498.
[doi: 10.1007/978-3-662-54577-5_28]
[9] Xu FW. Design and implementation of a verification framework for preemptive OS kernels [Ph.D. Thesis]. Hefei: University of Science
and Technology of China, 2016 (in Chinese with English abstract).
[10] Reynolds JC. Separation logic: A logic for shared mutable data structures. In: Proc. of the 17th Annual IEEE Symp. on Logic in
Computer Science. Copenhagen: IEEE, 2002. 55–74. [doi: 10.1109/LICS.2002.1029817]
[11] O’Hearn PW. Resources, concurrency and local reasoning. In: Proc. of the 15th Int’l Conf. on Concurrency Theory. London: Springer,
2004. 49–67. [doi: 10.1007/978-3-540-28644-8_4]
[12] Liedtke J. Toward real microkernels. Communications of the ACM, 1996, 39(9): 70–77. [doi: 10.1145/234215.234473]
[13] Gu RH, Koenig J, Ramananandro T, Shao Z, Wu X, Weng SC, Zhang HZ, Guo Y. Deep specifications and certified abstraction layers. In:
Proc. of the 42nd Annual ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages. Mumbai: ACM, 2015. 595–608.
[doi: 10.1145/2676726.2676975]
[14] Gu RH, Shao Z, Chen H, Kim J, Koenig J, Wu X, Sjöberg V, Costanzo D. Building certified concurrent OS kernels. Communications of
the ACM, 2019, 62(10): 89–99. [doi: 10.1145/3356903]
[15] Liang HJ, Feng XY. A program logic for concurrent objects under fair scheduling. In: Proc. of the 43rd Annual ACM SIGPLAN-
SIGACT Symp. on Principles of Programming Languages. St. Petersburg: ACM, 2016. 385–399. [doi: 10.1145/2837614.2837635]
[16] Liang HJ, Feng XY, Fu M. A rely-guarantee-based simulation for verifying concurrent program transformations. In: Proc. of the 39th
Annual ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages. Philadelphia: ACM, 2012. 455–468. [doi: 10.1145/
2103656.2103711]
[17] Liang HJ, Feng XY, Shao Z. Compositional verification of termination-preserving refinement of concurrent programs. In: Proc. of the
Joint Meeting of the 23rd EACSL Annual Conf. on Computer Science Logic and the 29th Annual ACM/IEEE Symp. on Logic in
Computer Science (LICS). Vienna: ACM, 2014. 65. [doi: 10.1145/2603088.2603123]
[18] Zhao YW, Sanán D. Rely-guarantee reasoning about concurrent memory management in Zephyr RTOS. In: Proc. of the 31st Int’l Conf.