BT

Your opinion matters! Please fill in the InfoQ Survey!

Announcing Verve – A Type-Safe Operating System

| by James Vastbinder  Followers on Dec 08, 2010. Estimated reading time: 2 minutes |

A note to our readers: As per your request we have developed a set of features that allow you to reduce the noise, while not losing sight of anything that is important. Get email and web notifications by choosing the topics you are interested in.

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. 

Rate this Article

Adoption Stage
Style

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

Login to InfoQ to interact with what matters most to you.


Recover your password...

Follow

Follow your favorite topics and editors

Quick overview of most important highlights in the industry and on the site.

Like

More signal, less noise

Build your own feed by choosing topics you want to read about and editors you want to hear from.

Notifications

Stay up-to-date

Set up your notifications and don't miss out on content that matters to you

BT