GhostFunc: Verification Method for Rust Operating System Kernel
Author:
Affiliation:

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

    The operating system serves as the foundational platform for software, and the security of its kernel is often of paramount importance. Rust, a memory-safe programming language that has steadily gained popularity, incorporates safety mechanisms such as lifetimes, ownership, borrowing checks, and RAII. Using Rust to build kernels has emerged as a prominent area of research. However, systems built with Rust often include some unsafe code segments, which prevent the language from offering comprehensive safety guarantees at the language level. As a result, verifying these unsafe code segments is essential to ensuring the correctness and reliability of Rust-based kernels. This study proposes a method for combining the safe and unsafe code segments, called GhostFunc, to verify a microkernel constructed with Rust. Different levels of abstraction are applied to the two types of code segments, and GhostFunc is used for combined verification. Focusing on the task management and scheduling module, this study formalizes unsafe code segments such as Arc<T> using λRust and presents the formal implementation of GhostFunc. An example verification of this method is also provided. All verification efforts are based on theorem proving, and correctness is validated in Coq using the Iris separation logic framework.

    Reference
    [1] 王戟, 詹乃军, 冯新宇, 刘志明. 形式化方法概貌. 软件学报, 2019, 30(1): 33–61. http://www.jos.org.cn/1000-9825/5652.htm
    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
    [2] Liang HJ, Feng XY, Fu M. Rely-guarantee-based simulation for compositional verification of concurrent program transformations. ACM Trans. on Programming Languages and Systems (TOPLAS), 2014, 36(1): 3.
    [3] 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]
    [4] 乔磊, 杨孟飞, 谭彦亮, 蒲戈光, 杨桦. 基于Event-B的航天器内存管理系统形式化验证. 软件学报, 2017, 28(5): 1204–1220. http://www.jos.org.cn/1000-9825/5218.htm
    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
    [5] Ghosh D, Tomazeli L, Jin F, Maheswaran M. SpaceOS: Operating system services for smart computing environments. In: Proc. of the 2014 IEEE Int’l Symp. on a World of Wireless, Mobile and Multimedia Networks. Sydney: IEEE, 2014. 1–6. [doi: 10.1109/WoWMoM.2014.6918932]
    [6] Klein G, Huuck R, Schlich B. Operating system verification. Journal of Automated Reasoning, 2009, 42(1): 123–124.
    [7] 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]
    [8] Andronick J, Lewis C, Morgan C. Controlled owicki-gries concurrency: Reasoning about the preemptible eChronos embedded operating system. In: Electronic Proc. in Theoretical Computer Science. Open Publishing Association, 2015. 10–24. [doi: 10.4204/EPTCS.196.2]
    [9] Hunt GC, Larus JR. Singularity: Rethinking the software stack. ACM SIGOPS Operating Systems Review, 2007, 41(2): 37–49.
    [10] Cui MH, Chen CJ, Xu H, Zhou YF. SafeDrop: Detecting memory deallocation bugs of Rust programs via static data-flow analysis. ACM Trans. on Software Engineering and Methodology, 2023, 32(4): 82.
    [11] Dai ZY, Liu S, Sjoberg V, Li XP, Chen Y, Wang WH, Jia YK, Anderson SN, Elbeheiry L, Sondhi S, Zhang Y, Ni ZZ, Yan SM, Gu RH, He ZY. Verifying Rust implementation of page tables in a software enclave hypervisor. In: Proc. of the 29th ACM Int’l Conf. on Architectural Support for Programming Languages and Operating Systems. La Jolla: ACM, 2024. 1218–1232. [doi: 10.1145/3620665.3640398]
    [12] Toman J, Pernsteiner S, Torlak E. Crust: A bounded verifier for Rust (N). In: Proc. of the 30th IEEE/ACM Int’l Conf. on Automated Software Engineering (ASE). Lincoln: IEEE, 2015. 75–80. [doi: 10.1109/ASE.2015.77]
    [13] Kroening D, Tautschnig M. CBMC-C bounded model checker (competition contribution). In: Proc. of the 20th Int’l Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Grenoble: Springer, 2014. 389–391. [doi: 10.1007/978-3-642-54862-8_26]
    [14] Vytautas A, Müller P, Poli F, Summers AJ. Leveraging Rust types for modular specification and verification. Proc. of the ACM on Programming Languages, 2019, 3(OOPSLA): 147.
    [15] Schilling J. Specifying and verifying sequences and array algorithms in a Rust verifier [MS. Thesis]. Zürich: Eidgen?ssische Technische Hochschule Zürich, 2021.
    [16] Jung R, Jourdan JH, Krebbers R, Dreyer D. RustBelt: Securing the foundations of the Rust programming language. Proc. of the ACM on Programming Languages, 2018, 2(POPL): 66.
    [17] Yanovski J, Dang HH, Jung R, Dreyer D. GhostCell: Separating permissions from data in Rust. Proc. of the ACM on Programming Languages, 2021, 5(ICFP): 92.
    [18] Matsushita Y, Denis X, Jourdan JH, Dreyer D. RustHornBelt: A semantic foundation for functional verification of Rust programs with unsafe code. In: Proc. of the 43rd ACM SIGPLAN Int’l Conf. on Programming Language Design and Implementation (PLDI 2022). San Diego: ACM, 2022. 841–856. [doi: 10.1145/3519939.3523704]
    [19] Paulin-Mohring C. Introduction to the Coq proof-assistant for practical software verification. In: Meyer B, Nordio M, eds. Tools for Practical Software Verification. Berlin: Springer, 2012. 45–95. [doi: 10.1007/978-3-642-35746-6_3]
    [20] Leroy X. Formal verification of a realistic compiler. Communications of the ACM, 2009, 52(7): 107–115.
    [21] Gonthier G. Formal proof—The four-color theorem. Notices of the AMS, 2008, 55(11): 1382–1393.
    [22] David D, Micaela M. Diophantus’ 20th problem and fermat’s last theorem for n=4: Formalization of fermat’s proofs in the Coq proof assistant. arXiv:cs/0510011, 2005.
    [23] Jung R, Krebbers R, Jourdan JH, Bizjak A, Birkedal L, Dreyer D. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming, 2018, 28: e20.
    [24] Jung R, Krebbers R, Birkedal L, Dreyer D. Higher-order ghost state. In: Proc. of the 21st ACM SIGPLAN Int’l Conf. on Functional Programming (ICFP). Nara: Association for Computing Machinery, 2016. 256–269. [doi: 10.1145/2951913.2951943]
    [25] Jung R, Swasey D, Sieczkowski F, Svendsen K, Turon A, Birkedal L, Dreyer D. Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning. ACM SIGPLAN Notices, 2015, 50(1): 637–650.
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

何韬,董威,文艳军. GhostFunc: 一种针对Rust操作系统内核的验证方法.软件学报,2025,36(8):1-18

Copy
Share
Article Metrics
  • Abstract:47
  • PDF: 54
  • HTML: 0
  • Cited by: 0
History
  • Received:August 25,2024
  • Revised:October 14,2024
  • Online: March 26,2025
You are the first2037993Visitors
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