Formal Specification of a Generic Separation Kernel (Q7361293)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry CISC-Kernel
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Formal Specification of a Generic Separation Kernel |
AFP entry CISC-Kernel |
Statements
18 July 2014
0 references
Freek Verbeek
0 references
Sergey Tverdyshev
0 references
Oto Havle
0 references
Holger Blasum
0 references
Bruno Langenstein
0 references
Werner Stephan
0 references
Yakoub Nemouchi
0 references
Abderrahmane Feliachi
0 references
Burkhart Wolff
0 references
Julien Schmaltz
0 references
Formal Specification of a Generic Separation Kernel (English)
0 references
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. This document corresponds to the deliverable D31.1 of the EURO-MILS Project http://www.euromils.eu .
0 references
