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 securityrelevant 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.
Cite
CITATION STYLE
Verbeek, F., Havle, O., Schmaltz, J., Tverdyshev, S., Blasum, H., Langenstein, B., … Nemouchi, Y. (2015). Formal API specification of the PikeOS separation kernel. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9058, pp. 375–389). Springer Verlag. https://doi.org/10.1007/978-3-319-17524-9_26
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
