### 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.

### License

BSD License

### Topics

- Computer science/Security

### Session CISC-Kernel

- Option_Binders
- List_Theorems
- K
- SK
- ISK
- CISK
- Step_configuration
- Step_policies
- Step
- Step_invariants
- Step_vpeq
- Step_vpeq_locally_respects
- Step_vpeq_weakly_step_consistent
- Separation_kernel_model
- Link_separation_kernel_model_to_CISK

## Cite

×

CISC-Kernel-AFP

    @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   = {July},
      year    = {2014},
      note    = {\url{https://isa-afp.org/entries/CISC-Kernel.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Jul 18, 2014 : Isabelle2013-2