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 thesis, we study the mechanisation of a series of models, from semantic to separation logic, for achieving this abstraction when performing interactive theorem-prover based verification of C systems code in higher- order logic. We do not commit common oversimplifications, but correctly deal with C's model of programming language values and the heap, while developing the ability to reason abstractly and efficiently. We validate our work by demonstrating that the models are applicable to real, security- and safety-critical code by formally verifying the memory allocator of the L4 microkernel. All formalisations and proofs have been developed and machine-checked in the Isabelle/HOL theorem prover.
| Identifer | oai:union.ndltd.org:ADTP/257802 |
| Date | January 2008 |
| Creators | Tuch, Harvey, Computer Science & Engineering, Faculty of Engineering, UNSW |
| Publisher | Publisher:University of New South Wales. Computer Science & Engineering |
| Source Sets | Australiasian Digital Theses Program |
| Language | English |
| Detected Language | English |
| Rights | http://unsworks.unsw.edu.au/copyright, http://unsworks.unsw.edu.au/copyright |
Page generated in 0.1753 seconds