Title: Formal Specification of a Generic Separation Kernel
Creators: Verbeek, F.; Tverdyshev, S.; Havle, O.; Blasum, H.; Langenstein, B.; Stephan, W.; Nemouchi, Y.; Feliachi, A.; Wolff, B.; Schmaltz, J.
Date of Archiving: 2014
Archive: Archive of Formal Proofs
Related links: http://afp.sourceforge.net/entries/CISC-Kernel.shtml
Publication type: Dataset
Access level : open access

Please use this identifier to cite or link to this item : http://hdl.handle.net/2066/151883   http://hdl.handle.net/2066/151883

Display more details
Key words: Intransitive noninterference
Generic Separation Kernel
Organization: Software Science
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.
Audience(s): Astronomy, astrophysics

This item appears in the following Collection(s)

Browse

Statistics