News

The content has been bookmarked!

There was an error bookmarking this content! Please retry.

Announcing Verve – A Type-Safe Operating System

Posted by James Vastbinder on Dec 08, 2010

Sections: Operations & Infrastructure,; Development
Topics: .NET ,; Architecture ,; Operating Systems ,; Programming ,; Verve ,; Z3 ,; Boogie ,; Singularity ,; Type Theory

Earlier this week Microsoft Research published a paper and announced the release of Verve, an operating system which grew out of the Singularity project, upon whose base premise is to use Typed Assembly Language, TAL, and Hoare logic to achieve the highest levels of security and safety. The Verve operating system consists of a nucleus, a kernel and one or more applications.

While Verve is written in C# for convenient automatic compilation to TAL, a second check is still performed to verify type safety. The Nucleus, itself, is written in assembly language which was hand-annotated with assertions. Boogie is used to verify the assembly language against a specification and guarantees safe interaction with the TAL code and hardware.

Verve successes

The first operating system mechanically verified to ensure type safety including each assembly language instruction that runs after booting which is statically verified.
Runs on commodity hardware supporting true language features such as classes, virtual methods, arrays and pre-emptive threads.
Highly efficient through the use of Bartok’s native layouts for objects, method tables and arrays.
Demonstration of automated techniques, TAL and automated theorem proving, to verify the safety of the complex low-level code in the operating system and run-time.
Demonstrates that a small amount of code verified with automated theorem proving can support an arbitrary large amount of TAL code.

Code that is verifiably type-safe accesses memory only through object references and associated features such as fields and properties. By accessing memory through well-defined paths, the runtimes or in this case, kernels can verify that code is not accessing memory locations to which it should not have access. Essentially, type safety means that a program cannot perform an operation on an object unless that operation is valid for that object. Type safety provides the most essential element for security in modern programming languages like Java & C# and when extended to the operating system level the result is efficiency which translates into performance.

Verve Limitations

Lack of support for many C# features like exception handling
Does not support the standard .NET class library due to its inclusion of unsafe code
Lacks dynamics loading of code
Runs only on a single processor
Lacks a comprehensive isolation mechanism like Singularity SIPS, Java Isolates and C# AppDomains
Verve uses verified garbage collectors that are stop-the-world and keeps interrupts disabled throughout the collection.

While Verve does have some limitations, its creators feel only multi-processor support is a significant hurdle which may require fundamental changes to its current incarnation.