微信服务号

微信订阅号

2025-5-15- 10
Home > Archive>Volume 36, Issue 8, 2025 >1-17. DOI:10.13328/j.cnki.jos.007351
PDF HTML XML Export Cite reminder
Formal Verification of Capability-based Access Control in Operating System Kernel
Author:
Affiliation:

Clc Number:

TP311

  • Article
    • | |
  • Metrics
    • |
  • Reference [24]
    • |
  • Related [20]
    • | | |
  • Comments
    Abstract:

    Operating system (OS) kernels serve as the foundation for designing safety-critical software systems. The correct functioning of computer system depends on the correctness of the underlying OS kernels, making their formal verification a critical task. However, behaviors such as multi-task concurrency, data sharing, and race conditions inherent in OS kernels pose significant challenges for formal verification. In recent years, theorem-proving methods have been widely applied to verify the functionality of OS kernel modules, achieving notable successes. The capability-based access control module in OS kernels provides fine-grained access control, designed to prevent unauthorized users from accessing kernel resources and services. Its implementation involves capability spaces for tasks, which form a set of tree structures. Each capability node includes nested, complex data structures and capability functions frequently perform operations such as access, modification, and recursive deletion of capability spaces. These factors make the formal verification of capability-based access control significantly more challenging compared to other OS modules. This study employs concurrent separation logic with refinement (CSL-R) to verify the functional correctness of a capability-based access control module in the aerospace embedded domain. The verification establishes refinement between the API functions of the capability module and their abstract specifications. First, the capability data structure is formally molded, followed by the definition of a global invariant to ensure the consistency of capability spaces. Next, the preconditions and postconditions for internal functions and the abstract specifications for API functions are defined to reflect functional correctness. Finally, the refinement between the C implementation of the API functions and their abstract specifications is rigorously proven. All definitions and verification steps are formalized using the Coq theorem prover. During the verification process, errors are identified in the C implementation, which are subsequently confirmed and corrected by the OS kernel designers.

    Reference
    [1] Woodcock J, Larsen PG, Bicarregui J, Fitzgerald J. Formal methods: Practice and experience. ACM Computing Surveys, 2009, 41(4): 19.
    [2] Gleirshcer M, Foster S, Woodcock J. New opportunities for integrated formal methods. ACM Computing Surveys, 2020, 52(6): 117.
    [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] 许峰唯. 抢占式操作系统内核验证框架的设计和实现 [博士学位论文]. 合肥: 中国科学技术大学, 2016.
    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.
    [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.
    [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. on Computer-aided Verification. New York: Springer, 2019. 515–533. [doi: 10.1007/978-3-030-25543-5_29]
    [19] Zhang LP, Zhao YW, Li JX. A comprehensive specification and verification of the L4 microkernel API. In: Proc. of the 30th Int’l Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Luxembourg: ACM, 2024. 217–234. [doi: 10.1007/978-3-031-57249-4_11]
    [20] Nipkow T, Wenzel M, Paulson LC. Isabelle/HOL: A Proof Assistant for Higher-order Logic. Berlin: Springer, 2002. [doi: 10.1007/3-540-45949-9]
    [21] Huet GP, Kahn G, Paulin-Mohring C. The Coq proof assistant: A tutorial. 1997. https://flint.cs.yale.edu/cs430/coq/pdf/Tutorial.pdf
    [22] Owre S, Rushby JM, Shankar N. PVS: A prototype verification system. In: Proc. of the 11th Int’l Conf. on Automated Deduction. Saratoga Springs: Springer, 1992. 748–752. [doi: 10.1007/3-540-55602-8_217]
    [23] Jasti NVK, Kodali R. Lean production: Literature review and trends. Int’l Journal of Production Research, 2015, 53(3): 867–885.
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

徐家乐,王淑灵,李黎明,詹博华,吕毅,代艺博,崔舍承,吴鹏,谭宇,张学军,詹乃军.操作系统内核权能访问控制的形式验证.软件学报,2025,36(8):1-17

Copy
Share
Article Metrics
  • Abstract:153
  • PDF: 247
  • HTML: 0
  • Cited by: 0
History
  • Received:August 26,2024
  • Revised:October 14,2024
  • Online: December 10,2024
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2044578Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address：4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code：100190
Phone：010-62562563 Fax：010-62562533 Email：jos@iscas.ac.cn
Technical Support：Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063