Log in

No account? Create an account
Previous Entry Share Next Entry

праздник пришел на нашу улицу!


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 comment count unavailable comments. Please comment there using OpenID.

  • 1
maxim June 24th, 2014
Нихуя Себе.

vp June 24th, 2014
оно ж широких масс не коснется, или?

wizzard0 June 24th, 2014
Гипервизор, а в него хоть венду, хоть Erlang-on-Xen, хоть что. Праздник на улице амазона, как минимум.

soonts June 25th, 2014
Мне кажется в обозримом будущем не взлетит.

Современный hardware-assisted hypervisor это совсем немного строк кода, которые вполне можно отладить и протестировать традиционными методами.

Я что-то не слышал ни одного случая, когда бы кто-то убегал из песочницы амазонового Xen-а.

wizzard0 June 25th, 2014
> ни одного случая
рабочие эксплоиты есть, и далеко не один
вот например


праздник пришел на нашу улицу!

livejournal June 24th, 2014
Пользователь sergey_cheban сослался на вашу запись в своей записи «праздник пришел на нашу улицу!» в контексте: [...] Оригинал взят у в праздник пришел на нашу улицу! [...]

Ivan Appel June 25th, 2014
А как в этом контексте правильно понимать фразу "compiler doesn't have to be trusted"?

wizzard0 June 25th, 2014
Бинарники (по семантике ARM ISA, не уверен насчет x86) тоже proof-checked.

  • 1