research-article

Public Access

Building certified concurrent OS kernels

Authors:

Jérémie Koenig,

Xiongnan (Newman) Wu,

Vilhelm Sjöberg,

David CostanzoAuthors Info & Claims

Communications of the ACM, Volume 62, Issue 10

Pages 89 - 99

https://doi.org/10.1145/3356903

Published: 24 September 2019 Publication History

All formats PDF

Abstract

Operating system (OS) kernels form the backbone of system software. They can have a significant impact on the resilience and security of today's computers. Recent efforts have demonstrated the feasibility of formally verifying simple general-purpose kernels, but they have ignored the important issues of concurrency, which include not just user and I/O concurrency on a single core, but also multi-core parallelism with fine-grained locking. In this work, we present CertiKOS, a novel compositional framework for building verified concurrent OS kernels. Concurrency allows interleaved execution of programs belonging to different abstraction layers and running on different CPUs/threads. Each such layer can have a different set of observable events. In CertiKOS, these layers and their observable events can be formally specified, and each module can then be verified at the abstraction level it belongs to. To link all the verified pieces together, CertiKOS enforces a so-called contextual refinement property for every such piece, which states that the implementation will behave like its specification under any concurrent context with any valid interleaving. Using CertiKOS, we have successfully developed a practical concurrent OS kernel, called mC2, and built the formal proofs of its correctness in Coq. The mC2 kernel is written in 6500 lines of C and x86 assembly and runs on stock x86 multicore machines. To our knowledge, this is the first correctness proof of a general-purpose concurrent OS kernel with fine-grained locking.

References

[1]

Alkassar, E., Hillebrand, M.A., Paul, W.J., Petrova, E. Automated verification of a small hypervisor. In Proceedings of 3rd International Conference on Verified Software: Theories, Tools, Experiments (VSTTE) (2010), 40--54.

[2]

Anderson, T., Dahlin, M. Operating Systems Principles and Practice. Recursive Books, 2011 (Figure 5.14).

[3]

