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.
