3 ms·

"In short, the implementation is proved to be bug-free." This reeks of bull shit. "We still assume correctness of hand- written assembly code, boot code, mana

"In short, the implementation is proved to be bug-free." This reeks of bull shit. "We still assume correctness of hand- written assembly code, boot code, management of caches, and the hardware" Sorry, I don't think you can claim you have a mathematical proof of the correctness of your kernel when you assume this much. And where is this proof? I can't seem to find it anywhere on their web site. The only thing I can find is the publication "seL4: Formal Verification of an Operating-System Kernel" http://ertos.nicta.com.au/research/l4.verified/pubs.pml http://ertos.nicta.com.au/research/l4.verified/pubs.pml which looks like it just talks about the proof, rather than providing it. Am I just blind? This looks interesting, but the confidence which they espouse is very suspicious.

daveasdf 12y ago
This reeks of bull shit The proof states that the C code of the kernel is a refinement of an high-level "abstract" specification of the kernel. This means that the C code only exhibits behaviours that are also exhibited by the high-level specification. The high-level specification (by construction) doesn't have certain bad behaviours that you often see in C programs: NULL pointer dereferences, buffer overruns, signed integer overflow, etc. Thus this class of bugs is proven to be absent. A good primer is available at: http://www.ertos.nicta.com.au/research/l4.verified/proof.pml http://www.ertos.nicta.com.au/research/l4.verified/proof.pml The original proof didn't make any claims about the high-level behaviour of the kernel, such as security. So for instance, the original kernel might have had a bug where you set up a system so that two processes shouldn't be able to communicate with each other, but after some unexpected sequence of API calls they form a communications channel between them. NICTA in the following years after the initial proof carried out two security proofs: an integrity proof and an information flow proof. These proofs state that the capabilities possessed by a process determine (i) what other processes a particular process can modify; and (ii) what other processes the process can communicate with. Like the original proof, these security proofs (especially the second) have assumptions. In particular, they can only talk about parts of the system that are modelled. Timing channels, hidden CPU state, etc. not modelled by the proof may still allow information flow between processes, for instance. Sorry, I don't think you can claim you have a mathematical proof of the correctness of your kernel when you assume this much. You need to assume something. Every operating system kernel makes these assumptions: seL4 is just explicit about them. Some of the assumptions are bigger than others (management of caches is a pain to get right and hard to test, for instance). Some assumptions remain just due to a lack of time, such as proving the initialisation code of the kernel. Additionally, as time has gone on the assumptions have been reduced. For instance, the work of Thomas Sewell and Magnus Myreen mean that the compiler no longer needs to be trusted: https://www.cl.cam.ac.uk/~mom22/pldi13.pdf https://www.cl.cam.ac.uk/~mom22/pldi13.pdf And where is this proof? I can't seem to find it anywhere on their web site. The proof will be part of the open-source release. It consists of around 200,000 lines of Isabelle/HOL proof script, which is machine-checked. Anyone will be able to inspect/modify/check the proofs after the release.
- dead10ck 12y ago
  This means that the C code only exhibits behaviours that are also exhibited by the high-level specification. The high-level specification (by construction) doesn't have certain bad behaviours that you often see in C programs: NULL pointer dereferences, buffer overruns, signed integer overflow, etc. Thus this class of bugs is proven to be absent. The problem I take with the literature is that it does not say that it is free of certain classes of bugs. The wording implies that it is completely bug-free. As any software developer knows, bug-free software does not exist. Furthermore, You need to assume something. Every operating system kernel makes these assumptions: seL4 is just explicit about them. they claim they have proven that their kernel is completely bug-free. They say they have proved this under the assumption that the assembly code was written correctly. It seems that what they have claimed is: we have proven our kernel is correct with a proof that assumes that the code is written correctly. The logical flaw in this is obvious. I don't take issue with claims of correctness, given that they are precise about what they have proven. I do take issue with inflated claims ("bug-free" vs. "free of bugs from this specific class of bugs") for marketing purposes.
adamgravitis 12y ago
When people talk about proofs of correctness of software, they don't generally mean some bloke has gone and worked out on paper a formal proof. It means that they have used provably correct methods and then run the whole thing through an automated verifier. It's not bull shit, it's just hard.
nl 12y ago
I'm not sure you are aware, but formal verification[1] is a well known and respected field of research. It does work, but it is hard to build practical tools using it. Nevertheless, if something is formally proven correct then for it to be incorrect one of three things must happen: 1) The proof is incorrect (which of course means it is no longer proven) 2) The prover has a bug (most proofs are done automatically). This is possible, but many of the same formal methods are used on the prover, and it is often build on a human-proved proof at the bottom. 3) Mathematics (the whole field) is wrong. This seems unlikely. In reality, the problem with formally verified software is generally that it must interact with non-verified software (and sometimes hardware - although hardware can be verified too). The wikipedia page[1] I referenced is worth reading. [1] http://en.wikipedia.org/wiki/Formal_methods http://en.wikipedia.org/wiki/Formal_methods
- josephlord 12y ago
  4) It meets the specification but the specification is incorrect/specifies sub-optimal behaviour.
  - nl 12y ago
    If you can fix that problem in the general case then you are about to be a very, very rich person.
