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

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

14 Citaten (Scopus)
6 Downloads (Pure)

Samenvatting

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.
Originele taal-2Engels
TitelNASA Formal Methods
Subtitel7th International Symposium, NFM 2015, Pasadena, CA, USA, April 27-29, 2015, Proceedings
RedacteurenK. Havelund, G. Holzmann, R. Joshi
Plaats van productieBerlin
UitgeverijSpringer
Pagina's375-389
ISBN van elektronische versie978-3-319-17524-9
ISBN van geprinte versie978-3-319-17523-2
DOI's
StatusGepubliceerd - 2015
Evenement7th NASA Formal Methods Symposium (NFM 2015), April 27-29, 2015, Pasadena, CA, USA - Pasadena, CA, Verenigde Staten van Amerika
Duur: 27 apr 201529 apr 2015

Publicatie series

NaamLecture Notes in Computer Science
Volume9058
ISSN van geprinte versie0302-9743

Congres

Congres7th NASA Formal Methods Symposium (NFM 2015), April 27-29, 2015, Pasadena, CA, USA
Verkorte titelNFM 2015
LandVerenigde Staten van Amerika
StadPasadena, CA
Periode27/04/1529/04/15
Ander7th International Symposium on Formal Methods

Vingerafdruk Duik in de onderzoeksthema's van 'Formal API specification of the PikeOS separation kernel'. Samen vormen ze een unieke vingerafdruk.

  • Citeer dit

    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 (editors), NASA Formal Methods : 7th International Symposium, NFM 2015, Pasadena, CA, USA, April 27-29, 2015, Proceedings (blz. 375-389). (Lecture Notes in Computer Science; Vol. 9058). Springer. https://doi.org/10.1007/978-3-319-17524-9_26