CSR-AES: Runtime Monitoring and Model Checking for High-Confidence System Software

System software, such as operating system (OS) kernels and middleware for distributed systems, is quite difficult to develop and maintain because it is: (1) asynchronous and event-driven in nature; (2) often written in the type-unsafe C programming language; and (3) complicated by numerous data structures, caches, locks, and reference counts, all intended to improve performance. System software also provides the critical infrastructure on which all other applications must run, and should therefore elicit a sense of high confidence from its developers and users. Static analysis techniques have matured to the point where they can catch a number of misuse errors (e.g., incorrect usage of an API), and model checking has proven effective in catching more insidious data-dependent bugs. The goal of this project is to develop advanced model-checking techniques, coupled with OS code instrumentation, to achieve always-on monitoring of system software. The proposed effort will result in the development of compiler and model-checking tools that allow formal modeling and verification to be applied to complex software packages. Embedded in the tools will be heuristics to quantify confidence levels for software components, and methods to balance confidence levels with the intensity of runtime checking. Techniques will be developed to explore models and produce actual test cases from CCMs, possibly feeding results back into model updates, until an equilibrium is reached. Finally, the formal verification of an embedded Linux kernel, which is used in numerous critical systems around the world, will be conducted.