EDN Admin
Well-known member
http://research.microsoft.com/en-us/projects/singularity/ 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, http://research.microsoft.com/pubs/122884/pldi117-yang.pdf 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 http://research.microsoft.com/en-us/projects/boogie/ Boogie and the theorem prover http://research.microsoft.com/en-us/um/redmond/projects/z3/ 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. Heres 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 http://research.microsoft.com/apps/pubs/?id=122884 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) http://research.microsoft.com/en-us/people/chrishaw/ 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. <img src=http://ecn.channel9.msdn.com/o9/content/images/emoticons/emotion-1.gif?v=c9 alt=Smiley /> Niner Richard Heins question is asked http://channel9.msdn.com/Shows/Going+Deep/Verve-A-Type-Safe-Operating-System#time=1h9m9s here . Enjoy. Learn. <img src="http://m.webtrends.com/dcs1wotjh10000w0irc493s0e_6x1g/njs.gif?dcssip=channel9.msdn.com&dcsuri=http://channel9.msdn.com/Feeds/RSS&WT.dl=0&WT.entryid=Entry:RSSView:2af56b37a9e8499c849b9e400130a16a
View the full article
View the full article