Formal API specification of the PikeOS separation kernel

F. Verbeek, O. Havle, J. Schmaltz, S. Tverdyshev, H. Blasum, B. Langenstein, W. Stephan, B. Wolff, Y. Nemouchi

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

14 Citations (Scopus)
6 Downloads (Pure)

Abstract

PikeOS is an industrial operating system for safety and security critical applications in, for example, avionics and automotive contexts. A consortium of several European partners from industry and academia works on the certification of PikeOS up to at least Common Criteria EAL5+, with "+" being applying formal methods compliant up to EAL7. We have formalized the hardware independent security-relevant part of PikeOS that is to be used in a certification context. Over this model, intransitive noninterference has been proven. We present the model and the methodology used to create the model. All results have been formalized in the Isabelle/HOL theorem prover.
Original languageEnglish
Title of host publicationNASA Formal Methods
Subtitle of host publication7th International Symposium, NFM 2015, Pasadena, CA, USA, April 27-29, 2015, Proceedings
EditorsK. Havelund, G. Holzmann, R. Joshi
Place of PublicationBerlin
PublisherSpringer
Pages375-389
ISBN (Electronic)978-3-319-17524-9
ISBN (Print)978-3-319-17523-2
DOIs
Publication statusPublished - 2015
Event7th NASA Formal Methods Symposium (NFM 2015), April 27-29, 2015, Pasadena, CA, USA - Pasadena, CA, United States
Duration: 27 Apr 201529 Apr 2015

Publication series

NameLecture Notes in Computer Science
Volume9058
ISSN (Print)0302-9743

Conference

Conference7th NASA Formal Methods Symposium (NFM 2015), April 27-29, 2015, Pasadena, CA, USA
Abbreviated titleNFM 2015
CountryUnited States
CityPasadena, CA
Period27/04/1529/04/15

Fingerprint Dive into the research topics of 'Formal API specification of the PikeOS separation kernel'. Together they form a unique fingerprint.

  • Cite this

    Verbeek, F., Havle, O., Schmaltz, J., Tverdyshev, S., Blasum, H., Langenstein, B., Stephan, W., Wolff, B., & Nemouchi, Y. (2015). Formal API specification of the PikeOS separation kernel. In K. Havelund, G. Holzmann, & R. Joshi (Eds.), NASA Formal Methods : 7th International Symposium, NFM 2015, Pasadena, CA, USA, April 27-29, 2015, Proceedings (pp. 375-389). (Lecture Notes in Computer Science; Vol. 9058). Springer. https://doi.org/10.1007/978-3-319-17524-9_26