World's First Formally-Proven OS Kernel

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.

Comments

spec?

[polar red]

but is the spec useable ? bugfree ?

Re:spec?

[VoidCrow]

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.

Re:spec?

[jadrian]

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?

[JasterBobaMereel]

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?

[Anonymous Coward]

I'm not going to go into a lot of detail here, but the common criteria defines 7 levels of assurance; EAL 1-7. EAL 1 equates to no robustness. EALs 2-4 equate to medium robustness. EALs 5-7 equate to high robustness. An OS, or in the case of the kernel mentioned on the home page a hypervisor, is evaluated against a protection profile. The protection profile is the spec asked about by the original poster. I believe there is only one protection profile, applicable to an OS or hyperviser, that has been evaluated to high robustness - the separation kernel protection profile (SKPP). Generally, when an OS is evaluated against a PP, it is proven to meet at least the minimum requirements of that PP. Or, another way to look at it is, it will be proven do everything it says it is going to do and nothing else.

An OS/hyperviser is evaluated. The OS/hypervisor + applications + hardware is accredited. The OS/hypervisor + applications + hardware + installation is certified.

As an interesting side note, there is a protection profile that evaluates to medium robustness which specifies an OS on a computer not connected to a network in an enclosed room with an armed gaurd standing at the door. WinXP has been successfully evaluated to medium robustness against this PP.

Re:spec?

[Amouth]

actualy it's both.. cosmic ray's flipping bits is a concern.. or disrupting clock cycles.. there is a reason they use slower larger circuits in long term space applications..

Re:spec?

[orangesquid]

The study of the halting problem taught us that certain categories of algorithms cannot be formally proved to do certain things. Work on incompleteness tells us that we know algorithms must exist that fit that category.

The question, really, is whether the algorithms in and design of operating systems can be done in such a way that we don't run into incompleteness and halting-problem issues within the constraints of what we are trying to achieve -- after all, we aren't trying to achieve the impossible, just trying to make some specific, absolute guarantees.

I'd recommend a solid study of the Mizar Journal of Formalized Mathematics, the implications of the standard axioms of set theory (maybe including reduced forms of the axiom of choice, but that's not necessarily highly relevant), and careful analyses of what Goedel and Turning actually proved. After that, emergent behavior from cellular automata may be a good next investigation.

[IANA professional set-theory mathematician, logician, nor computer scientist, so take my post as a starting point for finding answers, please, not as anything definitive!]

Re:spec?

[digitig]

The study of the halting problem taught us that certain categories of algorithms cannot be formally proved to do certain things. Work on incompleteness tells us that we know algorithms must exist that fit that category.

The question, really, is whether the algorithms in and design of operating systems can be done in such a way that we don't run into incompleteness and halting-problem issues within the constraints of what we are trying to achieve

And the answer in this case is pretty certainly "Yes, we can"; the tasks you can't do without running into halting or incompleteness issues are pretty esoteric and well outside the sort of thing an OS kernel would sensibly be called on to do.

Re:spec?

[Brewmeister_Z]

I worked as software engineer on avionics. The device I wrote for had a 486 chip and was basically the GUI for other avionics such as navigation and communication. It used a bunch of military and avionic standard protocols to communicate to the other boxes. I started coding for it in 2000 and at time it was just updates, new features and new boxes to integrate. However, they were on their way to porting this to PowerPC chips and using TCP/IP to a scalable multiple processor/box approach instead of a master/slave in two 486 boxes. The port to PowerPC also had forethought to write code that code be modular since the endian and bit size of the data had to be changed so code was was devised to know which architecture was being used for data.

The main reason for the port to PowerPC was the lack of 486 chips for new hardware for retrofitting other aircraft. At this point, they maybe looking for a new chip to replace the PowerPC.

Re:spec?

[kamatsu]

1) L4 is a microkernel. You have no idea what you're talking about. If L4 works, then you could apply similar principles for all the other servers that run in kernel space.

2)This is the largest formal proof ever done in this sort of field. Seriously, the results are not immediately useful, but it's a good start.

Disclaimer: I have worked at NICTA in the past.

Re:spec?

[ockegheim]

...and somewhere between halting and incompleteness, Omega sits, mocking us.

Re:spec?

[Tanktalus]

In your case? I think the second word is "*WHOOSH*".

Re:spec?

[TheLink]

Exactly. That's why these formal verification stuff is rather useless for most cases I see.

If you pass the customer a mix of water, flour, yeast, eggs and sugar and the customer says "That's not cake, it's not acceptable".

And you then say - "But we meet the cake spec we agreed on, so by that definition it's cake, you have to pay us".

