Linked by Thom Holwerda on Wed 8th Dec 2010 23:22 UTC, submitted by poundsmack
Microsoft "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.
Permalink for comment 452864
To read all comments associated with this story, please click here.
Real OSNews
by frytvm on Thu 9th Dec 2010 00:02 UTC
frytvm
Member since:
2009-11-11

A lot of people complain about osnews being too broad, too much a tech blog and no longer an "os site". However, projects like verve and singularity really look like the future of operating systems; so, if you care as much about OS's as you say you do, you ought to at least look at this stuff.

Moving to an os like verve would be a great step forwards in terms of security (pretty much all root-elevation kernel hacks would be gone), stability (the kernel isn't very likely to crash if its formally verified), and, to a small extent, performance (No context-switch overhead, IPC is cheaper). Of course, Verve is not a mature system, and surely integrating real 3d graphics drivers, for example, might be quite a project - but the idea and the future potential are there.

Reply Score: 2