Article

Applying source-code verification to a microkernel: the VFiasco project

Authors:

Michael Hohmuth,

Hendrik Tews,

Shane G. StephensAuthors Info & Claims

EW 10: Proceedings of the 10th workshop on ACM SIGOPS European workshop

Pages 165 - 169

https://doi.org/10.1145/1133373.1133405

Published: 01 July 2002 Publication History

Get Access

Abstract

We present the VFiasco project, in which we apply source-code verification to a complete operating-system kernel written in C++. The aim of the VFiasco project is to establish security-relevant properties of the Fiasco microkernel.Source-code verification works by reasoning about the semantics of the full source code of a program. Traditionally it is limited to small programs written in an academic programming language. The project's main challenges are to enable high-level reasoning about typed data starting from only low-level knowledge about the hardware, and to develop a clean semantics for the subset of C++ used by the kernel. In this extended abstract we present our ideas for tackling these challenges. We focus on a type-safe object store that is based on a hardware model that closely resembles the IA32 virtual-memory architecture and on guarantees provided by the kernel itself. We also briefly touch on the semantics for C++.Please find the full version of this paper at http://www.vfiasco.org/objstore.pdf.

References

[1]

D. Engler, D. Yu Chen, S. Hallem, A. Chou, and B. Chelf. Bugs as deviant behavior: A general approach to inferring errors in systems code. In Proceedings of the 18th ACM Symposium on Operating Systems Principles (SOSP-01), 2001.]]

Digital Library

Google Scholar

[2]

M. Hohmuth and H. Härtig. Pragmatic nonblocking synchronization for real-time systems. In USENIX Annual Technical Conference, Boston, MA, June 2001.]]

Digital Library

Google Scholar

[3]

M. Hohmuth, H. Tews, and S. G. Stephens. Applying source-code verification to a microkernel --- the VFiasco project. Technical Report TUD--FI02--03--März 2002, Dresden University of Technology, 2002. Available from URL: http://www.vfiasco.org/objstore.pdf]]

Google Scholar

[4]

M. Huisman and B. Jacobs. Java program verification via a Hoare logic with abrupt termination. In T. Maibaum, editor, Fundamental Approaches to Software Engineering, number 1783 in LNCS, 2000.]]

Digital Library

Google Scholar

[5]

X. Leroy, D. Doligez, J. Garrigue, D. Rémy, and J. Vouillon. The Objective Caml system, 2001. Available at URL http://caml.inria.fr/ocaml/.]]

Google Scholar

[6]

X. Liu, C. Kreitz, R. van Renesse, J. Hickey, M. Hayden, K. P. Birman, and R. L. Constable. Building reliable, high-performance communication systems from components. In 17th ACM Symposium on Operating System Principles (SOSP), pages 80--92, Kiawah Island, SC, December 1999.]]

Digital Library

Google Scholar

[7]

George C. Necula. Proof-carrying code. In Conference Record of POPL '97: The 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 106--119, Paris, France, 15--17 1997.]]

Digital Library

Google Scholar

[8]

L. C. Paulson. Isabelle: A Generic Theorem Prover. Number 828 in LNCS. Springer, Berlin, 1994.]]

Google Scholar

[9]

P. Tullmann, J. Turner, J. McCorquodale, J. Lepreau, A. Chitturi, and G. Back. Formal methods: A practical tool for OS implementors. In Workshop on Hot Topics in Operating Systems, pages 20--25, 1997.]]

Digital Library

Google Scholar

[10]

J. van den Berg, M. Huisman, B. Jacobs., and E. Poll. A type-theoretic memory model for verification of sequential Java programs. In D. Bert, C. Choppy, and P. Mosses, editors, WADT '99, number 1827 in LNCS, pages 1--21, 1999.]]

Digital Library

Google Scholar

Cited By

View all

Chen FXu WQian ZYang WLiu W(2020)Formal Verification of the Correctness of Operating System on Assembly Layer in Isabelle/HOLArtificial Intelligence and Security10.1007/978-981-15-8083-3_25(276-288)Online publication date: 13-Sep-2020
https://doi.org/10.1007/978-981-15-8083-3_25
Qian ZLiu YJin YXing XZhang MGong SLiu WYang WTan JZhang L(2018)Research on Formal Design and Verification of Operating SystemsEmbedded Systems Technology10.1007/978-981-13-1026-3_6(81-88)Online publication date: 10-Jul-2018
https://doi.org/10.1007/978-981-13-1026-3_6
Liang HZhang DPei XJia XLi GXu J(2016)A Correctness Verification Method for C Programs Based on VCC2016 IEEE 3rd International Conference on Cyber Security and Cloud Computing (CSCloud)10.1109/CSCloud.2016.30(172-177)Online publication date: Jun-2016
https://doi.org/10.1109/CSCloud.2016.30
Show More Cited By

Applying source-code verification to a microkernel: the VFiasco project

