Verve: A Type Safe Operating System

The Singularity project (an OS written in managed code used for research purposes) has provided several very useful research results and opened new avenues for exploration in operating system design. Recently, MSR released a paper covering an operating system research project that takes a new approach to building an OS stack with verifiable and type safe managed code. This project employs a novel use of Typed Assembly Language, which is what you think it is: Assembly with types (implemented as annotations and verified statically using the verification technology Boogie and the theorem prover Z3 (Boogie generates verification conditions that are then statically proven by Z3. Boogie is also a language used to build program verifiers for other languages)). As with Singularity, the C# Bartok compiler is used, but this time it generates TAL. The entire OS stack is verifiably type safe (the Nucleus is essentially the Verve HAL) and all objects are garbage collected. It does not employ the SIP model of process isolation (like Singularity). In this case, again, the entire operating system is type safe and statically proven as such using world-class theorem provers.” Channel9 has an interview on video with one of the developers behind this MSR project. Source code to Verve is available.

17 Comments

  1. 2010-12-09 12:02 am
    • 2010-12-09 12:42 am
    • 2010-12-09 3:21 am
      • 2010-12-09 4:34 am
      • 2010-12-09 5:59 am
        • 2010-12-09 6:25 am
          • 2010-12-09 7:16 am
          • 2010-12-09 7:50 am
        • 2010-12-09 7:05 am
          • 2010-12-09 7:28 am
          • 2010-12-09 7:46 am
          • 2010-12-09 8:23 am
          • 2010-12-09 10:14 am
          • 2010-12-10 3:29 am
          • 2010-12-10 11:37 pm
          • 2010-12-09 3:08 pm
          • 2010-12-09 8:26 pm