Nowadays formal methods are required for high assurance security and safety systems. Formal methods allow a precise specification and a deep analysis of system designs. However, usage of formal methods in a certification process can be very expensive. In this context, we analyse the security policy proposed by Greve et al in the theorem prover Isabelle/HOL. We show how this policy with some extensions can be applied in a modular way, and hence, reduce the number of formal models and artifacts to certify. Thus, we show how the security policy for a separation kernel is derived from the security policy of the micro-kernel that forms the basis of the separation kernel. We apply our approach to an example derived from an industrial real-time operating system. © 2011 Springer-Verlag.
CITATION STYLE
Tverdyshev, S. (2011). Extending the GWV security policy and its modular application to a separation kernel. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6617 LNCS, pp. 391–405). https://doi.org/10.1007/978-3-642-20398-5_28
Mendeley helps you to discover research relevant for your work.