Implicit Assumptions in a Model for Separation Kernels

ABSTRACT. In joint work with several industrial and academic partners throughout Europe, we are working towards the certification of PikeOS -- an industrial separation kernel developed at SYSGO -- according to the highest level of the Common Criteria. We present a new generic model of separation kernels that includes interrupts, control and context switches. For this generic model, noninterference has been proven in the Isabelle/HOL theorem prover from proof obligations on the step function. Noninterference holds for all separation kernels which satisfy these assumptions. In this paper, we discuss this methodology for certification purposes. On the one hand, it is clear that our instantiation of the step function for PikeOS must satisfy the proof obligations. On the other hand, there are many implicit assumptions made in defining the run function, that is, in defining how the step function is applied. Based on work-in-progress, we address the issue of providing evidence that PikeOS indeed satisfies our generic notion of noninterference.