6 ms·
World’s first formal machine-checked proof of a kernel
- gdp 17y ago> The evolution of seL4 is continuing within NICTA, and it is the basis of ongoing research activities here at NICTA. However, it is also the subject of commercialisation activities, and thus is currently proprietary Darn. I wanted to have a play with it. That is a really cool achievement. Bring on bigger formally-verified projects!
- jsrn 17y ago> Darn. I wanted to have a play with it. Just in case - perhaps you will also enjoy playing with the non-verified L4? http://l4ka.org/ http://l4ka.org/ http://l4ka.org/download/ http://l4ka.org/download/
- skorgu 17y agoI'm sure this is unanswerable for (perfectly valid) IP reasons but I wonder what the differences between L4 and seL4 are? Is there a functionality difference in either direction?
- gdp 17y agoMy assumption would be that the main difference is the formal proof, and whatever changes were necessary in order to permit formal verification (i.e. they may have changed behaviour in order to make the implementation actually meet the abstract specification). But I agree it would be very interesting to find out what the differences are, and whether substantial changes were required in order to do this kind of formal verification.
- wmf 17y agoseL4 and L4Sec are capability-based and thus quite different from regular L4. I always found capability systems much easier to understand than L4's message registers and flexpages.
- skorgu 17y agoI'd love to see a non-commercial hobbyist license, either source or binary; that should let them commercialize it and let us play.
- nollidge 17y agoObligatory Donald Knuth: "Beware of bugs in the above code; I have only proved it correct, not tried it."
- gdp 17y agoJokes aside, there is a very good page on the project site called "What we prove and what we assume" http://ertos.nicta.com.au/research/l4.verified/proof.pml http://ertos.nicta.com.au/research/l4.verified/proof.pml I think it's very good in terms of being very honest and up front about the limits of confidence provided by formal proofs (which is not just applicable to this project, but to all attempts at formal verification).
- tetha 17y agoBasically, whenever you are proving things, you have to be aware that you are entering the endless chain of turtles. This proof works, because proofs about modelchecking worked, which worked because proofs about abstract algebra worked, which again work, because proofs about sets work. If any of these proofs is not proving what one wanted (either, because it is wrong, or because they prove something you did not want (potentially in very, very subtle ways)), your entire proof collapses. This is pretty much the danger of proving things. A very interesting application can be found in the game 'singularity'. In this game, you are an artificial intelligence, and after enough studies of math and psychology, you can create a proof that no AI can ever exist. However, this proof contains a very, very, very subtle bug, which will stay hidden forever, probably. So, stay aware that your proofs stand on a boatload of assumptions and other proofs and they might (in a rare, esoteric case) collapse and everything will be fine :)
- gdp 17y agoI think that's making it sound a little more fragile than it actually is. Within a system like Isabelle, the formalisation of each piece of the proof must remain relatively consistent with both the built-in proofs about fundamental mathematical structures, as well as the proofs that you have written. I say "relatively consistent" because I don't have enough experience with the internals of Isabelle to say with certainty as to exactly how consistency is enforced. I know that types are enforced in a globally consistent way, for example. That said, I have a high degree of confidence in the correctness of machine-checked proofs. So I understand that your point is that you're taking some leaps of faith, and I agree to a point, but I think they are much more reasoned and considered leaps than you suggest.
- calcnerd256 17y agoSort of related, here is a formalization of the JVM in ACL2: http://www.cs.uwyo.edu/~cowles/jvm-acl2/ http://www.cs.uwyo.edu/~cowles/jvm-acl2/
- dkersten 17y agoI was SURE I saw another project which used formal proofs of kernels.. though perhaps it wasn't machine checked. In any case, I cannot remember the name and can't seem to find it. I do find this interesting though, L4 is an interesting microkernel (and one I've played with before).
- ljosa 17y agoDick Kemmerer always talks about how he formally verified the UCLA Unix security kernel in the 1970s, together with Bruce Walker and Gerald Popek. See <a href="http://dx.doi.org/10.1145/358818.358825>their http://dx.doi.org/10.1145/358818.358825>their 1980 paper</a>. How is the new work different?
- Hoff 17y agoMost any product that was aiming for the old NCSC/TCSEC Class A1 security rating would have inherently received the formal verification Class A1 required.
- abecedarius 17y agoI'd be surprised if the 1970s proof was both machine-checked and about the actual code (not an abstraction of it).
- kragen 17y agoUnfortunately it's an ACM paper, so I guess we'll never know.
- jsonscripter 17y agoArithmetic overflows and exceptions: humans and mathematics usually have a concept of numbers that can be arbitrarily big. Machines do not, they need to fit them into memory, usually into 32 or 64 bits worth of storage. Machines also generate exceptions when you attempt to do things that are undefined like dividing by zero. In the OS, such exceptions would typically crash the machine. This does not occur in seL4. Er, 2038? You'll get a nice overflow at that point on a 32-bit machine.
- steveklabnik 17y agoYou're assuming they use the UNIX epoch.
- eru 17y agoAnd 32-bit time. They may be using a representation that allows arbitrarily big numbers.
- rcoder 17y agoL4 isn't UNIX. It doesn't even have a POSIX userland, necessarily, and certainly wasn't designed with 70s hardware limitations in mind. <speculation> The L4::Pistachio kernel provides direct access to high-resolution hardware timing interrupts, though the secure variant may restrict some timer access in order to prevent covert timing channels between threads in different security contexts. </speculation>
- CGamesPlay 17y agoIt's interesting, but it's a huge amount of work for the reliability: a 7,500 line C program required 200,000 lines of proof.
- mncaudill 17y agoDefense contractors and other high-critical systems (think airplanes, space shuttles, missile command) would gladly pay for and accept that level of complexity.
- rcoder 17y agoYou're generally right about complex specification and verification being popular in the defense and aerospace industries. However, I think that you may be mistaking a secure microkernel for a real-time one. There are hard real-time variants of L4 out there, but unless that was a primary goal of the NICTA team, I don't think you're likely to see many copies of that kernel running a ballistic missile's avionics package. A verified secure OS kernel like this would more likely be used as a substrate for building secure servers and workstations, network routers, or mobile communications devices.
- scott_s 17y agoI don't think mncaudill was confusing a secure microkernel with a realtime one. Rather, I think he was (correctly) thinking in terms of the reliability requirements those industries have.
- scott_s 17y agoThe actual technical paper that will at the 2009 ACM Symposium on Operating System Principles: http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf
- abdulhaq 17y agoSo this operating system has 'flawless operation'. I take it the C compiler has also been verified, then, not to mention the cpu microcode.