Sure you can go sue the customer and force them to pay you the full sum, but unless most other people agree the customer has just been way too fussy, you might have fewer customers in the future.

Amiga Hand?

[ArcadeNut]

Or do you mean the "Guru Meditation Error"?

The Amiga Hand?

[johannesg]

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?

[TheCycoONE]

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?

[Anonymous Coward]

The missing word is formal.

They use a formal specification, which is then formally verified.

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.

Re:The Amiga Hand?

[Tom]

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.

Re:The Amiga Hand?

[feldicus]

"Easier to read" is subjective, and generally only applies if the reader has spent a fairly significant amount of time dealing with the syntax. Coming from years of C/C++/C#/Python, I can tell you that Haskell is about as easy to read as a set of VCR instructions written in Japanese and translated to English by a blind Venezuelan with Carpal Tunnel Syndrome.

Re:The Amiga Hand?

[Chris Mattern]

The benefit is if the specification is right, the program should be right.

We'll have to prove the specification does what we want, then. Of course, then we have to make sure our conception of what we want is right...

Personally, I think it's elephants all the way down.

Re:Yeah right

[oji-sama]

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

Give me six lines of code...

[Joce640k]

"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...

[Telecommando]

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...

[ranulf]

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

HACF?

Re:Give me six lines of code...

[Anonymous Coward]

/*
  *
  *
  *
  *
  */

Re:Give me six lines of code...

[etwills]

In PHP I once had a bug in the whitespace of a comment. When I left the /* and */ away, and the comment just stood there as if it were code, it worked. Go figure...

Nested comments maybe? If you hadn't noticed the outer comment markers, you'd get something that "didn't" work with the inner markers in place and "did" work without.

(In PHP, attempting to nest comments leads to the second '/*' being considered as enveloped by the first '/*' and the first '*/', leading to the second '*/' being flagged as erroneous, and the interpreter bailing out)

// writing my first bit of non-trivial PHP _today_

Apps running on top will crash... so

[WiseOwl2001]

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

[John Hasler]

> 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

[Fri13]

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

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

[Tom]

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.

Knuth on proven correct:

[John Hasler]

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

Re:Thank goodness

[morgan_greywolf]

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

[johannesg]

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!

Then a driver blows it all up..

[tjstork]

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

But...

[TheDarkMaster]

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

Who proved the proof-checker?

[Dr. Manhattan]

Recursion (n): see recursion.

Re:Who proved the proof-checker?

[Kerrigann]

I'm not saying it's impossible, just that it's *much* harder to understand than simply writing it recursively.

Let me put it this way... suppose in C++ you have a template instantiation defined dimension matrix...

In order to do operations on the matrix, you have to iterate through an arbitrary number of dimensions, then loop over (a subset of) the length of the matrix in that dimension. It's like a for loop inside a for loop, but the number of for loops deep has to be *runtime defined* (well, in my case template defined, but you get the idea). Without recursion you end up either writing gotos, or some other funky math where you determine the overall size of the n-dimensional matrix (dimensions multiplied together) and then loop through that index, and figure out the actual n-dimensional coordinates as you go (messy).

Here it is in code...

        template<typename OpType>
        inline Array& eval(OpType op, IndexType index = IndexType(),
                        size_t dim = 0) {
                for(size_t i = 0; i < extent(dim); ++i) {
                        index[dim] = i;
                        if(dim == Dimension - 1)
                                operator()(index) = op(index);
                        else
                                eval(op, index, dim+1);
                }
                return *this;
        }

where IndexType is some vector unsigneds of size Dimension, extent is a member function that returns the size of the array in that dimension, and operator() retrieves the value at the given location.

This is a (modified for clarity) member function of a class I have called Array, that has template defined dimension. I'm filling the Array by calling the passed in function on every location in the Array, and assigning the result to the location.

You *can* write it without recursion, but it's even more confusing than what I wrote.

There are probably better examples of exponential time algorithms that are clearer, but they make my head hurt.

By the way, at my old job, our simulation had to interpolate lots and lots and lots of experimentally gathered data in big tables (like an 11 dimensional table for infrared signature data). Writing an arbitrary dimensional interpolation library was the *simplest* option :)

Re:Who proved the proof-checker?

[dumael]

Compilers that implement something called Tail Call Optimization can convert recursive functions into iterative equivalents. This relies on the function either: returning a value *or* the result of a call to another function with new parameters. (it can be the same or different function) e.g. a way to do it in C would look like:

f(int x){
.. some code ..

if( cond )
return 0;
else
return f( x + y);
}

