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

25 Citations (Scopus)
6 Downloads (Pure)


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
ISBN (Electronic)978-3-319-17524-9
ISBN (Print)978-3-319-17523-2
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
ISSN (Print)0302-9743


Conference7th NASA Formal Methods Symposium (NFM 2015), April 27-29, 2015, Pasadena, CA, USA
Abbreviated titleNFM 2015
Country/TerritoryUnited States
CityPasadena, CA


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

Cite this