BT

Announcing Verve – A Type-Safe Operating System

by James Vastbinder on Dec 08, 2010 |

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. 

Hello stranger!

You need to Register an InfoQ account or or login to post comments. But there's so much more behind being registered.

Get the most out of the InfoQ experience.

Tell us what you think

Allowed html: a,b,br,blockquote,i,li,pre,u,ul,p

Email me replies to any of my messages in this thread
Community comments

Allowed html: a,b,br,blockquote,i,li,pre,u,ul,p

Email me replies to any of my messages in this thread

Allowed html: a,b,br,blockquote,i,li,pre,u,ul,p

Email me replies to any of my messages in this thread

Discuss

Educational Content

General Feedback
Bugs
Advertising
Editorial
InfoQ.com and all content copyright © 2006-2014 C4Media Inc. InfoQ.com hosted at Contegix, the best ISP we've ever worked with.
Privacy policy
BT