Formal verification is the only known way of building bug-free or hacker-proof programs. However, due to its prohibitive associated costs, formal verification has rarely been considered as an option in building robust large-scale system software. Practical system software normally consists of highly correlated interdependent subsystems, with complex invariants that need to be globally maintained. To reason about the correctness of a program, we not only need to show that the program in consideration satisfies the invariants and the specification, but also prove that the invariants cannot be accidentally broken by other parts of the system, e.g., via pointer manipulation. Furthermore, we often have some snippet of code that temporarily breaks the invariants, and re-establishes them later, which could make reasoning of such code more complex. Even worse, many complex system software contains device drivers to work with the devices, which brings a major challenge of handling device interrupts; and consists of multiple threads running on multiple CPUs concurrently. This forces us to further reason about arbitrary interactions and interleaved executions among different devices, interrupts, and programs running on different CPUs, which could quickly make the verification task intractable.
In this dissertation, we present a compositional, and powerful automation engine for effectively verifying complex system software. It is compositional because it solely focuses on providing strong automation support for verifying functional correctness properties of C source programs, while taking the memory isolation and invariant properties as given, and separately provide a systematic approach for guaranteeing the isolation among different in-memory data, and proving invariants, completely at the logical level. The engine also contains a novel way of representing devices and drivers, and simulation-based approach for turning the low-level interrupt model into an equivalent abstract model which is suitable for reasoning about interruptible code. Furthermore, the engine provides a new way of representing concurrently shared states into a sequence of external UO events and allows us to verify concurrent programs as if they were sequential and provided a separate logical framework to effectively reason about interleaved executions. This very modular design allows us to be able to reason about each aspect of the system separately, and while each of the reasoning tasks looks unbelievably simple, we could combine all the proofs to obtain proofs of properties about complex system software. An OS kernel is a typical example of complex low-level system software with highly interdependent modules. To illustrate the effectiveness of our approach, using all the tools, we have developed a fully verified feature-rich operating system kernel with machine-checkable proof in the Coq proof assistant.
|School Location:||United States -- Connecticut|
|Source:||DAI-B 80/07(E), Dissertation Abstracts International|
|Keywords:||Abstraction Layer, Certified OS Kernels, Concurrency, Device Drivers, Modularity, Verification|
Copyright in each Dissertation and Thesis is retained by the author. All Rights Reserved
The supplemental file or files you are about to download were provided to ProQuest by the author as part of a
dissertation or thesis. The supplemental files are provided "AS IS" without warranty. ProQuest is not responsible for the
content, format or impact on the supplemental file(s) on our system. in some cases, the file type may be unknown or
may be a .exe file. We recommend caution as you open such files.
Copyright of the original materials contained in the supplemental file is retained by the author and your access to the
supplemental files is subject to the ProQuest Terms and Conditions of use.
Depending on the size of the file(s) you are downloading, the system may take some time to download them. Please be