Although in C it can look very ugly, for functional languages such as Haskell or Erlang, it is required as you have to express loops through recursion due to only being able to assign to variables once. In these langauges, it looks a lot better as you can pattern match on the value of arguments, allowing you to concisely deal with obvious error or base cases, leaving you to handle the generic cases without worrying about those cases. Scheme implementations are required to implement tail call optimization.

Re:Who proved the proof-checker?

[Jeremi]

If he were being honest, he would say that recursion is a just convoluted, unnecessarily confusing method of doing iteration

Some would say that iteration is just a convoluted, unnecessarily confusing method of doing recursion.

For example, try iterating over all the nodes in a tree without using recursion. It's doable, but more complicated and error-prone than the recursive method.

Proven?

[mseeger]

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).

Re:Godel's Incompleteness Theorem?

[TheSunborn]

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:Provable?

[jamesh]

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

Then obviously this OS is not sufficiently complex.

World's First Formally-Proven OS Kernel - NOT

[neongenesis]

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.

Re:World's First Formally-Proven OS Kernel - NOT

[TheRaven64]

Thanks, I was surprised by this claim too. I remember hearing back in 2007 about a formally-verified kernel written in Ocaml that some people at Cambridge had written, and they weren't claiming that theirs was the first (although it may have been the first to run on commodity x86 hardware).

Re:Godel's Incompleteness Theorem?

[bramez]

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.

Wish I had mod points

[Viol8]

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.

Re:Wish I had mod points

[Anonymous Coward]

That this moves the bugs to the formal specification is true, but that therefore you might just as well write the actual code is an invalid derivation. Formal specification languages are designed with the idea that one should be able to reason about them in mind (be it manually or with the help of automatic/interactive theorem proving, model checking). This typically leads to a language in which systems can be expressed on a higher level, because performance issues are not important: the specification does not need to be executed. Due to this higher level and the fact that they are easier to reason about with tool support, it is easier to find a bug in a formal specification than it is in programming language code.

Re:Wish I had mod points

[ralphbecket]

I don't thinks that's fair: the spec. just says *what* properties the system should have; the implementation says *how* those properties are provided. Where you can do it, denotational semantics (the spec.) let you say a lot more than you can with operational semantics (the code).

Of course, your argument also suffers from circularity: to debug code you have to have a spec. in the first place to tell you when the implementation is doing the wrong thing.

OK, you had me going there for a while...

[pedantic bore]

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...

Re:OK, you had me going there for a while...

[noz]

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.

Microkernels provde:

• address spaces
• threads
• IPC

L4 checks these boxes. Nanokernel and picokernel are poorly defined, emotive terms. Not reasonable criticism.

Re:Provable?

[bramez]

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.

Not very useful...

[jamesivie]

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

[Jacques Chester]

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.

Re:Sounds like automated unit test generation to m

[maxwell demon]

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).

Re:Empty promises...

[ezzzD55J]

Most faults on most platforms are caused by hardware faults

bullshit.

Great work, but...

[Salamander]

...there are two caveats. One is that "executable specification in Haskell" is a bit of a dodge. It means that they have effectively verified the translation from Haskell to C, but if there are bugs in the Haskell then there will be bugs in the C as well (in fact this is part of what they've proven). They admit as much at the very top of http://ertos.nicta.com.au/research/l4.verified/proof.pml, but it still leaves the question of why this is any better than simply rewriting the microkernel in Haskell. If the benefit of a concise and abstract specification is lost, what's left?

The second major caveat is that they had to leave out some features that they couldn't verify. Most significant is that they didn't verify multi-core - by which it seems they mean multi-processor, but "multi-core" is the much hipper word. Since even laptops are multi-processor now, this limits applicability until they take the next step. With all of these shortcuts, though, if you look at the list of what they did manage to verify - mostly pointer errors and overflows - it's not clear that it couldn't have been done with a more real-code-oriented tool such as the Stanford Checker or sparse.

Re:Thank goodness

[Anonymous Coward]

Name the logic that C is based on, then.

C may be "logical" in a colloquial sense. It's not based on a formal logical calculus.

Do you even know what the hell you are talking about?

Re:Thank goodness

[Idiot with a gun]

It's a paradigm, technically. Although Haskell isn't a logic language, it's functional. Prolog is logical, and nigh useless for most applications.

You mean they aren't all tested like this?

[Remus Shepherd]

As someone who does not work in IT, count me as surprised that not all OSes are tested this rigorously.

Re:You mean they aren't all tested like this?

[maxwell demon]

Linux has more than ten million lines of code. Given that they needed 5 years for 12 persons to verify ten thousand lines of code, this means verifying the Linux kernel would give an estimated cost of 60,000 man-years. So even if they got a thousand people doing nothing else but verifying the Linux kernel, it would take then 60 years to finish.

Re:You mean they aren't all tested like this?

[DerekLyons]

That more like "not only doesn't work in IT, but doesn't know of or understand the theory". No slam, just the facts.
 
Seriously, the reason all OSes aren't tested this vigorously is that the time/amount of work needed to do so rises exponentially with the size/complexity of the OS. Not only does that imply the OS would take years to bring to market, but also that said OS would incredibly expensive. Worse yet, after all that time and expense, all you've actually proven is that your running code matches your specification - you're protected against errors arising from faulty programming, but not from errors arising from conceptual errors in the spec or from incorrect algorithms embedded in the spec.

Re:Empty promises...

[Anonymous Coward]

Thanks for quoting me.

You're welcome. (I am not the poster you replied to, but you're full of shit)