Recommendations

Applying formal verification to microkernel IPC at meta
CPP 2022: Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs

We use Iris, an implementation of concurrent separation logic in the Coq proof assistant, to verify two queue data structures used for inter-process communication in an operating system under development. Our motivations are twofold. First, we wish to ...
Comprehensive formal verification of an OS microkernel

We present an in-depth coverage of the comprehensive machine-checked formal verification of seL4, a general-purpose operating system microkernel.

We discuss the kernel design we used to make its verification tractable. We then describe the functional ...
Proving Memory Separation in a Microkernel by Code Level Verification
ISORCW '11: Proceedings of the 2011 14th IEEE International Symposium on Object/Component/Service-Oriented Real-Time Distributed Computing Workshops

Often, an integrated mixed-criticality system is built in an environment which provides separation functionality for available on-board resources. In this paper we treat such an environment: the PikeOS separation kernel--a commercial real-time embedded ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

EW 10: Proceedings of the 10th workshop on ACM SIGOPS European workshop

July 2002

258 pages

ISBN:9781450378062

DOI:10.1145/1133373

General Chair:
Gilles Muller,
Program Chair:
Eric Jul

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 ACM 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: 01 July 2002

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Acceptance Rates

Overall Acceptance Rate 37 of 37 submissions, 100%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

16
Total Citations
View Citations
225
Total Downloads

Downloads (Last 12 months)3
Downloads (Last 6 weeks)0

Reflects downloads up to 21 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Chen FXu WQian ZYang WLiu W(2020)Formal Verification of the Correctness of Operating System on Assembly Layer in Isabelle/HOLArtificial Intelligence and Security10.1007/978-981-15-8083-3_25(276-288)Online publication date: 13-Sep-2020
https://doi.org/10.1007/978-981-15-8083-3_25
Qian ZLiu YJin YXing XZhang MGong SLiu WYang WTan JZhang L(2018)Research on Formal Design and Verification of Operating SystemsEmbedded Systems Technology10.1007/978-981-13-1026-3_6(81-88)Online publication date: 10-Jul-2018
https://doi.org/10.1007/978-981-13-1026-3_6
Liang HZhang DPei XJia XLi GXu J(2016)A Correctness Verification Method for C Programs Based on VCC2016 IEEE 3rd International Conference on Cyber Security and Cloud Computing (CSCloud)10.1109/CSCloud.2016.30(172-177)Online publication date: Jun-2016
https://doi.org/10.1109/CSCloud.2016.30
Gong S(2013)Formal Model of Classic Operating System KernelAdvanced Materials Research10.4028/www.scientific.net/AMR.748.1020748(1020-1023)Online publication date: Aug-2013
https://doi.org/10.4028/www.scientific.net/AMR.748.1020
Cronkite-Ratcliff BHosking AEugster P(2013)Development of automatically verifiable systems using data representation synthesisProceedings of the 2013 companion publication for conference on Systems, programming, & applications: software for humanity10.1145/2508075.2514874(109-110)Online publication date: 26-Oct-2013
https://dl.acm.org/doi/10.1145/2508075.2514874
Qian ZHuang HSong F(2013)VTOS: Research on Methodology of “Light-Weight” Formal Design and Verification for Microkernel OSInformation and Communications Security10.1007/978-3-319-02726-5_2(17-32)Online publication date: 20-Nov-2013
https://dl.acm.org/doi/10.1007/978-3-319-02726-5_2
Vemuri DAl-Hamdani WWhitman MZafar H(2011)Measures to improve security in a microkernel operating systemProceedings of the 2011 Information Security Curriculum Development Conference10.1145/2047456.2047460(25-33)Online publication date: 30-Sep-2011
https://dl.acm.org/doi/10.1145/2047456.2047460
Zhu LZhang MHuang YShi JZhu H(2011)Formalizing Application Programming Interfaces of the OSEK/VDX Operating System SpecificationProceedings of the 2011 Fifth International Conference on Theoretical Aspects of Software Engineering10.1109/TASE.2011.12(27-34)Online publication date: 29-Aug-2011
https://dl.acm.org/doi/10.1109/TASE.2011.12
Klein G(2009)Operating system verification—An overviewSadhana10.1007/s12046-009-0002-434:1(27-69)Online publication date: 16-Jul-2009
https://doi.org/10.1007/s12046-009-0002-4
Tuch H(2009)Formal Verification of C Systems CodeJournal of Automated Reasoning10.1007/s10817-009-9120-242:2-4(125-187)Online publication date: 1-Apr-2009
https://dl.acm.org/doi/10.1007/s10817-009-9120-2
Show More Cited By

View Options

Get Access

Login options

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

Cited By

Recommendations

Applying formal verification to microkernel IPC at meta

Comprehensive formal verification of an OS microkernel

Proving Memory Separation in a Microkernel by Code Level Verification