[cryptography] seL4 going open source

ianG iang at iang.org
Tue Jun 24 13:43:59 EDT 2014


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


 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.


More information about the cryptography mailing list