High-level computer applications build on services provided by lower-level software layers, such as operating systems and language run-time systems. These lower-level software layers should be reliable and secure. Without reliability, users endure frustration and potential data loss when the system software crashes. Without security, users are vulnerable to attacks from the network, which often exploit low-level bugs such as buffer overflows to take over a user™s computer. Unfortunately, today™s low-level software still suffers from a steady stream of bugs, often leaving computers vulnerable to attack until the bugs are patched.
Many projects have proposed using safe languages to increase the reliability and security of low-level systems. Safe languages ensure type safety and memory safety: accesses to data are guaranteed to be well-typed and guaranteed not to overflow memory boundaries or dereference dangling pointers. This safety rules out many common bugs, such as buffer overflow vulnerabilities. Unfortunately, even if a language is safe, implementations of the language™s underlying run-time system might have bugs that undermine the safety. For example, such bugs have left web browsers
open to attack.
This paper presents Verve, an operating system and run-time system that we have verified to ensure type and memory safety. Verve has a simple mantra: every assembly language instruction in the software stack must be mechanically verified for safety. This includes every instruction of every piece of software except the boot loader: applications, device drivers, thread scheduler, interrupt handler, allocator, garbage collector, etc.
The goal of formally verifying low-level OS and run-time system code is not new. Nevertheless, very little mechanically verified low-level OS and run-time system code exists, and that code still requires man-years of effort to verify.
Source: Microsoft research
