Fwd: [Cryptography] seL4 going open source

====== Forwarded Message ======
Date: 6/24/14 6:43 PM
Received: 6/24/14 1:56 PM -0400
From: [email protected] (ianG)
To: cryptography-of7zbby7T3pWk0Htik3J/[email protected] (Cryptography Mailing List), 
cryptography-JWVWRpNfo5ceIZ0/[email protected] (Crypto discussion list)

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.

...

_______________________________________________
The cryptography mailing list
cryptography-of7zbby7T3pWk0Htik3J/[email protected]
http://www.metzdowd.com/mailman/listinfo/cryptography

====== End Forwarded Message ======
-------------------------------------------------------------------------
Bill Frantz        | Re: Hardware Management Modes: | Periwinkle
(408)356-8506      | If there's a mode, there's a   | 16345 
Englewood Ave
www.pwpconsult.com | failure mode. - Jerry Leichter | Los Gatos, 
CA 95032