Formal verification of C systems code: Structured types, separation logic and theorem proving
Tuch, Harvey
2009-04-02
Journal Article
Journal of Automated Reasoning
42
2-4
125-187
Systems code is almost universally written in the C programming language or a variant. C has a very low level of type and memory abstraction and formal reasoning about C systems code requires a memory model that is able to capture the semantics of C pointers and types. At the same time, proof-based verification demands abstraction, in particular from the aliasing and frame problems. In this paper we present a study in the mechanisation of two proof abstractions for pointer program verification in the Isabelle/HOL theorem prover, based on a low-level memory model for C. The language's type system presents challenges for the multiple independent typed heaps (Burstall-Bornat) and separation logic proof techniques. In addition to issues arising from explicit value size/alignment, padding, type-unsafe casts and pointer address arithmetic, structured types such as C's arrays and structs are problematic due to the non-monotonic nature of pointer and lvalue validity in the presence of the unary -operator. For example, type-safe updates through pointers to fields of a struct break the independence of updates across typed heaps or separating-and-conjuncts. We provide models and rules that are able to cope with these language features and types, eschewing common over-simplifications and utilising expressive shallow embeddings in higher-order logic. Two case studies are provided that demonstrate the applicability of the mechanised models to real-world systems code; a working of the standard in-place list reversal example and an overview of the verification of the L4 microkernel's memory allocator.
http://www.springerlink.com/content/100280/
1573-0670
nicta:2324
Tuch, Harvey. Formal verification of C systems code: Structured types, separation logic and theorem proving. Journal of Automated Reasoning. 2009-04-02; 42(2-4):125-187. http://hdl.handle.net/102.100.100/111168?index=1
Loading citation data...
Citation counts
(Requires subscription to view)