Using Isabelle/HOL to Develop and Maintain Separation Invariants for an Operating System (Extended Abstract)
Authors: Holger Blasum, Oto Havle, Bruno Langenstein, Yakoub Nemouchi, Julien Schmaltz, Werner Stephan, Sergey Tverdyshev, Freek Verbeek and Burkhart Wolff
Paper Information
| Title: | Using Isabelle/HOL to Develop and Maintain Separation Invariants for an Operating System (Extended Abstract) |
| Authors: | Holger Blasum, Oto Havle, Bruno Langenstein, Yakoub Nemouchi, Julien Schmaltz, Werner Stephan, Sergey Tverdyshev, Freek Verbeek and Burkhart Wolff |
| Proceedings: | Isabelle 2014 Papers (Unrefereed) |
| Editors: | Tobias Nipkow, Lawrence Paulson and Makarius Wenzel |
| Keywords: | MILS (multiple independent levels of security), separation kernel, IPC API, events API |
| Abstract: | ABSTRACT. We describe work on an Isabelle model for the specification of a separation kernel done within the EURO-MILS project |
| Pages: | 6 |
| Talk: | Jul 13 16:30 |
| Paper: |  |