Belay, A., Bittau, A., Mashtizadeh, A., Mazières, D., Kozyrakis, C. Dune: Safe user-level access to privileged CPU features. In Proceedings of 10th USENIX Symposium on Operating Systems Design and Implementation (OSDI'12) (2012), 335--348.

[4]

Carbonneaux, Q., Hoffmann, J., Ramananandro, T., Shao, Z. End-to-end verification of stackspace bounds for C programs. In Proceedings of 2014 ACM Conference on Programming Language Design and Implementation (PLDI'14) (2014), 270--281.

[5]

Chen, H., Wu, X., Shao, Z., Lockerman, J., Gu, R. Toward compositional verification of interruptible OS kernels and device drivers. In Proceedings of 2016 ACM Conference on Programming Language Design and Implementation (PLDI'16) (2016), 431--447.

Digital Library

[6]

Chen, H., Ziegler, D., Chajed, T., Chlipala, A., Kaashoek, M.F., Zeldovich, N. Using Crash Hoare logic for certifying the FSCQ file system. In Proceedings of 25th ACM Symposium on Operating System Principles (SOSP) (2015), 18--37.

Digital Library

[7]

Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S. VCC: A practical system for verifying concurrent C. In Proceedings of 22nd International Conference on Theorem Proving in Higher Order Logics (2009), 23--42.

Digital Library

[8]

Costanzo, D., Shao, Z., Gu, R. End-to-end verification of information-flow security for C and assembly programs. In Proceedings of 2016 ACM Conference on Programming Language Design and Implementation (PLDI'16) (2016), 648--664.

Digital Library

[9]

Dijkstra, E.W. The structure of the "THE"-multiprograrnrning system. Commun. ACM, (1968), 341--346.

[10]

Gu, R., Koenig, J., Ramananandro, T., Shao, Z., Wu, X., Weng, S.-C., Zhang, H., Guo, Y. Deep specifications and certified abstraction layers. In Proceedings of 42nd ACM Symposium on Principles of Programming Languages (POPL'15) (2015), 595--608.

Digital Library

[11]

Gu, R., Shao, Z., Chen, H., Wu, X.N., Kim, J., Sjöberg, V., Costanzo, D. Certikos: An extensible architecture for building certified concurrent OS kernels. In Proceedings of 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI'16) (2016), 653--669.

[12]

Gu, R., Shao, Z., Kim, J., Wu, X.N., Koenig, J., Sjöberg, V., Chen, H., Costanzo, D., Ramananandro, T. Certified concurrent abstraction layers. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation (2018), ACM, 646--661.

Digital Library

[13]

Hawblitzel, C., Howell, J., Lorch, J.R., Narayan, A., Parno, B., Zhang, D., Zill, B. Ironclad apps: End-to-end security via automated full-system verification. In Proceedings of 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI'14) (2014), 165--181

[14]

Hawblitzel, C., Petrank, E., Qadeer, S., Tasiran, S. Automated and modular refinement reasoning for concurrent programs. In International Conference on Computer Aided Verification (2015), Springer 449--465.

[15]

Herlihy, M., Shavit, N. The Art of Multiprocessor Programming. Morgan Kaufmann, 2008.

Digital Library

[16]

Kim, J., Sjöberg, V., Gu, R., Shao, Z. Safety and liveness of MCS lock---Layer by layer. In Asian Symposium on Programming Languages and Systems (2017), Springer, 273--297.

[17]

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 Proceedings of 22nd ACM Symposium on Operating Systems Principles (SOSP) (2009), ACM, 207--220.

Digital Library

[18]

Lampson, B.W. Experience with processes and monitors in Mesa. Commun. ACM 23, 2 (1980).

Digital Library

[19]

Leroy, X. Formal verification of a realistic compiler. Commun. ACM 52, 7 (2009), 107--115.

Digital Library

[20]

Liang, H., Feng, X. A program logic for concurrent objects under fair scheduling. In Proceedings of 43rd ACM Symposium on Principles of Programming Languages (POPL'16) (2016), 385--399.

Digital Library

[21]

Mellor-Crummey, J.M., Scott, M.L. Algorithms for scalable synchronization on shared-memory multiprocessors. ACM T. Comput. Syst. 9, 1 (1991), 21--65.

Digital Library

[22]

Peters, S., Danis, A., Elphinstone, K., Heiser, G. For a microkernel, a big lock is fine. In APSys '15 Asia Pacific Workshop on Systems, Tokyo, Japan (2015).

Digital Library

[23]

von Tessin, M. The clustered multikernel: An approach to formal verification of multiprocessor operating-system kernels. PhD thesis, School of Computer Science and Engineering, The University of New South Wales (2013).

[24]

Xu, F., Fu, M., Feng, X., Zhang, X., Zhang, H., Li, Z. A practical verification framework for preemptive OS kernels. In Proceedings of 28th International Conference on Computer-Aided Verification (CAV), Part II (2016), 59--79.

Cited By

Li XChen SGuan YZhang QWang GShi Z(2024)Refinement Verification of OS Services based on a Verified Preemptive MicrokernelFundamental Approaches to Software Engineering10.1007/978-3-031-57259-3_9(188-209)Online publication date: 6-Apr-2024
https://doi.org/10.1007/978-3-031-57259-3_9
Feng ZYongwang ZYang LJun S(2024)A Comprehensive Formal Specification of ARINC 653 With Conformity ProofSoftware Testing, Verification and Reliability10.1002/stvr.1901Online publication date: Oct-2024
https://doi.org/10.1002/stvr.1901
Zhang FZhang LZhao YLiu YSun J(2023)Refinement-based Specification and Analysis of Multi-core ARINC 653 Using Event-BFormal Aspects of Computing10.1145/361718335:4(1-29)Online publication date: 21-Nov-2023
https://dl.acm.org/doi/10.1145/3617183
Show More Cited By

Index Terms

Building certified concurrent OS kernels

Recommendations

Certified concurrent abstraction layers
PLDI 2018: Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation

Concurrent abstraction layers are ubiquitous in modern computer systems because of the pervasiveness of multithreaded programming and multicore hardware. Abstraction layers are used to hide the implementation details (e.g., fine-grained synchronization) ...
Certified concurrent abstraction layers
PLDI '18

Concurrent abstraction layers are ubiquitous in modern computer systems because of the pervasiveness of multithreaded programming and multicore hardware. Abstraction layers are used to hide the implementation details (e.g., fine-grained synchronization) ...
Towards certified separate compilation for concurrent programs
PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation

Certified separate compilation is important for establishing end-to-end guarantees for certified systems consisting of multiple program modules. There has been much work building certified compilers for sequential programs. In this paper, we propose a ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Communications of the ACM

Communications of the ACM Volume 62, Issue 10

October 2019

89 pages

ISSN:0001-0782

EISSN:1557-7317

DOI:10.1145/3363418

Editor:
Andrew A. Chien
Association for Computing Machinery, New York, NY

Issue’s Table of Contents

Copyright © 2019 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 24 September 2019

Published in CACM Volume 62, Issue 10

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Research-article
Research
Refereed

Funding Sources

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

24
Total Citations
View Citations
19,531
Total Downloads

Downloads (Last 12 months)2,579
Downloads (Last 6 weeks)106

Reflects downloads up to 14 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Li XChen SGuan YZhang QWang GShi Z(2024)Refinement Verification of OS Services based on a Verified Preemptive MicrokernelFundamental Approaches to Software Engineering10.1007/978-3-031-57259-3_9(188-209)Online publication date: 6-Apr-2024
https://doi.org/10.1007/978-3-031-57259-3_9
Feng ZYongwang ZYang LJun S(2024)A Comprehensive Formal Specification of ARINC 653 With Conformity ProofSoftware Testing, Verification and Reliability10.1002/stvr.1901Online publication date: Oct-2024
https://doi.org/10.1002/stvr.1901
Zhang FZhang LZhao YLiu YSun J(2023)Refinement-based Specification and Analysis of Multi-core ARINC 653 Using Event-BFormal Aspects of Computing10.1145/361718335:4(1-29)Online publication date: 21-Nov-2023
https://dl.acm.org/doi/10.1145/3617183
Fox AStockwell GXiong SBecker HMulligan DPetri GChong N(2023)A Verification Methodology for the Arm® Confidential Computing Architecture: From a Secure Specification to Safe ImplementationsProceedings of the ACM on Programming Languages10.1145/35860407:OOPSLA1(376-405)Online publication date: 6-Apr-2023
https://dl.acm.org/doi/10.1145/3586040
Qian ZZhong SSun GXing XJin Y(2023)A Formal Approach to Design and Security Verification of Operating Systems for Intelligent Transportation Systems Based on Object ModelIEEE Transactions on Intelligent Transportation Systems10.1109/TITS.2022.322438524:12(15459-15467)Online publication date: 1-Dec-2023
https://dl.acm.org/doi/10.1109/TITS.2022.3224385
Qian ZXia RSun GXing XXia K(2023)A measurable refinement method of design and verification for micro-kernel operating systems in communication networkDigital Communications and Networks10.1016/j.dcan.2022.03.0249:5(1070-1079)Online publication date: Oct-2023
https://doi.org/10.1016/j.dcan.2022.03.024
Liu MShao ZChen HYoon MKim J(2022)Compositional virtual timelines: verifying dynamic-priority partitions with algorithmic temporal isolationProceedings of the ACM on Programming Languages10.1145/35632906:OOPSLA2(60-88)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563290
Li YWeirich S(2022)Program adverbs and Tlön embeddingsProceedings of the ACM on Programming Languages10.1145/35476326:ICFP(312-342)Online publication date: 31-Aug-2022
https://dl.acm.org/doi/10.1145/3547632
Sammler MHammond ALepigre RCampbell BPichon-Pharabod JDreyer DGarg DSewell PJhala RDillig I(2022)Islaris: verification of machine code against authoritative ISA semanticsProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3519939.3523434(825-840)Online publication date: 9-Jun-2022
https://dl.acm.org/doi/10.1145/3519939.3523434
Mulder IKrebbers RGeuvers HJhala RDillig I(2022)Diaframe: automated verification of fine-grained concurrent programs in IrisProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3519939.3523432(809-824)Online publication date: 9-Jun-2022
https://dl.acm.org/doi/10.1145/3519939.3523432
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Digital Edition

View this article in digital edition.

Digital Edition

Magazine Site

View this article on the magazine site (external)

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents