Verve: A Type Safe Operating System by Microsoft Research

MSR released a paper covering an operating system research project that takes a new approach to building an OS stack with verifiable and type safe managed code. This project employs a novel use of Typed Assembly Language, which's what you think it's: Assembly with types (implemented as annotations and verified statically using verification technology Boogie […]

MSR released a paper covering an operating system research project that takes a new approach to building an OS stack with verifiable and type safe managed code. This project employs a novel use of Typed Assembly Language, which's what you think it's: Assembly with types (implemented as annotations and verified statically using verification technology Boogie and theorem prover Z3 (Boogie generates verification conditions that're then statically proven by Z3.

"We use TAL and Hoare logic to achieve highly automated, static verification of the safety of a new operating system called "Verve." Our techniques and tools mechanically verify the safety of every assembly language instruction in the operating system, run-time system, drivers, and apps (in fact, every part of the system software except the boot loader). Verve consists of a "Nucleus" that provides primitive access to hardware and memory, a kernel that builds services on top of the Nucleus, and apps that run on top of the kernel."