Email Gateway (Aug 19 2022 at 14:57): Email Gateway (Aug 19 2022 at 14:57):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
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)
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.
http://afp.sf.net/entries/CISC-Kernel.shtml
Enjoy!
Gerwin
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.
Last updated: Apr 25 2024 at 04:18 UTC