Computer system reliability and robustness depends on operating system correctness. An incorrect operating system is vulnerable to random crashes or, worse, attack, where one program corrupts another program's execution. Thus, the longstanding goal of a verified operating system: one whose correctness is proved beyond doubt. Although aspects of operating systems, such as interactions with memory hardware, are currently hard for even advanced automatic verifiers, coordinated kernel interface changes and verification advances may be able to break this impasse. This exploratory research program addresses several basic issues in kernel verification. Advances are made both to the BLAST lazy predicate abstraction verification tool, and to a small, readable kernel specially designed for verification. Particular advances include specialized types and abstractions for bit-packed structures and for unbounded data structures, and transactional kernel interfaces. All tool advances will be made publicly available. This program will clear the obstructions to a more ambitious project: the construction of a fully verifiable kernel. Its success will connect the operating systems and verification communities, leading to more reliable, dependable systems and system designs.