It's paravirtualization

[Lemming Mark]

Disclaimer: my background is on working on Xen but I have a research interest in L4, amongst other things. Should also note that I've not yet RTFA'd but I will do as it sounds awesome.

Paravirtualization is where you modify a kernel so that it can run on something other than "bare hardware". Often in this situation you call the kernel that *does* run on bare hardware the "hypervisor" to distinguish it from the Linux (or whatever) kernel running on top. In this case Linux is running on top of their L4 kernel as a userspace program - instead of accessing parts of the hardware to get its job done it uses L4 system calls. This is basically the same as what Xen does, with L4 taking the role of the hypervisor. Researchers working on L4 have been playing with Linux-on-L4 for many years - longer than Xen has been about, AFAIK.

One nice trick you get, in this case, is that you have the ability to run Linux programs on your nice, formally-proven microkernel. But alongside that you can still run programs *directly* on the L4 kernel, independently of Linux (or with some controlled interaction with it). So, say you have some untrusted code you want to sandbox - you can run it directly on L4, which (now) has proven security properties. Or perhaps you have a crypto app which you want to isolate from Linux in case a root exploit leaves it vulnerable - you can run it directly on L4, outside Linux. You could potentially do similar things for programs that need realtime guarantees - let normal applications get scheduled by Linux's scheduler and realtime apps run directly on L4.

Basically, having L4 there is giving you an ability to start other "virtual machines" running paravirtualised OSes or high assurance applications. It's always been part of the goal that because L4 is simpler than Linux you get to have high assurance that it'll do what it's supposed to. Now a derivative has been formally proven the guarantees could potentially be even better.

The TUD:OS demo CD website has some interesting information about a real-world system that mixes the ability to run (multiple) Linux virtual machines, plus isolated secure applications, all under a security-oriented GUI. It's a pretty cool demo and you can run it as a LiveCD: http://demo.tudos.org/

Re:Thank goodness

[xaxa]

It's a paradigm, technically. Although Haskell isn't a logic language, it's functional. Prolog is logical, and nigh useless for most applications.

No, it's just more difficult to write the program for most applications.

IMO, it's because it's more difficult to precisely articulate the problem and method (for Prolog) than to work through the solution (for an imperative language).

NOT TRUE: Remeber Dijkstra & THE?

[fortunatus]

In the 1960's Edsger Dijkstra (arguably one the founding fathers of "Computer Science", at least as a university subject) led a group at Eindhoven to develop a multiprocessing OS called "THE". The kernal was formally proven BY HAND .

I daresay the folks who have made this recent excellent achievement are likely well aware of THE, and therefore are being specious in claiming to be the world's first at doing this.

A truly marvelous

[autophile]

I have written a truly marvelous bug-free operating system, however there is not enough space on this disk to include it here.

Re:Thank goodness

[arethuza]

While C includes some logical operators based on boolean logic most of the language has no connection whatsoever to anything that looks like formal logic. Compare this to Prolog - which has a much closer mapping to predicate calculus or pure functional languages which have a very good mapping to lambda calculus.

Re:Empty promises...

[JKDguy82]

You gotta love how a single word "bullshit" response gets modded "Insightful".

Re:Thank goodness

[kamatsu]

Dude, can C's types be reasoned by formal inference? No. Hence, C does not follow typed logical calculus.

C doesn't follow boolean logic either, actually, it just maps to assembly instructions. The best thing you could do to reason about C is to use Dijkstra's proof method which is impractical in a large scale and easy to screw up.

Re:Empty promises...

[Wraithlyn]

The context of your full original post does not change the fact that you claim most faults are caused by hardware, which is the specific point he was disputing.

If you have something to strengthen your claim (from your original "context" or otherwise), present it. Otherwise, complaining about being quoted "out of context" is just rhetorical posturing.

