Beta
×

Welcome to the Slashdot Beta site -- learn more here. Use the link in the footer or click here to return to the Classic version of Slashdot.

Thank you!

Before you choose to head back to the Classic look of the site, we'd appreciate it if you share your thoughts on the Beta; your feedback is what drives our ongoing development.

Beta is different and we value you taking the time to try it out. Please take a look at the changes we've made in Beta and  learn more about it. Thanks for reading, and for making the site better!

World's First Formally-Proven OS Kernel

Soulskill posted more than 5 years ago | from the wait-for-it dept.

Operating Systems 517

An anonymous reader writes "Operating systems usually have bugs — the 'blue screen of death,' the Amiga Hand, and so forth are known by almost everyone. NICTA's team of researchers has managed to prove that a particular OS kernel is guaranteed to meet its specification. It is fully, formally verified, and as such it exceeds the Common Criteria's highest level of assurance. The researchers used an executable specification written in Haskell, C code that mapped to Haskell, and the Isabelle theorem prover to generate a machine-checked proof that the C code in the kernel matches the executable and the formal specification of the system." Does it run Linux? "We're pleased to say that it does. Presently, we have a para-virtualized version of Linux running on top of the (unverified) x86 port of seL4. There are plans to port Linux to the verified ARM version of seL4 as well." Further technical details are available from NICTA's website.

cancel ×

517 comments

Sorry! There are no comments related to the filter you selected.

spec? (5, Insightful)

