Entries:
Comments:
Posts:

Loading User Information from Channel 9

Something went wrong getting user information from Channel 9

Latest Achievement:

Loading User Information from MSDN

Something went wrong getting user information from MSDN

Visual Studio Achievements

Latest Achievement:

Loading Visual Studio Achievements

Something went wrong getting the Visual Studio Achievements

Verve: A Type Safe Operating System

Download

Right click “Save as…”

 

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. 

Here's the basic idea (from the introduction of the paper):

Typed assembly language (TAL) and Hoare logic can verify the absence of many kinds of errors in low-level code. We use TAL and Hoare logic to achieve highly automated, static verification of the safety of a new operating system called Verve. Our techniques and tools mechanically verify the safety of every assembly language instruction in the operating system, run-time system, drivers, and applications (in fact, every part of the system software except the boot loader). Verve consists of a “Nucleus” that provides primitive access to hardware and memory, a kernel that builds services on top of the Nucleus, and applications that run on top of the kernel.

Here, Microsoft research scientist and operating system expert (he worked on the Singularity project) Chris Hawblitzel sits down with me to discuss the rationale behind the Verve project, the architecture and design of Verve and the Nucleus, Typed Assembly Language (TAL), potential for Verve in the real world, and much more. This is a conversational piece (no demos, no whiteboarding), but if you are into operating research and strategies for building type safe systems at the lowest levels, then this is for you. If you are interested, perhaps we could get Chris into our studio for a lecture or two on OS design. Smiley

Niner Richard Hein's question is asked here.

Get the Verve source code here.

Enjoy. Learn.

Tags:

Follow the Discussion

  • Bent Rasmussenexoteric stuck in a loop, for a while

    UACK! . My wet OS dream. Must watch...

  • @exoteric: ha!  I haven't even watched the video yet and was thinking the same thing, type-safe operating system.... booyah!

  • CharlesCharles Welcome Change

    I recommend that you read the paper and then watch this. The gory details are in the scientific literature. The goal of this conversation was to explore the thinking behind this research project. Of course, as usual, this is a conversation, not a presentation. My random questions aren't too random (I read the paper before we chatted). I like how this turned out. A little long, yes. But there are many good nuggets in this one. Hunt for them, Niners! Use your minds.

    C

  • erm didnt you say in the video that Verve was available on codeplex or did i miss-heard ?

     

    btw: is the codeplex "The Singularity project" dead ? have been no activity for a long time  Sad

  • CharlesCharles Welcome Change

    , Mr Crash wrote

    erm didnt you say in the video that Verve was available on codeplex or did i miss-heard ?

     

    btw: is the codeplex "The Singularity project" dead ? have been no activity for a long time  Sad

    You heard correctly. The Singularity Project is more than a single thing (so saying "it's" dead is somewhat meaningless...) I mean, there would be no Verve project without the Singularity research findings. In some sense, Verve is a natural, though with different specific focus (e.g., fully verifiable operating system, typed AL, managed HAL (Nucleus), etc), evolution of the Singularity project. The important point is that OS research is alive and very well both inside and outside of MS. Verve, like Singularity, is about exploring fundamentals and rethinking the OS stack. Also, as is the case with Singlularity the OS, there is no product trajectory for Verve. It's basic science, not product development...

    Here's the link to source code: http://singularity.codeplex.com/SourceControl/changeset/changes/45126

    C

     

  • @Charles:
    From: http://singularity.codeplex.com
    "Committed On: Sun May 16 2010 at 2:45 AM"

    Need i say more ?  Expressionless


    Where's the updated code ?

     

  • felix9felix9 the cat that walked by itself

    wow, its indeed an impressive project, it looks like verifiable software stack is not too far away.

    thanks Charles.

    now lets wait to see the 'C3' paper from Wolfram Schulte etc, maybe a verifiable web platform ?

  • Bent Rasmussenexoteric stuck in a loop, for a while

    Great interview, Charles. Now onto the research paper. I wonder if this has something to do with the iTALiX project, also comming out of MSR...

    http://research.microsoft.com/apps/pubs/default.aspx?id=121445

    Looks like it, same author!

  • CharlesCharles Welcome Change

    , exoteric wrote

    Great interview, Charles. Now onto the research paper. I wonder if this has something to do with the iTALiX project, also comming out of MSR...

    http://research.microsoft.com/apps/pubs/default.aspx?id=121445

    Looks like it, same author!

    Indeed. Chris and company have been working on TAL for a while now. It is certainly a very related project in this respect. For Verve, all of the code for the OS is statically verified when the system is built. The only unverified code in the system is the boot loader, which is fine in some sense because it only runs once and then is no longer executed... Even the GC is verified (I asked this question in the interview and he said it was or will be soon. At least, that's what I remember).

    It would be useful to learn more about TAL specifically. Perhaps we'll get Chris on 9 again ( E2E Smiley ) to go over the TAL stuff with a language expert..

    C

  • magicalclickmagicalclick C9 slogan, #dealwithit. WinPh8.1 IE empty tab crash and removable video control edition.

    I know I am asking redundent question. But, how likely and how soon in estimation would be seeing this in the market? I really really really hope to see this or Singularity in 5 years, but, I am also affraid MS will not take the step and waiting for competitors. I understand their marketing decisions, but, would I be able to see MS releasing Type Safed OS first in the name of practical science?

  • Bent Rasmussenexoteric stuck in a loop, for a while

    , Charles wrote

    It would be useful to learn more about TAL specifically. Perhaps we'll get Chris on 9 again ( E2E Smiley ) to go over the TAL stuff with a language expert..

    C

    It would indeed. I think we'd all love to hear more about the TAL.

  • Thanks for your time Chris. I hope you push Verve further into a real OS.

     

    Look forward to hearing more.

     

  • reidgiselreidgisel

    This is intresting.It shows that M$ spends on research.Renaissance for assembler maybee?

  • the interesting thing about this, to me, isn't even that it's an OS, its the use of Z3/boogie as a prover...this speaks directly to turings halting problem. these guys have the coolest job on the planet.

Remove this comment

Remove this thread

close

Comments Closed

Comments have been closed since this content was published more than 30 days ago, but if you'd like to continue the conversation, please create a new thread in our Forums,
or Contact Us and let us know.