Verve - New non-Windows OS from Microsoft

Verve is the latest non-Windows operating system for which Microsoft has shared details with the world via the “Safe to the Last Instruction: Automated Verification of a Type-Safe Operating System” whitepaper.

Still just a prototype from Microsoft Research, Verve is designed as an operating system and run-time system that the software giant has focused on ensuring that both type and memory are secure.

According to the Redmond company, Verve is a spin-off of another non-Windows operating system that users might already be familiar with: Singularity.

The Singularity platform project, an OS written in managed code used for research purposes, has inspired new platforms such as Verve, and also Midori, on which there are very little details available.

“Typed assembly language (TAL) and Hoare logic can verify the absence of many kinds of errors in low-level code. 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 applications (in fact, every part of the system software except the boot loader),” reads an excerpt from the whitepaper accompanying the OS.

Microsoft reveals that overall OS security is ensured by mechanically verifying every assembly language instruction in the software stack for safety.

Essentially, all instructions of all software running on top of the platform are checked.

“Verve consists of a “Nucleus” that provides primitive access to hardware and memory, a kernel that builds services on top of the Nucleus, and applications that run on top of the kernel.

“The Nucleus, written in verified assembly language, implements allocation, garbage collection, multiple stacks, interrupt handling, and device access. The kernel, written in C# and compiled to TAL, builds higher-level services, such as preemptive threads, on top of the Nucleus.

“A TAL checker verifies the safety of the kernel and applications. A Hoare-style verifier with an automated theorem prover verifies both the safety and correctness of the Nucleus,” the company noted.

Microsoft reveals that Verve is the first operating system to sport mechanical verification for both type and memory safety.