Linked by Thom Holwerda on Wed 8th Dec 2010 23:22 UTC, submitted by poundsmack
"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.
To read all comments associated with this story, please click here.
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.
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?
Member since:2007-08-20
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.
Features
Linked by Thom Holwerda on 05/21/13 21:38 UTC
At an event earlier today, Microsoft unveiled the next Xbox - the third model, but confusingly named Xbox One. The big focus was TV, integrated Kinect, and all the other stuff we all expected to be forced down our throats. I think it took them 25 minutes to actually come to what should be the core of the story: gaming. Nothing groundbreaking in the gaming department, except for how Microsoft intends to handle the used games market and borrowing games from friends: pay up, buddy!
Linked by Thom Holwerda on 05/20/13 11:29 UTC
The day has finally come! Jolla has finally announced the launch device for its Sailfish operating system - and by god this is a looker. It's decidedly different from other phones out there, but it has good specifications and carries a relatively reasonably price tag - EUR 399, and it's up for pre-order today, shipping in the fourth quarter of this year.
Linked by Thom Holwerda on 05/18/13 21:33 UTC
Why does Google get so much credit in the technology industry? Why, despite the company's many obvious failings, do many geeks and enthusiasts still hold a somewhat positive view on the all-knowing technology giant? A specific talk at Google I/O this week provides the answer.
Linked by David Adams on 05/16/13 4:23 UTC
OSNews is a sponsor of this year's O'Reilly OSCON in Portland, Oregon, USA. A lucky OSNews reader will win a free three-day pass, including two tutorials days. To win the pass, post a comment on this story saying something about Open Source Software or OSCON. We'll pick a winner at random next week. If you don't have an OSNews account, you may email us your entry. Part of the conference is the 9th annual Open Source Awards, and today the 16th is the deadline for nominations. If you'd like to nominate an outstanding open source contributor, do it here. Read on for more information about OSCON. Update: The 20% discount code for OSNews readers is "OSN."
Linked by Thom Holwerda on 05/11/13 21:41 UTC
"Windows is indeed slower than other operating systems in many scenarios, and the gap is worsening." That's one way to start an insider explanation of why Windows' performance isn't up to snuff. Written by someone who actually contributes code to the Windows NT kernel, the comment on Hacker News, later deleted but reposted with permission on Marc Bevand's blog, paints a very dreary picture of the state of Windows development. The root issue? Think of how Linux is developed, and you'll know the answer.
Linked by Thom Holwerda on 05/08/13 14:22 UTC
This is one of those news items that's fun to write, fun to read, fun to comment on, and where no one will be able to say anything unkind. It's all just one big ball of awesome fluffiness. TuneTracker, the BeOS radio automation software, has just released something very special: TuneTracker System 5, the first version designed entirely and specifically for Haiku. In fact, it actually includes Haiku in the software package. Better yet, TuneTracker also unveiled several system-in-a-box products - which have Haiku and TuneTracker pre-installed.
Linked by Thom Holwerda on 05/02/13 15:28 UTC
Exactly twenty years ago, a document was published that played a huge role in establishing the web as we know it today. Twenty years later, and this simple and straightforward document is proof of an irrefutable fact: while closed technologies can change markets, open technologies can change the world.
Linked by Thom Holwerda on 04/29/13 21:06 UTC
Oh multitasking. That staple of computing that got thrown out the window with many modern smartphones. We got some rudimentary thing in its place - but even as multitasking on phone and tablets improves, its user-visible side remains cumbersome. Windows 8 has a neat implementation, and now it's time Android follows in it footsteps.
Linked by Thom Holwerda on 04/24/13 22:24 UTC
They're here! Whether that excites you or not remains to be seen, but the Galaxy S4, which will most likely become the best selling Android smartphone of the year by a huge margin, has been reviewed by all the major sites, and there's lots of interesting conclusions in there - although I think most of you will get the gist.
Linked by Thom Holwerda on 04/18/13 11:21 UTC
Nokia has posted its quarterly results for the first quarter of 2013, and just like the quarters that came before, there's not a whole lot of good news in there. The rise in Lumia sales still can't even dream of making up for the sales drop in Symbian phones, and when broken down in versions, the sales figures for Windows Phone 8 Lumias in particular are very disappointing. In North America, Nokia is getting slaughtered.More Features »
Sponsored Links
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.