(SGER) Preliminary Steps Toward a Verifiable Kernel

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

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.