Re:Thank goodness

[ioshhdflwuegfh]

You know the funny thing about this whole discussion is that the OS linked to in the article is not the first. Integrity from Green Hills Software was proven correct a while ago. It is popular for safety critical stuff like flight controls for airplanes and is one of the dominant players in that niche.
http://www.informationweek.com/blog/main/archives/2008/11/green_hills_sof.html
And what is truly amusing about following this argument, is that Integrity is written in C. :)

Although I can see that you're amused, what you're saying is false: Integrity is not formally proven correct, it only has some amusing but mathematically irrelevant industry certificate.

Re:Thank goodness

[morgan_greywolf]

You're conflating two different concepts. Common Criteria Evaluation Assurance Level focuses on security while this test focuses on complete mathematical provability IOW, can it be mathematically proven that the kernel meets all of its specifications and that the compiled kernel is exactly what was specified in the source code? CC EAL focuses only on security aspects.

Furthermore, a system that was specified as being completely secure[1] would, in theory, be equivalent to a EAL 7, not merely "6+".

[1] I mean this only in a hypothetical sense since I don't believe it is even possible to specify a system that is completely impenetrable, let alone implement one. But then, that's because I subscribe to the theory of information security that says a completely secure system is impossible, therefore we must use multiple compensating ocntrols that get us to a 'virtually impenetrable' state, tuned to prevent the most likely types of attacks (cheap) vs. the possibility of someone building a multi-billion dollar super cluster to break the security.

Re:Thank goodness

[kamatsu]

It doesn't return anything about success or failure.

My experience with formally proven OS in the 80's

[chongo]

This Slashdot article, referring to the so called "World's First Formally-Proven OS Kernel",was brought to my attention by a colleague who is aware of my experience with formally proven OS' in the 1980's. What follows is my response to the claim of being first, and the value of proving the correctness of an OS:

I am aware of at least two instances of operating system kernels that were built in the late 1970's / early 1980's using formal proofs of correctness. I will talk about my experience with one of them.

One of them, produced in the late 1970's was a kernel designed for a specialized environment. This kernel/OS was a reasonably functional kernel complete with multiprocessing, time-sharing, file systems, etc. Unfortunately while the formal proof for this kernel was solid, the axiomatic set on which this formal proof was based did not perfectly match its operating environment. This mismatch proved to be fatal to the OS security.

This formally proven OS took years to create and prove its correctness. Those who developed and maintained the OS were very proud of their work. There were plans underway to create a commercial version of their work and to market it through a certain hardware vendor on which their OS ran.

When I was a student intern working for the organization where that developed this OS worked, I worked in their OS environment from time to time. I came in from the outside where my OS experience was with a wide variety OS' such as MVS, NOS, KRONOS, TOPS-10, RSTS/E, VMS, Multics, and Unix (5th/6th/7th edition). I had enough experience in jumping into new OS environments that I felt comfortable as a user in this one, even though it was unusual.

An important point to observe here is I was one of the first people who enter this OS environment from the outside. I was not steeped in the development world of the OS. I brought with me, ideas that differed from the OS developers. As a young student, I believed that the OS should work for me instead of getting in my way. To help come up to speed, I ported over my collection of OS-independent tools and soon began coding away on my assigned tasks.

Then one day, working within my OS-independent tools, something very odd happened. By mistake, I did something that produced an unusual result. I quickly realized that something was very wrong because the result was "impossible" according to the formal proof of OS correctness. Under the rules set down by my employer I immediately contacted the appropriate security officer and the next thing I knew, I was in a long sequence of meetings with people trying to figure out what in the hell happened.

In the first meeting after my mistake, I learned that I had been reassigned to a new team. I was assured that I was not being disciplined, far from it: I had made a number of people very happy and they moved paperwork mountains to move me into their team. This team was given a task of attempting to repeat my previous "mistake" as well as to discover if exploits that are more general were possible against this OS. We were assigned to work âoeundercoverâ as developers under test/QA installations using this OS. In the end, the team was successful in discovering a much more general form of the OS hole I accidentally found.

What went wrong with the OS formal proof? Well the mapping from the formal logic world to the real world of hardware, physics, people, and the environment was flawed. In other words, when you added in the "real-world", the proof was incomplete. Attempts by the OS developers to expand their proof to address the "real-world" only produced a set of inconsistent theorems. I believe the OS project was abandoned after the OS developers failed multiple times to expand their formal proof to deal with âoereal-worldâ environments.

During this experience I was introduced to two "Security Camps": One, "the absolutists" as they called themselves, included people who worked on this formally proven OS. The opposing camp called the