праздник пришел на нашу улицу!
Оригинал взят у wizzard0 в праздник пришел на нашу улицу!
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.
- all of the kernel's source code,
- all the proofs,
- other code and proofs useful for building highly trustworthy systems.
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).
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.
This entry was originally posted at http://wizzard.dreamwidth.org/377469.html. It has
comments. Please comment there using OpenID.
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.
- all of the kernel's source code,
- all the proofs,
- other code and proofs useful for building highly trustworthy systems.
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).
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.
This entry was originally posted at http://wizzard.dreamwidth.org/377469.html. It has
comments. Please comment there using OpenID.