Formal API Specification of the PikeOS Separation Kernel

  • Freek Verbeek
  • Oto Havle
  • Julien Schmaltz
  • Sergey Tverdyshev
  • Holger Blasum
  • Bruno Langenstein
  • Werner Stephan
  • Burkhart Wolff
  • Yakoub Nemouchi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9058)

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.

Copyright information

© Springer International Publishing Switzerland 2015

Authors and Affiliations

  • Freek Verbeek
    • 1
    • 2
  • Oto Havle
    • 3
  • Julien Schmaltz
    • 4
  • Sergey Tverdyshev
    • 3
  • Holger Blasum
    • 3
  • Bruno Langenstein
    • 5
  • Werner Stephan
    • 5
  • Burkhart Wolff
    • 6
  • Yakoub Nemouchi
    • 6
  1. 1.Open University of The NetherlandsHeerlenThe Netherlands
  2. 2.Radboud University NijmegenNijmegenThe Netherlands
  3. 3.SYSGO AGKlein-winternheimGermany
  4. 4.Eindhoven University of TechnologyEindhovenThe Netherlands
  5. 5.DFKI GmbHKaiserslauternGermany
  6. 6.University Paris-SudOrsayFrance

Personalised recommendations