(SGER) Preliminary Steps Toward a Verifiable Kernel

计算机系统的可靠性和健壮性取决于操作系统的正确性. 一个不正确的操作系统很容易受到随机崩溃，或者更糟的攻击，一个程序破坏另一个程序的执行。因此，一个经过验证的操作系统的长期目标是：一个毫无疑问的正确性被证明。 尽管操作系统的某些方面，比如与内存硬件的交互，目前甚至对高级自动验证器来说都很困难，但协调的内核接口变化和验证进展可能能够打破这一僵局。 这一探索性研究计划解决了内核验证中的几个基本问题。在BLAST惰性谓词抽象验证工具和专门为验证设计的小型可读内核方面都取得了进展。特别的进展包括位封装结构和无界数据结构的专用类型和抽象以及transactionalkernel接口。 所有工具的进步都将被公开。这个计划将为一个更雄心勃勃的项目扫清障碍：构建一个完全可验证的内核。 它的成功将连接操作系统和验证社区，导致更可靠，更可靠的系统和系统设计。

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.