Secure Microkernels, State Monads and Scalable Refinement

Select |




Print


Cock, David; Klein, Gerwin; Sewell, Thomas

Cock, David; Klein, Gerwin; Sewell, Thomas


2008-08-18


Conference Material


Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics


Montreal, Canada


167-182


We present a scalable, practical Hoare Logic and refinement calculus for the nondeterministic state monad with exceptions and failure in Isabelle/HOL. The emphasis of this formalisation is on large-scale verification of imperative-style functional programs, rather than expressing monad calculi in full generality. We achieve scalability in two dimensions. The method scales to multiple team members working productively and largely independently on a single proof and also to large programs with large and complex properties. We report on our experience in applying the techniques in an extensive (100K lines of proof) case study---the formal verification of an executable model of the seL4 operating system microkernel.


Springer


State Monad, Refinement, Microkernel, Isabelle/HOL, seL4


https://doi.org/10.1007/978-3-540-71067-7_16


http://www.springerlink.com/content/60516t16g2318146/


nicta:483


Cock, David; Klein, Gerwin; Sewell, Thomas. Secure Microkernels, State Monads and Scalable Refinement. In: Otmane Ait Mohamed, César Muñoz, So?ène Tahar Editor, editor/s. Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics; Montreal, Canada. Springer; 2008-08-18. 167-182. https://doi.org/10.1007/978-3-540-71067-7_16



Loading citation data...

Citation counts
(Requires subscription to view)