| Popis: |
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. |
