Formal specification of a generic separation kernel

F. Verbeek, S. Tverdyshev, O. Havle, H. Blasum, B. Langenstein, W. Stephan, Y. Nemouchi, A. Feliachi, B. Wolff, J. Schmaltz

Research output: Contribution to journalArticleAcademicpeer-review

64 Downloads (Pure)

Abstract

Intransitive noninterference has been a widely studied topic in the last few decades. Several well-established methodologies apply interactive theorem proving to formulate a noninterference theorem over abstract academic models. In joint work with several industrial and academic partners throughout Europe, we are helping in the certification process of PikeOS, an industrial separation kernel developed at SYSGO. In this process, established theories could not be applied. We present a new generic model of separation kernels and a new theory of intransitive noninterference. The model is rich in detail, making it suitable for formal verification of realistic and industrial systems such as PikeOS. Using a refinement-based theorem proving approach, we ensure that proofs remain manageable.
Original languageEnglish
JournalArchive of Formal Proofs
Volume2014
Issue number2014-07-18
Publication statusPublished - 2014

Fingerprint Dive into the research topics of 'Formal specification of a generic separation kernel'. Together they form a unique fingerprint.

  • Cite this

    Verbeek, F., Tverdyshev, S., Havle, O., Blasum, H., Langenstein, B., Stephan, W., Nemouchi, Y., Feliachi, A., Wolff, B., & Schmaltz, J. (2014). Formal specification of a generic separation kernel. Archive of Formal Proofs, 2014(2014-07-18).