(SGER) Preliminary Steps Toward a Verifiable Kernel

点击翻译按钮获取中文摘要

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