- Joined
- Jun 27, 2006
- Messages
- 23,048
- Thread Author
- #1
Link Removed(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, Link Removed 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 Link Removed and the theorem prover Link Removed(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 Link Removed. 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) Link Removedsits 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. Link Removed
Niner Richard Hein's question is asked Link Removed.
Enjoy. Learn.
Link Removed
Link Removed
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 Link Removed. 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) Link Removedsits 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. Link Removed
Niner Richard Hein's question is asked Link Removed.
Enjoy. Learn.
Link Removed
Link Removed
