|
Formal
Specification
of
a
Generic
Separation
Kernel
Title: |
Formal Specification of a Generic Separation Kernel |
Authors:
|
Freek Verbeek (Freek /dot/ Verbeek /at/ ou /dot/ nl),
Sergey Tverdyshev (stv /at/ sysgo /dot/ com),
Oto Havle (oha /at/ sysgo /dot/ com),
Holger Blasum (holger /dot/ blasum /at/ sysgo /dot/ com),
Bruno Langenstein (langenstein /at/ dfki /dot/ de),
Werner Stephan (stephan /at/ dfki /dot/ de),
Yakoub Nemouchi (yakoub /dot/ nemouchi /at/ york /dot/ ac /dot/ uk),
Abderrahmane Feliachi (abderrahmane /dot/ feliachi /at/ lri /dot/ fr),
Burkhart Wolff and
Julien Schmaltz (Julien /dot/ Schmaltz /at/ ou /dot/ nl)
|
Submission date: |
2014-07-18 |
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.
This document corresponds to the deliverable D31.1 of the EURO-MILS
Project http://www.euromils.eu. |
BibTeX: |
@article{CISC-Kernel-AFP,
author = {Freek Verbeek and Sergey Tverdyshev and Oto Havle and Holger Blasum and Bruno Langenstein and Werner Stephan and Yakoub Nemouchi and Abderrahmane Feliachi and Burkhart Wolff and Julien Schmaltz},
title = {Formal Specification of a Generic Separation Kernel},
journal = {Archive of Formal Proofs},
month = jul,
year = 2014,
note = {\url{http://isa-afp.org/entries/CISC-Kernel.html},
Formal proof development},
ISSN = {2150-914x},
}
|
License: |
BSD License |
Status: [ok] |
This is a development version of this entry. It might change over time
and is not stable. Please refer to release versions for citations.
|
|