Certifying Virtual Memory Manager Using Multiple Abstraction Levels
Last modified: Mon Dec 10 05:21:39 2012 GMT.
Abstraction is the main tool that makes the creation of complex software systems tractable. However, software verification using the Hoare-logic approach has only a few methods in its arsenal to make use of abstraction, with separation logic being the most popular. Combined with recursive predicates, separation logic can be used for defining abstract data types (ADTs) and information hiding in verification. But there are limits to its application: separation logic cannot be used to define abstractions that rely on the alteration of operational semantics of primitive operations. One example of such abstraction is virtual memory: in the concrete model, any memory access goes through address translation, but in abstract model, memory accesses operate on a virtual data store that hides a particular address translation. Other examples of non-ADT abstractions include compilation, transactions, and time-sharing. Currently, these abstractions can not be implemented by current Hoare-logic verification techniques.
In our thesis, we present an alternative approach to handling abstraction in software verification that allows us to define the abstractions not expressible in separation logic. Instead of using a single machine model and a complex logic for verification, our new software verification framework makes use of multiple machine models and common static semantics expressed in simple logic. For every module of a complex software system, our framework enables us to define a new machine model with the abstract primitives natural for that module, thereby simplifying the verification of code. These machine models are then connected to each other by abstraction relations, from which our framework generates the refinements. Using these refinements, we link the modules verified at different levels of abstraction. The final result is that though we define and specify software modules at their natural levels of abstraction, we still get the proof that all modules linked together are sound with respect to the most concrete machine model. In other words, our framework merges the techniques of abstract machines and refinement with Hoare-logic style verification.
To show that this approach is effective, we have used our framework to deal with the virtual address space abstraction. For a large portion of the OS kernel, the abstract address space model is more natural than the concrete address translation model, making it preferable to certify the kernel using address space primitives. However, the virtual memory manager, a complicated and error-prone part of the OS, relies on the address translation primitives to operate, and therefore can only be verified using the concrete model. Instead of using the address translation model to verify the entire kernel, which would make the verification more complicated, we use our framework to link the virtual memory manager and the rest of the kernel, both verified in their natural models. The verified linking guarantees that the entire kernel will execute correctly on the machine with address translation. Using Coq Proof Assistant, we have machine-checked the proofs of both the framework and the certification of address space abstraction to ensure correctness.
The work presented in the thesis raises the state-of-art in the field of formal software verification frameworks. Our framework is both entirely language independent and can handle self-modifying code without relying on separation logic. However, in our opinion, the main contribution of this work lies in modularity and reusability of certified code. Software verification tends to be all-or-nothing deal. To be reused in a different context verified modules require new specifications, and thus new proofs. Our framework enables their refinement into the new context without re-proving them. It is our hope that our work will spur the development of reusable certified libraries and creation of ever larger certified software systems.
Copyright © 1996-2017 The FLINT Group
<flint at cs dot yale dot edu>
Yale University Department of Computer Science