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.
Thread beginning with 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

RE: Real OSNews
by zlynx on Thu 9th Dec 2010 00:42 in reply to "Real OSNews"
zlynx Member since:
2005-07-20

The kernel may not crash, but it also may not do what is expected.

Because of course the software runs into the problem of Who Verifies The Verification Rules?

Also I just thought of many ways a fully verified kernel can still crash: all sorts of hardware interaction.

Say a driver orders a device to DMA network packets into a RAM block but somehow frees that RAM block before shutting down the DMA engine, then that block gets reused for a loadable driver code, then WHAM kernel crash when another network packet gets received.

Reply Parent Score: 2

RE: Real OSNews
by somebody on Thu 9th Dec 2010 03:21 in reply to "Real OSNews"
somebody Member since:
2005-07-07

like first, i'm not bashing this project. i'm bashing pipe dream about perfect world they want to show.

since when did verification mean anything? especially in commercial waters? you have ms verified drivers and they usually work worse then non verified. you have all sorts of verifications elsewhere, and to what account? for pr bogus that helps them sell more

unfortunately, coders don't really decide on their product. management and pr does. which often leads to going out with completely bogus half assed project.

i think i'm going to live to have meaningful conversation with gingerbread people long before i see something like completely secure and trustworthy.

and like the other poster said... who polices the police?

Reply Parent Score: 1

RE[2]: Real OSNews
by Morph on Thu 9th Dec 2010 04:34 in reply to "RE: Real OSNews"
Morph Member since:
2007-08-20

you have ms verified drivers and they usually work worse then non verified

I think you've confused 'verified' with 'certified'.

Reply Parent Score: 3

RE[2]: Real OSNews
by galvanash on Thu 9th Dec 2010 05:59 in reply to "RE: Real OSNews"
galvanash Member since:
2006-01-25

since when did verification mean anything? especially in commercial waters? you have ms verified drivers and they usually work worse then non verified.


You are mixing your terms. Microsoft "certifies" drivers, meaning nothing more than "trust us, it works - cause we looked at it... and were Microsoft". "Verified", as it is used by the developers on this project, means it has passed a specific set of rigid mathematically proven tests for type safety that guarantees the code in question does not do certain explicitly defined "bad" things. It does not mean the code is perfect and does not contain bugs, but it does mean it does not perform certain unsafe operations. Verified != bug free.

and like the other poster said... who polices the police?


The point is not to "police" anything. You are taking what amounts to a very interesting but currently unrealistic experiment, and trying to project it's affect on your world view of whats wrong with software development... that ain't the point.

Verification at this level is simply a tool. It is very useful because it acts as insurance against human error (assuming the fundamentals of the type checking are sound). It is also highly specialized and not applicable to any "normal" software development practice currently in use - they had to essentially build their own little software development ecosystem in order to test it...

The point is if you can build something that can type check code at the assembly level, and you can build a runtime/compiler/jit that can reliably annotate the assembly code it generates with type annotations for such a tool to work with, you can then build verification tools that can determine with a great deal of accuracy if said code is doing something wonky you don't want it doing. Thats it. Its useful, but it is no panacea.

On a side note... I often get the general impression that a lot of programmers get all riled up about all this "new age" stuff from Channel9 and lash out against it simply because it is Microsoft backing it. Watch the video. If you are a programmer and can't relate to the guy being interviewed please turn in your geek card - the guy is obviously intelligent, motivated, and cares about what he is doing. I couldn't care less what company he is working for, and I don't think he cares much either. He is in it for the work - this is what research is supposed to be and I applaud Microsoft for funding it.

Reply Parent Score: 4