Automated deductive verification of systems software

Software has become an integral part of our everyday lives, and so is our reliance on his correct functioning. Systems software lies at the heart of computer systems, consequently ensuring its reliability and security is of paramount importance. This thesis explores automated deductive verification for increasing reliability and security of systems software. The thesis is comprised of the three main threads. The first thread describes how the state-of-the art deductive verification techniques can help in developing more secure operating system. We have developed a prototype of an Android-based operating system with strong assurance guarantees. Operating systems code heavily relies on mutable data structures. In our experience, reasoning about such pointer-manipulating programs was the hardest aspect of the operating system verification effort because correctness criteria describes intricate combinations of structure (shape), content (data), and separation. Thus, in the second thread, we explore design and development of an automated verification system for assuring correctness of pointer-manipulating programs using an extension of Hoare’s logic for reasoning about programs that access and update heap allocated data-structures. We have developed a verification framework that allows reasoning about C programs using only domain specific code annotations. The same thread contains a novel idea that enables efficient runtime checking of assertions that can express properties of dynamically manipulated linked-list data structures. Finally, we describe the work that paves a new way for reasoning about distributed protocols. We propose certified program models, where an executable language (such as C) is used for modelling – an executable language enables testing, and emerging program verifiers for mainstream executable languages enable certification of such models. As an instance of this approach, concurrent C code is used for modelling and a program verifier for concurrent C (VCC from Microsoft Research) is used for certification of new class of systems software that serves as a backbone for efficient distributed data storage