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 452924
To view parent comment, click here.
To read all comments associated with this story, please click here.
RE[4]: Real OSNews
by galvanash on Thu 9th Dec 2010 07:46 UTC in reply to "RE[3]: Real OSNews"
Member since:

certification, verification is the same. looked at solution based on certain circumstances and parameters set by persons/mechanisms which control quality

Its not the same, not how it is being used by this project. Mathematical verification means you have a proof backing your logic at every level from the bottom up. You are building a construct, starting from nothing, where every component you add is proven mathematically sound - you have to prove out the design. That of course doesn't mean that the implementation is perfect and does not contain flaws, but it does mean the model is logically perfect - there are no unknown corner cases - all possible permutations have been factored in.

tests can be incomplete. in fact in real world, they are always incomplete. there is simply no way to predict every possibility

Hence why the scope of what exactly is being verified is so limited. There IS simply no way to predict every possibility - but with a thorough understanding of how a compiler/runtime/jit generates code you can with absolutely certainty identify code which performs certain unsafe operations. That is verification.

Certification is a form of insurance based on reputability, verification is a form of insurance based on mathematical certainties.

Reply Parent Score: 2

RE[5]: Real OSNews
by somebody on Thu 9th Dec 2010 08:23 in reply to "RE[4]: Real OSNews"
somebody Member since:

not to be nitpicking;)

one part of your answer excludes other.

Reply Parent Score: 3

RE[6]: Real OSNews
by galvanash on Thu 9th Dec 2010 10:14 in reply to "RE[5]: Real OSNews"
galvanash Member since:

I don't really know what you mean by that... Maybe Im not being clear. The verification software is mathematically proven. Again, that doesn't mean it has no bugs, but it is logically consistent and all permutations of input have been factored into its design. It is not possible to give it input that produces an unknown output.

The software it is verifying on the other hand is not. The verification software can be given a block of code, and based on the assumption that the code is annotated correctly - it can with absolutely certainty make certain claims about it, one such claim for example being "this block of code does not cast an int to a pointer".

That doesn't mean that the code being tested is bug free, but it DOES mean that it does not cast an int to a pointer. There is absolutely no way it could do that, because the verification software has been mathematically proven to catch any input that would represent a cast of an int to a pointer.

Sure, the verifier could have a bug in it, you still have to do due diligence. But the point is very few software products are proven out this way - this is a way to apply the benefits of proven code to other code - and it doesn't require a runtime to do so (like for example the way .NET does it).

Edited 2010-12-09 10:32 UTC

Reply Parent Score: 2