polar red (215081) | more than 5 years ago | (#29049945)

but is the spec useable ? bugfree ?

Re:spec? (-1, Troll)

Anonymous Coward | more than 5 years ago | (#29049983)

The spec is written in C, a Linux language, and as such is inherently untrustworthy. This becomes the weak point in the chain, from which the rest of their theory collapses; the fact that Isabelle can prove a faulty system secure by way of a faulty spec shows nothing. Also, the fact that they are using a functional language like Haskell is pure smoke and mirrors.

Re:spec? (-1, Offtopic)

Anonymous Coward | more than 5 years ago | (#29050085)

I have nothing against gay people and I am sure some of them need to have computers like normal people. What they do behind closed door is their own business, whether that be taking a penis up the anus or using their Linux based PC to access online gay communities like Craigslist, Myspace and Facebook to meet and keep in touch with other homosexuals.

Re:spec? (0)

Anonymous Coward | more than 5 years ago | (#29050119)

Someone take away this person's keyboard and internet connection please!

Re:spec? (0)

Anonymous Coward | more than 5 years ago | (#29050185)

Also, the fact that they are using a functional language like Haskell is pure smoke and mirrors.

In java, we all agree - form before function.

Re:spec? (1)

maxwell demon (590494) | more than 5 years ago | (#29050239)

form before function.

That's why you first write it in a formal language, then in a functional language.

Re:spec? (1)

hesiod (111176) | more than 5 years ago | (#29050421)

first write it in a formal language, then in a functional language.M

I don't believe Java fits either of those.

Re:spec? (0)

mkeeler (1611713) | more than 5 years ago | (#29050333)

Why is C a linux language. Most operating systems are all written using C except maybe vista which would account for why it is such a slow piece of crap.

Re:spec? (1)

IamTheRealMike (537420) | more than 5 years ago | (#29050149)

Is the hardware itself bug free?!

Re:spec? (2)

VoidCrow (836595) | more than 5 years ago | (#29050207)

Perhaps not currently but, given the work on high level hardware compilation languages, it's only a matter of time before similar techniques are applied to hardware design.

How's that warrantless wiretapping program going? (-1, Offtopic)

Anonymous Coward | more than 5 years ago | (#29050177)

What's that you say? Not only is it still around, but after a bunch of phony posturing for the media the Democrats all voted in favor of continuing it? LOLOLOLOLOLOLOLOLOL!!!!!!!!

Re:spec? (0)

Anonymous Coward | more than 5 years ago | (#29050195)

no. another theorem tells that you can never verify that a code is bug free (it may be bug free, but you cannot prove it)

Re:spec? (4, Insightful)

jadrian (1150317) | more than 5 years ago | (#29050277)

To verify the software meets its specification the specification itself must formalised in the theorem prover. This in turn gives you the possibility of proving properties of the spec itself.

Re:spec? (5, Informative)

JasterBobaMereel (1102861) | more than 5 years ago | (#29050349)

It only means it meets the spec, not that the spec is correct ...

It does not mean that the faulty or erratic hardware cannot crash the system

It does not mean that other programs cannot crash and lose your data ...

It does not mean that buggy device drivers can make your system unusable

It does not mean that the system is perfect, only that it will always do what it is supposed to ... which may not be what you want ...

Re:spec? (1)

Pascal Sartoretti (454385) | more than 5 years ago | (#29050439)

but is the spec useable ? bugfree ?

And does it match the user or system needs ? And how easily can it be modified to cover new needs ?

first post hopefully (0)

Anonymous Coward | more than 5 years ago | (#29049953)

first please

Thank goodness (1, Insightful)

2.7182 (819680) | more than 5 years ago | (#29049961)

People are starting to see the value of this. Also of programming in logic based languages like Haskell, ML etc.

Re:Thank goodness (2, Insightful)

morgan_greywolf (835522) | more than 5 years ago | (#29050055)

As opposed to programming languages that aren't logic-based? What separates Haskell, Ocaml, Lisp, Scheme, etc. from others is that they are functional programming languages, as opposed to imperative-based languages like C.

Both use logic, just in different ways.

Re:Thank goodness (3, Insightful)

johannesg (664142) | more than 5 years ago | (#29050071)

People are starting to see the value of this. Also of programming in logic based languages like Haskell, ML etc.

People have seen the value of this since the first days of programming. In fact, the value is so enormous that no one can afford it... And they have just finished proving that first few lines of code they wrote. In another five decades they hope to be able to have Notepad proven and ready to run so you can actually get some work done!

Re:Thank goodness (0)

mrjb (547783) | more than 5 years ago | (#29050191)

In fact, the value is so enormous that no one can afford it...

If you're a techie, you should use be more accurate in your use of language. Substituting the word 'price' for 'value' is something you should only do in sleazy sales pitches.

Re:Thank goodness (0, Flamebait)

Desler (1608317) | more than 5 years ago | (#29050223)

Also of programming in logic based languages like Haskell, ML etc.

Since when was C not based in logic? Do you even know what the hell you're talking about?

Yeah right (0)

Anonymous Coward | more than 5 years ago | (#29049979)

Major bug found in 3...2...

Re:Yeah right (5, Funny)

oji-sama (1151023) | more than 5 years ago | (#29050001)

It's not a bug, it's a formally proved feature ^.^

Amiga Hand? (4, Informative)

ArcadeNut (85398) | more than 5 years ago | (#29049981)

Or do you mean the "Guru Meditation Error"?

Re:Amiga Hand? (0)

Anonymous Coward | more than 5 years ago | (#29050323)

Ah you beat me to this. The submitter only seems to know a little about the Amiga. What I think he is referring to is the Floppy Boot Screen, which you get if you don't have a hard drive. It has a hand holding a floppy and a number like 1.0, 1.1, 1.2 or 1.3. It later got replaced by an other floppy boot screen for higher kickstart roms.

The Amiga Hand? (5, Interesting)

johannesg (664142) | more than 5 years ago | (#29049995)

The Amiga Hand was the boot screen, not an error screen. You're thinking of the famous Guru Meditation.

Besides, who says that the Amiga kernel did _not_ meet the specifications? Have you read them? Does it mention "crash free" anywhere?

The Haskell code is called a "specfication", but if it is Haskell code, surely it should count as a _program_ already? How can you prove that that program is bug-free? How about conceptual bugs?

Was the toolchain verified? How about the hardware on which it runs?

What overhead does this approach have? Are the benefits worth it?

I'm not saying this is all bullshit, but it looks like me that they are pointing to one program, calling it a "specification", and then demonstrating machine translation / verification to a similar program. I'm not sure if I buy that methodology.

Re:The Amiga Hand? (3, Interesting)

TheCycoONE (913189) | more than 5 years ago | (#29050083)

Well the typical bugs that affect C programs, like buffer overflows, using a dereferenced pointer, etc; along with common mistakes made in procedural programming in general like off-by-one errors are much less likely to come up in a functional language like Haskel. In a lot of cases Haskel code is simply a LOT shorter and easier to read than it's C/C++ counterpart which makes it much easier to find a problem; not much harder than finding the problem in a spec on paper.

So, no I don't think it guarantees anything, but it's a lot better than C code on its own.

Re:The Amiga Hand? (5, Informative)

Anonymous Coward | more than 5 years ago | (#29050217)

The missing word is formal.

They use a formal specification [wikipedia.org] , which is then formally verified [wikipedia.org] .

The overhead? It took something like 5 years for a 10,000 line program. The benefit is if the specification is right, the program should be right.

Other questions are answered in the FAQ linked in the summary and this page [nicta.com.au] .

And if the spec has bugs the program will have bug (1)

Viol8 (599362) | more than 5 years ago | (#29050493)

So who gets to prove the spec then?

Re:The Amiga Hand? (4, Interesting)

Tom (822) | more than 5 years ago | (#29050321)

How can you prove that that program is bug-free? How about conceptual bugs?

Formal verification does not tackle conceptual bugs. What it does is prove that the implementation conforms to the specification. If your specification is false, then it is false, but the implementation will correctly implement the false behaviour. In other words, this checks whether the house and the building plan are identical. If the plan has a window where there shouldn't be one, then that window will be there, because it's on the plan.

What overhead does this approach have? Are the benefits worth it?

RTFA. The amount of work required is staggering (four years, 200,000 theorems to prove) but since it's a verification of code, not additional testing code, there is zero overhead when the system is running.

All this talk about Amiga? (0)

Anonymous Coward | more than 5 years ago | (#29050445)

I was born in 1989, you insensitive clod.

Re:The Amiga Hand? (-1, Troll)

Dog-Cow (21281) | more than 5 years ago | (#29050455)

Obviously the mods didn't read the article either, or you would have been modded redundant. Or simply stupid.

Karlan Mitchell (0)

Anonymous Coward | more than 5 years ago | (#29049997)

Yet another abstraction layer, just what we need......pssha bullocks

Give me six lines of code... (4, Funny)

Joce640k (829181) | more than 5 years ago | (#29050015)

"If you give me six lines of code written by the most diligent of programmers, I will surely find enough in them to crash the OS" - Cardinal Ritchielieu

Re:Give me six lines of code... (5, Funny)

Telecommando (513768) | more than 5 years ago | (#29050067)

Every program contains at least one bug, and can be shortened by at least
one instruction. By induction, every program can be reduced to a single
instruction which doesn't work. /old, I know.

Re:Give me six lines of code... (4, Funny)

ranulf (182665) | more than 5 years ago | (#29050211)

> By induction, every program can be reduced to a single instruction which doesn't work.

HACF?

And that instruction is... (1)

camperdave (969942) | more than 5 years ago | (#29050229)

Every program contains at least one bug, and can be shortened by at least one instruction. By induction, every program can be reduced to a single instruction which doesn't work.

And that instruction is...

HCF [wikipedia.org] .

Re:Give me six lines of code... (1)

Tenebrousedge (1226584) | more than 5 years ago | (#29050143)

Excellent line, but I don't think it really holds up. Certainly a literal reading could be a nontrivial problem, perhaps impossible, but even just assuming the general idea that app-level code can always be used to crash the underlying OS seems fraught with troubles.

Re:Give me six lines of code... (5, Funny)

Anonymous Coward | more than 5 years ago | (#29050459)

/*
  *
  *
  *
  *
  */

The amiga hand? (0)

Anonymous Coward | more than 5 years ago | (#29050019)

The "Amiga hand" is the Amiga bootscreen. Whoever wrote this probably meant "Guru Meditation".

Isn't being older than 14 (or knowing how to use wikipedia) required to be a slashdot editor?

Re:The amiga hand? (1)

cdrom600 (981598) | more than 5 years ago | (#29050129)

The "Amiga hand" is the Amiga bootscreen. Whoever wrote this probably meant "Guru Meditation".

Isn't being older than 14 (or knowing how to use wikipedia) required to be a slashdot editor?

You must be new here.

Re:The amiga hand? (0)

Anonymous Coward | more than 5 years ago | (#29050201)

Isn't being older than 14 (or knowing how to use wikipedia) required to be a slashdot editor?

You don't even have to know anything about computers to be an editor [wikipedia.org] . CmdrTaco just takes any warm body that can hen peck at a keyboard enough to post a submission.

Re:The amiga hand? (1)

daveime (1253762) | more than 5 years ago | (#29050281)

CmdrTaco just takes any warm body that can hit CTRL-C and CTRL-V in quick succession. FTFY.

CmdrTaco just takes any warm body. FTFYA.

Apps running on top will crash... so (3, Insightful)

WiseOwl2001 (742135) | more than 5 years ago | (#29050021)

Even if we have a perfect kernel, it won't insulate us from bugs in the software running on top of that kernel, so do we really gain much? I guess for mission critical apps the answer could be yes... But for every-day computing?? On my desktop I have more trouble with Firefox crashing than I do the OS! (Yes I run linux).

Re:Apps running on top will crash... so (5, Informative)

John Hasler (414242) | more than 5 years ago | (#29050057)

> Even if we have a perfect kernel, it won't insulate us from bugs in the
> software running on top of that kernel, so do we really gain much?

Since a kernel crash kills all your applications and background processes, kills your network connection, requires you to reboot, and can scribble anywhere on the disk, yes.

Re:Apps running on top will crash... so (2, Informative)

Fri13 (963421) | more than 5 years ago | (#29050189)

Well, kernel bug brings down whole OS and all the applications running top of it. But the kernel is usually most secure and stable. Most errors comes from drivers.

http://www.usenix.org/publications/login/2006-04/openpdfs/herder.pdf [usenix.org]

And that is the problem with the monolithic OS's. One bug in the driver or any other part of the OS, brings it down. But even it is about monolithic OS, it can be as secure as microkernel-based OS's like Hurd, Minix or NT.

And I believe that the star of the next 10 years will come to be the MS Singularity.

Re:Apps running on top will crash... so (1)

PybusJ (30549) | more than 5 years ago | (#29050139)

It's the other way round. Once you've formally proven things you care about for your application (security, correctness, whatever), and people are doing this though much less than they might. What do you run it on to maintain your guarantees, if there is no formally proven kernel?

So far the current answer seems to be you compile your code down to bare metal and run as an embedded app without an OS, but that only gets you so far. Mind you I can't see a fully fledged web browser based on formal methods coming along any time soon.

Re:Apps running on top will crash... so (4, Insightful)

Tom (822) | more than 5 years ago | (#29050365)

Yes, it gains you a lot.

Firefox crashing means your userland memory is fucked up and can't be trusted anymore. No problem, kill it, clean it and restart the application.

A kernel crash leads to undefined behaviour on the ring 0 level. You don't want that, it's where root exploits live.

Furthermore, we have a lot of really, really strong kernel-level security extensions, like SELinux, whose only two vulnerable spots are kernel-level exploits and weak security policies. If you can remove one of them, you've done a lot to improve security.

Re:Apps running on top will crash... so (1)

Arlet (29997) | more than 5 years ago | (#29050491)

Firefox crashing means your userland memory is fucked up and can't be trusted anymore. No problem, kill it, clean it and restart the application.

If your filesystem task running on top of a proven kernel has a bug, it can still corrupt your disk.

Knuth on proven correct: (5, Insightful)

John Hasler (414242) | more than 5 years ago | (#29050027)

"Beware of bugs in the above code. I have only proven it correct, not tested it."

Who proved the proof-checker? (3, Funny)

Dr. Manhattan (29720) | more than 5 years ago | (#29050137)

Recursion (n): see recursion.

Re:Who proved the proof-checker? (0)

Anonymous Coward | more than 5 years ago | (#29050317)

> Who proved the proof-checker?

You just run the proof-checker on itself, of course!

It's turtles all the way down.

(Disclaimer: Only for some definitions of "down." Certain exclusions may apply. See store for details.)

riight (1)

jointm1k (591234) | more than 5 years ago | (#29050043)

World's First Formally-Proven OS Kernel

Beware of bugs in the above code; I have only proved it correct, not tried it.
--Donald Knuth

Empty promises... (1, Insightful)

Anonymous Coward | more than 5 years ago | (#29050053)

You can't assure we'd never see a kernel fault again even using this. Most faults on most platforms are caused by hardware faults that even a formally proven OS cannot prevent. They also claim that something entirely on spec' has no bugs, which of course is laughable to anyone that has done any length of development. You just cannot account for everything that could happen within a complex system with maybe thousands of independant components.

Further more they claim in the article that software faults have caused plane crashes, when? Off the top of my head I cannot name a single instance when a software fault caused a plane crash (and yes, that includes the recent Air France crash).

Re:Empty promises... (5, Insightful)

ezzzD55J (697465) | more than 5 years ago | (#29050453)

Most faults on most platforms are caused by hardware faults

bullshit.

Provable? (1, Interesting)

tedgyz (515156) | more than 5 years ago | (#29050065)

I thought any sufficiently complex system was impossible to prove correct.

Re:Provable? (1)

Prof.Phreak (584152) | more than 5 years ago | (#29050219)

Well, one thing you can do is cut and paste your code into the specification. Now your code perfectly matches the specification---and is coded as specified.

They seem to be doing the same thing, except going about it some backwards way.

Re:Provable? (1)

mwvdlee (775178) | more than 5 years ago | (#29050429)

Well, one thing you can do is cut and paste your code into the specification. Now your code perfectly matches the specification---and is coded as specified.

That would be doing it backwards...

They seem to be doing the same thing, except going about it some backwards way.

...and doing a backwards thing backwards would be the right way again.

Re:Provable? (5, Insightful)

jamesh (87723) | more than 5 years ago | (#29050225)

I thought any sufficiently complex system was impossible to prove correct.

Then obviously this OS is not sufficiently complex.

Re:Provable? (2, Informative)

bramez (190835) | more than 5 years ago | (#29050367)

only if you want to prove it automatically. this proof is constructed by hand, with some automatical steps in between, and then *verified* automatically. to manage the complexity of the proof, the proof is done in a more abstract formal specification language , then refined two times (haskel, C) . the correctness of the refinements are formally proven by the Isabelle system.

Godel's Incompleteness Theorem? (1, Interesting)

wisebabo (638845) | more than 5 years ago | (#29050073)

As a once (very long ago!) C.S. major, I'm curious to know how they got around Godel's Incompleteness Theorem. While their system is certainly not "complete" if someone can explain (in advanced layman's terms!) what they left out and how that allowed them to formally prove the correctness of their kernel, it would be much appreciated. (Is it because, as an AC wrote, the spec was written in C? Does this "hide" the parts which are unprovable?)

Re:Godel's Incompleteness Theorem? (1)

achten (1032738) | more than 5 years ago | (#29050161)

They are not trying to prove theorems written within the specified system. Hence not constrained by GIT.

Re:Godel's Incompleteness Theorem? (0)

Anonymous Coward | more than 5 years ago | (#29050165)

What is there to get around? GÃdel says that not every true statement is provable. They have not proven every true statement. Just one, that their kernel is correct.

Re:Godel's Incompleteness Theorem? (1)

maxwell demon (590494) | more than 5 years ago | (#29050309)

What is there to get around? GÃfdel says that not every true statement is provable. They have not proven every true statement. Just one, that their kernel is correct.

No. They didn't prove that their kernel is correct. Just that their C code and their formalization of the specification share the same set of bugs.

Re:Godel's Incompleteness Theorem? (4, Insightful)

TheSunborn (68004) | more than 5 years ago | (#29050205)

Godel's Incompleteness Theorem just say(In this context) that there exists infinite many kernels that are correct but which can not be proven correct. It does not say that no kernel can be proven correct.

So they just happen to write one of the kernels that could be proven.

Re:Godel's Incompleteness Theorem? (1)

Desler (1608317) | more than 5 years ago | (#29050251)

Except that the only "proved" that their Haskell specification was correct, not the C translation.

Hm I thought they proved the mapping (1)

Nicolas MONNET (4727) | more than 5 years ago | (#29050319)

Hm I thought they proved the mapping from Haskell to C was correct, as well. At lest, so far, for the ARM version.

Re:Godel's Incompleteness Theorem? (0)

Anonymous Coward | more than 5 years ago | (#29050249)

I don't mean to be pedantic, but the Godel Incompleteness Theorem(s) apply to formal axiomatic systems of a certain minimal complexity (sufficient for elementary arithmetic, in the case of the first theorem; sufficient for elementary arithmetic, plus some metalogical notions like provability, in the case of the second), not computers. Given this, the Incompleteness Theorems only have implications for the theory of computation via the Church-Turning thesis, which states that any computable function is equivalent to a general recursive function (hence the connection to elementary arithmetic), and anything which can be done via a general recursive function can be done via a Turing machine.

And therein lies the answer to your question: although it's common to model computers as Turing machines, that is only a convenient idealisation. A Turing machine has an infinite tape. Real computers, given their finite memory and finite storage, are nothing more than (very large) finite state machines. And those are much more theoretically tractable beasts.

Re:Godel's Incompleteness Theorem? (2, Interesting)

bramez (190835) | more than 5 years ago | (#29050259)

you dont have to "get around Godel's Incompleteness Theorem". (from wikipedia:): "Any effectively generated theory capable of expressing elementary arithmetic cannot be both consistent and complete. In particular, for any consistent, effectively generated formal theory that proves certain basic arithmetic truths, there is an arithmetical statement that is true, but not provable in the theory". it says "a statement" not "every statement". So, you can make formal theories where a lot of statements are provable, including a large class of computer programs.

Re:Godel's Incompleteness Theorem? (1)

dmbasso (1052166) | more than 5 years ago | (#29050311)

Godel found that, within a system of axioms, there are questions you can't answer using only those axioms. The specification of an OS, although extensive, is not composed of "hard" questions. You don't need to prove P=NP for an OS to work.

Re:Godel's Incompleteness Theorem? (1)

TapeCutter (624760) | more than 5 years ago | (#29050341)

Incomplete != incorrect.

Re:Godel's Incompleteness Theorem? (1)

hasdikarlsam (414514) | more than 5 years ago | (#29050461)

Goedel's theorem simply states that you cannot prove a system in itself, for any sufficiently interesting system.. not repeating the definition of /that/ one here. In any case, this kernel qualifies.

But that doesn't at all prevent you from proving it in a higher-level system, such as the theorem prover they used. Um, though it would cause trouble if you want to prove the /prover/ correct...

Formal Methods vs Time (1)

ShipIt (674797) | more than 5 years ago | (#29050087)

I had a professor in college, along with several colleagues and students, working on a formal proof for nuclear power plant control software. They had been been working for 5 years and, at the time, were about 10% complete.

Obviously, at that rate, the time to complete the formal proof is probably longer than the lifetime of the particular control system they were targeting.

Hopefully Formal Methods have come a long way since I last studied them 10 years ago. In any case, congratulations to this team of researchers at NICTA.

Then a driver blows it all up.. (4, Funny)

tjstork (137384) | more than 5 years ago | (#29050089)

Suddenly after that, the proven kernel will be brought to its knees when someone adds a driver for an old graphics card.

Re:Then a driver blows it all up.. (0)

Anonymous Coward | more than 5 years ago | (#29050337)

Obviously we need proven graphics drivers. Maybe we need a pop up window saying, "Warning: About to execute Unproven Driver!"

I have no idea if I am joking or not.

Re:Then a driver blows it all up.. (0)

Anonymous Coward | more than 5 years ago | (#29050345)

seL4 is a microkernel so all drivers run in isolated domains and cannot affect the kernel - so if you have a bug in a driver, all that happens is the driver crashes and the rest of the kernel (and other drivers) keep on running - unlike Linux or Window which are monoliths and a bug in a single driver can bring down the whole kernel.

Idiot poster (1, Informative)

Anonymous Coward | more than 5 years ago | (#29050095)

every respectable geek knows the amiga hand is not an indication the system crashed, but the hardware asking for its OS.

Nope, the amiga crashes are known for the guru meditation, where the screen goes black and displays a BLINKING RED text.
Most amiga users have jumped out of their seat at least once or twice out of sheer surprise...

But... (2, Funny)

TheDarkMaster (1292526) | more than 5 years ago | (#29050099)

... we will lost all the fun for Blue Screens and Kernel Panics!

Singularity (1)

Vahokif (1292866) | more than 5 years ago | (#29050133)

What about Microsoft Research's Singularity? [wikipedia.org] AFAIK its kernel is written in a contract-based version of C# and can be proven correct.

Re:Singularity (1)

ledow (319597) | more than 5 years ago | (#29050215)

I think the relevant word is "can", not "has". It has the potential to do the same thing but doesn't seem to have made it that far. Provable but not proven?

And besides that, from the very article you linked to, I can spot a number of problems - such that isn't just written in one language and translated to a final, provable "one language + assembly" like the main article, but several (and a lot more than the bare minimum necessary to boot a kernel, it seems). It's kind of mid-way to what the main article has achieved.

Beware of bugs (0, Redundant)

mrjb (547783) | more than 5 years ago | (#29050147)

``Beware of bugs in the above code; I have only proved it correct, not tried it.''

Proven? (5, Insightful)

mseeger (40923) | more than 5 years ago | (#29050175)

There is an old corollary that says, you cannot get from the informal to the formal by formal means. All they have proven is, that two specifications contain the same bugs. Both specification were formal (Haskell, C). This is the same as having Perl and Python code and you to prove they implement the same functionality. Neither is a proof, it is bug free (informal definition of bug, not if a bug is specified it isn't a bug).

Wish I had mod points (2, Insightful)

Viol8 (599362) | more than 5 years ago | (#29050327)

This is something that people who bang on about formal proofs conveniently forget - all it does is move the bugs from the source code to the formal specification. And if the spec is detailed enough to be useful it effectively becomes code anyway so you might just as well write the actual code and debug *that* instead.

what if you made a kernel so perfect (1)

FudRucker (866063) | more than 5 years ago | (#29050199)

the kernel was so perfect that it thought it was god and it condemned the rest of the OS to hell

Re:what if you made a kernel so perfect (1)

jamesh (87723) | more than 5 years ago | (#29050243)

the kernel was so perfect that it thought it was god and it condemned the rest of the OS to hell

Windows is a good example of an OS that _thinks_ it is perfect. Fortunately Microsoft's idea of hell is my idea of heaven :)

Sounds like automated unit test generation to me (0, Offtopic)

Anonymous Coward | more than 5 years ago | (#29050203)

Most large scale commercial software that is worth anything has massive batches of automated unit and functional tests applied to it - How does this differ? Are they automatically generating their "formal proof" code (unit tests I assume). If so, how do the automatically generated tests stack up against manually generated versions? I would imagine said tests can catch a variety of bugs, but as regards insisting that a program has been verified "bug free" - I will believe it when I see it.

Re:Sounds like automated unit test generation to m (3, Informative)

maxwell demon (590494) | more than 5 years ago | (#29050415)

Formal proofs are not unit tests. Unit tests test that certain values work correctly. Formal proofs show that the code works to the specification in all cases (modulo errors in the proof, of course). They of course cannot find bugs in the specification (which unit tests might, if they test what you thought the specification said, instead of what the specification really said).

World's First Formally-Proven OS Kernel - NOT (3, Informative)

neongenesis (549334) | more than 5 years ago | (#29050241)

Do some research Guys...

Honywell SCOMP Early 1980s Was intended to me a secure front-end to Multics.

Verified by NSA et all as part of the first Orange-book A1 level certification.

For the time it was a magnificent bit of work.

Too late (1)

lisaparratt (752068) | more than 5 years ago | (#29050247)

I was fairly sure the OS running on the MONDEX smartcards was formally proven.

Yeah, but... (0)

Anonymous Coward | more than 5 years ago | (#29050273)

does it ru... uhhh... never mind.

excellent news (1)

Tom (822) | more than 5 years ago | (#29050283)

This should once and for all silence the people who claim that it's impossible to formally verify any non-trivial code.

Oh, what am I dreaming. They won't shut up, but maybe now they'll die out.

Re:excellent news (1)

Desler (1608317) | more than 5 years ago | (#29050447)

No, what people claimed was that to formally verify any non-trivial code that it would take a long time to do. This announcement proves that. It took them 5 years to verify 10,000 lines of code for something that isn't even that complex of a piece of code. Come back to us when you can formally verify a sufficiently complex kernel that can actually be put into production in less time and we'll talk.

If anything ever replaces the Linux kernel... (0)

Anonymous Coward | more than 5 years ago | (#29050285)

I would expect it to be something designed and built along these formal lines. So far, feature set has been the main driver for software development, with robustness coming second. The emphasis seems to be very slowly shifting, as some relatively high level feature sets are reaching a stable point.

In the case of single core CPUs, we do actually seem to have reached a fairly stable performance point now. The way things are pushing forward is with mult-core CPUs, which requires a different mindset of design previously restricted to high end supercomputer and cluster programming. Now even desktop machines will need to start worrying about multi-core related design issues.

This is a more complex sort of programming, and most of the work being done today seems to be more about making existing abilities work faster (naturally, as that's the highest immediate productivity payoff). Which is not to say there won't be a stream of new ideas that continues to flow - what I do mean is that increasingly high level features of operating systems and even system libraries will become "standard" and be worth putting the extra work in for provably correct behavior, particularly in the complex world of ubiquitous multi-core hardware. If you ALWAYS have to implement feature X to support existing design paradigms and tools, and the expected behavior of feature X is well defined de-facto, then it begins to make sense to define it formally as well and insofar as possible forever eliminate it as a source of ANY bugs. This will subsequently free the human resources to concentrate on other problems.

It remains to be seen if the admittedly severe demands of provable software design and development (toolchain, programmer discipline and background knowledge, etc.) can be supported by the broader (non-academic-based) open source community, but given all that it has achieved and the open source tools available in the proof software domain there are definitely some interesting possibilities. Certainly the potential payoffs are exciting! Interesting times.

OK, you had me going there for a while... (3, Interesting)

pedantic bore (740196) | more than 5 years ago | (#29050335)

This is a nice accomplishment, but L4 is such a minimal kernel that some folks argue that it's not even a microkernel. It's a picokernel.

It's a lot easier to get the kernel right when it only has twelve entry points...

kernel on a kernel? (1)

gbelteshazzar (1214658) | more than 5 years ago | (#29050363)

sorry, but they mention that they have linux running on top of their kernel? how can you run a kernel on top of a another kernel?

Not very useful... (2, Insightful)

jamesivie (805019) | more than 5 years ago | (#29050379)

In addition to what's already been pointed out about formal vs. informal specifications,

1. Running Linux on top of this is no more safe than running Linux directly on the hardware--it's Linux that crashes (though not very often!)

2. Running this on a CPU that has not been formally proven is nearly useless because only part of the system has been proven, which results in an overall system that is unproven.

Good News and Bad News (4, Insightful)

Jacques Chester (151652) | more than 5 years ago | (#29050389)

First off, as an Australian and a nerd, I am very proud.

Now.

Good news: there is now a formally verified microkernel. 8,700 lines of C and 600 odd lines of ARM assembly. Awesome.

Bad news: it took 200,000 lines of manually-generated proof and approximately 25 person-years by PhDs to verify the aforementioned microkernel.

Conclusion: formal verification of software is not going to take off any time soon.

Conflicting Theories (1)

crrkrieger (160555) | more than 5 years ago | (#29050391)

Isn't there a theory that if we ever get a formally proven OS that all OSs will instantly vanish and be replaced by something more complex? I think there is a corallary that says this has already happened. Obviously, the proof referred to must be mistaken as my OS is still running as I typ

Um, maybe I'm missing why this is such a big deal (1)

idiotnot (302133) | more than 5 years ago | (#29050419)

Okay, so you have a proven kernel. But it's L4. L4 provides nearly nothing in the way of functionality, just thread scheduling, and very rudimentary IPC.

Yes, an L4 kernel can be written in anything. Most variants have been written in C, but L4-Pistachio was written in C++. Anything that adheres to the L4 specification works. So it could be written in pretty much anything that doesn't require significant runtime libraries (and the associated overhead for filesystem handling, etc.).

Someone care to enlighten me?

Formally proven software (1)

jdimarco (109401) | more than 5 years ago | (#29050501)

In layman's terms, formally proven software is software written twice, once as a formal specification, and once as code, and then the two are proven to be equivalent. This is a labour-intensive way to write software, and it makes bugs much less likely, but it's not perfect: there can be corresponding errors in both the code and the specification, and there can be errors in the proof too. But nothing is perfect, and this certainly can be a good approach to write code that is as close as possible to bug-free.

Load More Comments
Slashdot Login

Need an Account?

Forgot your password?