Anyone from RTOS community know how this relates to INTEGRITY-178B ?
Sel4: We’re going open source
41–50 of 65 posts
Re: Sel4: We’re going open source
#42"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 fi…
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.
Re: Sel4: We’re going open source
#43Anyone from RTOS community know how this relates to INTEGRITY-178B ?
INTEGRITY-178B and seL4 are not related in terms of their source code or origin, though they do both aim at the same target audience (security and/or safety-critical systems).
I don't have a good knowledge of INTEGRITY-178B, but as far as I can tell some differences are:
* INTEGRITY-178B is a static separation kernel. seL4 can be used as a static separation kernel, but also allows for dynamic systems, for instance with processes being created and torn-down dynamically at run-time;
* INTEGRITY-178B has a proof that a model of the code satisfies particular security properties, while seL4 has a proof that the actual C implementation satisfies particular properties;
* INTEGREITY-178B is certified to EAL6+, while seL4 has not undergone any external certification process. (Without having a good knowledge of EAL6+, my suspicion would be that the code-level aspects of seL4 would meet or exceed EAL6+ certification, while the process-level aspects would need work on the seL4 side.)
If someone has worked with INTEGRITY-178B, please correct me if I have made any mistakes.
Re: Sel4: We’re going open source
#44"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 fi…
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). Th…
4) It meets the specification but the specification is incorrect/specifies sub-optimal behaviour.
Re: Sel4: We’re going open source
#45"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 fi…
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). Th…
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.
Re: Sel4: We’re going open source
#46Earlier quoted context omitted.
Why isn't it already open source? Not sure if you are Australian or not, but - unlike the in the US - in Australia there is no assumption that publicly funded work will be in the public domain. Generally the way it works here is that bodies like Nicta (and CSIRO) are expected to make a return on the investments that are made in them - ie, they are expected to make money somehow. The default way they do that is genera…
Just a little bit more on this: NICTA was originally set up as a research group by the Australian Government with the explicit mandate of commercialising its research. The OKL4 and seL4 microkernels developed by NICTA were commercialised through the company Open Kernel Labs, which was subsequently acquired by General Dynamics (who thus acquired the IP of both projects). At NICTA, we are very happy to see seL4 finally…
Will there be future work with Genode, e.g. is the codebase going to stay focused on ARM or will it also support x86?
Re: Sel4: We’re going open source
#47Earlier quoted context omitted.
Just a little bit more on this: NICTA was originally set up as a research group by the Australian Government with the explicit mandate of commercialising its research. The OKL4 and seL4 microkernels developed by NICTA were commercialised through the company Open Kernel Labs, which was subsequently acquired by General Dynamics (who thus acquired the IP of both projects). At NICTA, we are very happy to see seL4 finally…
Will there be future work with Genode, e.g. is the codebase going to stay focused on ARM or will it also support x86? http://genode.org/documentation/articles/genode-on-okl4
The seL4 kernel currently supports the ARMv6, ARMv7 and x86 architectures, though the proof only applies to ARMv6.
I am not sure what Genode's plans are. seL4 is a different kernel to OKL4, with a substantially different API, so it will be quite some work to move it across from OKL4 to seL4.
Re: Sel4: We’re going open source
#48Earlier quoted context omitted.
Concerning the compiler, in the link it is written: "There is a further proof that the binary code that executes on the hardware is a correct translation of the C code. This means that the compiler does not have to be trusted, and extends the functional correctness property to the binary." (I wonder how that works but it is related to your compiler concern) Now even though the issue of hardware (say rogue hardware wi…
On that note: what even is a correct translation of C when it has so many undefined behaviors in it's spec.
They use a formally-specified subset of C described in Harvey Tuch's PhD thesis: http://www.ssrg.nicta.com.au/publications/papers/Tuch:phd.pd...
Re: Sel4: We’re going open source
#49Does "end-to-end proof of implementation correctness and security enforcement" mean there is zero change of a bug or security flaw?
Re: Sel4: We’re going open source
#50Anyone from RTOS community know how this relates to INTEGRITY-178B ?
INTEGRITY-178B and seL4 are not related in terms of their source code or origin, though they do both aim at the same target audience (security and/or safety-critical systems). I don't have a good knowledge of INTEGRITY-178B, but as far as I can tell some differences are: * INTEGRITY-178B is a static separation kernel. seL4 can be used as a static separation kernel, but also allows for dynamic systems, for instance wi…
Thank you for responding that is a good description.
I remember someone from one of the government agencies gave a talk at in college many years ago about INTEGRITY-178B and about this separation kernel idea.
That was maybe 7-10 ago. The idea was pretty neat. And the claim was that the future will belong to more secure OSes based on this separation kernel (microkernel?). And how say every little component -- memory, filesystem, mouse, display are all in userspace. He talked about ok general purpose computer at that time were too slow to operate in that way (so Linux was better and winning because of performance). But just wait some 10 years or so and machines will be so fast that it won't matter.
So since then that story kind of stuck with me that kind of prompted the question.