[isabelle] new in the AFP: CISC-Kernel

Formal Specification of a Generic Separation Kernel

Freek Verbeek         (Open University of The Netherlands)
Sergey Tverdyshev     (SYSGO AG)
Oto Havle             (SYSGO AG)
Holger Blasum         (SYSGO AG)
Bruno Langenstein     (DFKI GmbH)
Werner Stephan        (DFKI GmbH)
Yakoub Nemouchi       (University Paris Sud)
Abderrahmane Feliachi (University Paris Sud)
Burkhart Wolff        (University Paris Sud)
Julien Schmaltz       (Open University of The Netherlands)

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




The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.