Formal API Specification of the PikeOS Separation Kernel

  • Freek VerbeekEmail author
  • 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)


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.


Security Policy Atomic Action Proof Obligation Context Switch Covert Channel 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Kaiser, R., Wagner, S.: Evolution of the PikeOS microkernel. In: First International Workshop on Microkernels for Embedded Systems, p. 50 (2007)Google Scholar
  2. 2.
    Rushby, J.: Noninterference, transitivity, and channel-control security policies. SRI International, Computer Science Laboratory (1992)Google Scholar
  3. 3.
    van der Meyden, R.: What, indeed, is intransitive noninterference? In: Biskup, J., López, J. (eds.) Computer Security ESORICS 2007. LNCS, vol. 4734, pp. 235–250. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  4. 4.
  5. 5.
    Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., et al.: seL4: Formal verification of an OS kernel. In: Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles, pp. 207–220. ACM (2009)Google Scholar
  6. 6.
    Murray, T., Matichuk, D., Brassil, M., Gammie, P., Bourke, T., Seefried, S., Lewis, C., Gao, X., Klein, G.: seL4: from general purpose to a proof of information flow enforcement. In: 34th IEEE Symposium on Security and Privacy (2013)Google Scholar
  7. 7.
    Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: a proof assistant for higher-order logic (2012)Google Scholar
  8. 8.
    Jacob, J.: On the derivation of secure components. In: Proceedings of the IEEE Symposium on Security and Privacy, pp. 242–247, May 1989Google Scholar
  9. 9.
    Mantel, H., Sudbrock, H.: Comparing countermeasures against interrupt-related covert channels in an information-theoretic framework. In: Proceedings of 20th IEEE Computer Security Foundations Symposium (CSF 2007), pp. 326–340, July 2007Google Scholar
  10. 10.
    Goguen, J.A., Meseguer, J.: Unwinding and inference control (1984)Google Scholar
  11. 11.
    Mantel, H.: Information flow control and applications - bridging a gap -. In: Oliveira, J., Zave, P. (eds.) Formal Methods for Increasing Software Productivity (FME 2001). LNCS, vol. 2021, pp. 153–172. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  12. 12.
    Roscoe, A.W., Goldsmith, M.H.: What is intransitive noninterference? In: Proceedings of the 12th IEEE Computer Security Foundations Workshop, pp. 228–238 (1999)Google Scholar
  13. 13.
    von Oheimb, D.: Information flow control revisited: Noninfluence = noninterference + nonleakage. In: Samarati, P., Ryan, P., Gollmann, D., Molva, R. (eds.) Computer Security - ESORICS 2004. LNCS, vol. 3193, 225th edn, p. 243. Springer, Heidelberg (2004)Google Scholar
  14. 14.
    Leslie, R.: Dynamic intransitive noninterference. In: IEEE International Symposium on Secure Software Engineering (2006)Google Scholar
  15. 15.
    Engelhardt, K., van der Meyden, R., Zhang, C.: Intransitive noninterference in nondeterministic systems. In: Proceedings of the 2012 ACM Conference on Computer and Communications Security, pp. 869–880. ACM (2012)Google Scholar
  16. 16.
    Haigh, J.T., Young, W.D.: Extending the noninterference version of MLS for SAT. IEEE Trans. Softw. Eng. 13(2), 141–150 (1987)CrossRefGoogle Scholar
  17. 17.
    Whalen, M., Greve, D., Wagner, L.: Model checking information flow. In: Hardin, D.S. (ed.) Design and Verification of Microprocessor Systems for High-Assurance Applications, pp. 381–428. Springer, US (2010)CrossRefGoogle Scholar
  18. 18.
    Eggert, S., van der Meyden, R., Schnoor, H., Wilke, T.: The complexity of intransitive noninterference. In: 2011 IEEE Symposium on Security and Privacy (SP), pp. 196–211 (2011)Google Scholar
  19. 19.
    Murray, T., Matichuk, D., Brassil, M., Gammie, P., Klein, G.: Noninterference for operating system kernels. In: Hawblitzel, C., Miller, D. (eds.) Certified Programs and Proofs. LNCS, vol. 7679, pp. 126–142. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  20. 20.
    Klein, G., Andronick, J., Elphinstone, K., Murray, T.C., Sewell, T., Kolanski, R., Heiser, G.: Comprehensive formal verification of an OS microkernel. ACM Trans. Comput. Syst. 32(1), 2 (2014)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2015

Authors and Affiliations

  • Freek Verbeek
    • 1
    • 2
    Email author
  • 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