Mind the Gap: A Verification Framework for Low-Level C

Select |




Print


Winwood, Simon; Klein, Gerwin; Sewell, Thomas; Andronick, June; Cock, David; Norrish, Michael

Winwood, Simon; Klein, Gerwin; Sewell, Thomas; Andronick, June; Cock, David; Norrish, Michael


2009-08-20


Conference Material


TPHOLs


Munich, Germany


500-515


This paper presents the formal Isabelle/HOL framework we use to prove refinement between an executable, monadic specification and the C implementation of the seL4 microkernel. We describe the refinement framework itself, the automated tactics it supports, and the connection to our previous C verification framework. We also report on our experience in applying the framework to seL4. The characteristics of this microkernel verification are the size of the target (8,700 lines of C code), the treatment of low-level programming constructs, the focus on high performance, and the large subset of the C programming language addressed, which includes pointer arithmetic and type-unsafe code.


Springer


seL4, Isabelle, OS verification, C


https://doi.org/10.1007/978-3-642-03359-9_34


http://www.springerlink.com/content/m853h8912641/?p=6c938061f299441bbb60953e185385ec&pi=72


nicta:1842


Winwood, Simon; Klein, Gerwin; Sewell, Thomas; Andronick, June; Cock, David; Norrish, Michael. Mind the Gap: A Verification Framework for Low-Level C. In: S. Berghofer, T. Nipkow, C. Urban, M. Wenzel Editor, editor/s. TPHOLs; Munich, Germany. Springer; 2009-08-20. 500-515. https://doi.org/10.1007/978-3-642-03359-9_34



Loading citation data...

Citation counts
(Requires subscription to view)