Abstract
The Verisoft project aims at the pervasive formal verification of entire computer systems. In particular, the seamless verification of the academic system is attempted. This system consists of hardware (processor and devices) on top of which runs a microkernel, an operating system, and applications. In this paper we define the computation model CVM (communicating virtual machines) in which concurrent user processes interact with a generic microkernel written in C. We outline the correctness proof for concrete kernels, which implement this model. This result represents a crucial step towards the verification of a kernel, e.g. that in the academic system. We report on the current status of the formal verification.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Hutt, A.E., Hoyt, D.B., Bosworth, S. (eds.): Computer Security Handbook. John Wiley & Sons, Inc., Chichester (1995)
Shapiro, J.S., Hardy, N.: Eros: A principle-driven operating system from the ground up. IEEE Software 19, 26–33 (2002)
Rushby, J.: Proof of separability: A verification technique for a class of security kernels. In: Proc. 5th International Symposium on Programming, pp. 352–367. Springer, Turin (1982)
Wulf, W.A., Cohen, E.S., Corwin, W.M., Jones, A.K., Levin, R., Pierson, C., Pollack, F.J.: HYDRA: The kernel of a multiprocessor operating system. CACM 17(6) (1974)
Pfitzmann, B., Riordan, J., Stüble, C., Waidner, M., Weber, A.: The PERSEUS system architecture. In: Fox, D., Köhntopp, M., Pfitzmann, A. (eds.) VIS 2001, Sicherheit in komplexen IT-Infrastrukturen, pp. 1–18. Vieweg Verlag (2001)
Liedtke, J.: On micro-kernel construction. In: Proceedings of the 15th ACM Symposium on Operating systems principles, pp. 237–250. ACM Press, New York (1995)
The Common Criteria Project Sponsoring Organisations: Common Criteria for Information Technology Security Evaluation version 2.1, Part I (1999), http://www.commoncriteriaportal.org/public/files/ccpart1v21.pdf
Bevier, W.R.: Kit: A study in operating system verification. IEEE Transactions on Software Engineering 15, 1382–1396 (1989)
OSEK group: OSEK/VDX time-triggered operating system (2001), http://www.osek-vdx.org/mirror/ttos10.pdf
The Verisoft Consortium: The Verisoft project (2003), http://www.verisoft.de/
Aho, A.V., Hopcroft, J.E., Ullman, J.: Data Structures and Algorithms. Addison-Wesley Longman Publishing Co., Inc., Amsterdam (1983)
Dalinger, I., Hillebrand, M., Paul, W.: On the verification of memory management mechanisms. Technical report, Verisoft project (2005), http://www.verisoft.de/.rsrc/SubProject2/verificationmm.pdf
Leinenbach, D., Paul, W., Petrova, E.: Compiler verification in the context of pervasive system verification. Draft manuscript (2005)
Hennessy, J.L., Patterson, D.A.: Computer Architecture: A Quantitative Approach. Morgan Kaufmann, San Mateo (1996)
Müller, S.M., Paul, W.J.: Computer Architecture: Complexity and Correctness. Springer, Heidelberg (2000)
Nielson, H.R., Nielson, F.: Semantics with Applications: A Formal Introduction. John Wiley & Sons, Inc., New York (1999)
Winskel, G.: The formal semantics of programming languages. The MIT Press, Cambridge (1993)
Norrish, M.: C formalised in HOL. Technical Report UCAM-CL-TR-453, University of Cambridge, Computer Laboratory (1998)
Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)
Beyer, S., Jacobi, C., Kröning, D., Leinenbach, D., Paul, W.: Instantiating uninterpreted functional units and memory system: Functional verification of the VAMP processor. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 51–65. Springer, Heidelberg (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gargano, M., Hillebrand, M., Leinenbach, D., Paul, W. (2005). On the Correctness of Operating System Kernels. In: Hurd, J., Melham, T. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2005. Lecture Notes in Computer Science, vol 3603. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11541868_1
Download citation
DOI: https://doi.org/10.1007/11541868_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-28372-0
Online ISBN: 978-3-540-31820-0
eBook Packages: Computer ScienceComputer Science (R0)