- daveasdf 12y ago
  The prover has a bug (most proofs are done automatically). Minor point: while many formal verification projects are proven automatically, seL4 is proven in Isabelle/HOL which is an interactive theorem prover. This means that the proofs are actually carried out mostly manually. (The downside is that it takes much longer to carry out proofs; the upside is that you can prove far more sophisticated properties than is possible with the current state-of-the-art automated provers). You are still right that the proof checker could have a bug, though. Proof checkers tend to be much smaller and simpler than things like SMT solvers, which helps increase confidence in them, however.

daveasdf 12y ago

This reeks of bull shit The proof states that the C code of the kernel is a refinement of an high-level "abstract" specification of the kernel. This means that the C code only exhibits behaviours that are also exhibited by the high-level specification. The high-level specification (by construction) doesn't have certain bad behaviours that you often see in C programs: NULL pointer dereferences, buffer overruns, signed integer overflow, etc. Thus this class of bugs is proven to be absent. A good primer is available at: http://www.ertos.nicta.com.au/research/l4.verified/proof.pml http://www.ertos.nicta.com.au/research/l4.verified/proof.pml The original proof didn't make any claims about the high-level behaviour of the kernel, such as security. So for instance, the original kernel might have had a bug where you set up a system so that two processes shouldn't be able to communicate with each other, but after some unexpected sequence of API calls they form a communications channel between them. NICTA in the following years after the initial proof carried out two security proofs: an integrity proof and an information flow proof. These proofs state that the capabilities possessed by a process determine (i) what other processes a particular process can modify; and (ii) what other processes the process can communicate with. Like the original proof, these security proofs (especially the second) have assumptions. In particular, they can only talk about parts of the system that are modelled. Timing channels, hidden CPU state, etc. not modelled by the proof may still allow information flow between processes, for instance. Sorry, I don't think you can claim you have a mathematical proof of the correctness of your kernel when you assume this much. You need to assume something. Every operating system kernel makes these assumptions: seL4 is just explicit about them. Some of the assumptions are bigger than others (management of caches is a pain to get right and hard to test, for instance). Some assumptions remain just due to a lack of time, such as proving the initialisation code of the kernel. Additionally, as time has gone on the assumptions have been reduced. For instance, the work of Thomas Sewell and Magnus Myreen mean that the compiler no longer needs to be trusted: https://www.cl.cam.ac.uk/~mom22/pldi13.pdf https://www.cl.cam.ac.uk/~mom22/pldi13.pdf And where is this proof? I can't seem to find it anywhere on their web site. The proof will be part of the open-source release. It consists of around 200,000 lines of Isabelle/HOL proof script, which is machine-checked. Anyone will be able to inspect/modify/check the proofs after the release.

dead10ck 12y ago
This means that the C code only exhibits behaviours that are also exhibited by the high-level specification. The high-level specification (by construction) doesn't have certain bad behaviours that you often see in C programs: NULL pointer dereferences, buffer overruns, signed integer overflow, etc. Thus this class of bugs is proven to be absent. The problem I take with the literature is that it does not say that it is free of certain classes of bugs. The wording implies that it is completely bug-free. As any software developer knows, bug-free software does not exist. Furthermore, You need to assume something. Every operating system kernel makes these assumptions: seL4 is just explicit about them. they claim they have proven that their kernel is completely bug-free. They say they have proved this under the assumption that the assembly code was written correctly. It seems that what they have claimed is: we have proven our kernel is correct with a proof that assumes that the code is written correctly. The logical flaw in this is obvious. I don't take issue with claims of correctness, given that they are precise about what they have proven. I do take issue with inflated claims ("bug-free" vs. "free of bugs from this specific class of bugs") for marketing purposes.

adamgravitis 12y ago

When people talk about proofs of correctness of software, they don't generally mean some bloke has gone and worked out on paper a formal proof. It means that they have used provably correct methods and then run the whole thing through an automated verifier. It's not bull shit, it's just hard.

nl 12y ago

I'm not sure you are aware, but formal verification[1] is a well known and respected field of research. It does work, but it is hard to build practical tools using it. Nevertheless, if something is formally proven correct then for it to be incorrect one of three things must happen: 1) The proof is incorrect (which of course means it is no longer proven) 2) The prover has a bug (most proofs are done automatically). This is possible, but many of the same formal methods are used on the prover, and it is often build on a human-proved proof at the bottom. 3) Mathematics (the whole field) is wrong. This seems unlikely. In reality, the problem with formally verified software is generally that it must interact with non-verified software (and sometimes hardware - although hardware can be verified too). The wikipedia page[1] I referenced is worth reading. [1] http://en.wikipedia.org/wiki/Formal_methods http://en.wikipedia.org/wiki/Formal_methods

josephlord 12y ago
4) It meets the specification but the specification is incorrect/specifies sub-optimal behaviour.
- nl 12y ago
  If you can fix that problem in the general case then you are about to be a very, very rich person.
daveasdf 12y ago
The prover has a bug (most proofs are done automatically). Minor point: while many formal verification projects are proven automatically, seL4 is proven in Isabelle/HOL which is an interactive theorem prover. This means that the proofs are actually carried out mostly manually. (The downside is that it takes much longer to carry out proofs; the upside is that you can prove far more sophisticated properties than is possible with the current state-of-the-art automated provers). You are still right that the proof checker could have a bug, though. Proof checkers tend to be much smaller and simpler than things like SMT solvers, which helps increase confidence in them, however.