Re: Fwd: [Cryptography] seL4 going open source

On Thu, 2014-06-26 at 22:33 -0700, Bill Frantz wrote:
> ====== 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.

I think it is not the only one kernel that can give hard real-time
guarantees.

please take a look here http://www.xtratum.org/