[cryptography] seL4 going open source

Kevin kevinsisco61784 at gmail.com
Tue Jun 24 14:33:31 EDT 2014

On 6/24/2014 1:43 PM, ianG wrote:
> http://sel4.systems/
>   General Dynamics C4 Systems and NICTA are pleased to announce the open
> sourcing of seL4, the world's first operating-system kernel with an
> end-to-end proof of implementation correctness and security enforcement.
> It is still the world's most highly-assured OS.
> What's being released?
> It will include all of the kernel's source code, all the proofs, plus
> other code and proofs useful for building highly trustworthy systems.
> All will be under standard open-source licensing terms. More details
> will be posted here closer to the release date.
> When is it happening?
> The release will happen at noon of Tuesday, 29 July 2014 AEST (UTC+10),
> in celebration of International Proof Day (the fifth aniversary of the
> completion of seL4's functional correctness proof).
> ...
> http://sel4.systems/About/
>   What's special about seL4?
> Completely unique about seL4 is its unprecedented degree of assurance,
> achieved through formal verification. Specifically, the ARM version of
> seL4 is the first (and still only) general-purpose OS kernel with a full
> functional correctness proof, meaning a mathematical proof that the
> implementation (written in C) adheres to its specification. In short,
> the implementation is proved to be bug-free. This implies a number of
> other properties, such as freedom from buffer overflows, null pointer
> exceptions, use-after-free, etc.
> 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.
> Furthermore, there are proofs that seL4's specifcation, if used
> properly, will enforce integrity and confidentiality, core security
> properties. Combined with the proofs mentioned above, these properties
> are guaranteed to be enforced not only by a model of the kernel (the
> spec) but the actual binary. Therefore, seL4 is the world's first (and
> still only) OS that is proved secure in a very strong sense.
> Finally, seL4 is the first (and still only) protected-mode OS kernel
> with a sound and complete timeliness analysis. Among others this means
> that it has provable upper bounds on interrupt latencies (as well as
> latencies of any other kernel operations). It is therefore the only
> kernel with memory protection that can give you hard real-time guarantees.
> ...
> _______________________________________________
> cryptography mailing list
> cryptography at randombit.net
> http://lists.randombit.net/mailman/listinfo/cryptography
I think this is great!


More information about the cryptography mailing list