@inproceedings{60370ca8a0b34dda89bbbab96a67cb23,
title = "Formal API specification of the PikeOS separation kernel",
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.",
author = "F. Verbeek and O. Havle and J. Schmaltz and S. Tverdyshev and H. Blasum and B. Langenstein and W. Stephan and B. Wolff and Y. Nemouchi",
year = "2015",
doi = "10.1007/978-3-319-17524-9_26",
language = "English",
isbn = "978-3-319-17523-2",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "375--389",
editor = "K. Havelund and G. Holzmann and R. Joshi",
booktitle = "NASA Formal Methods",
address = "Germany",
note = "7th NASA Formal Methods Symposium (NFM 2015), April 27-29, 2015, Pasadena, CA, USA, NFM 2015 ; Conference date: 27-04-2015 Through 29-04-2015",
}