General Dynamics C4 Systems и NICTA рады объявить об открытии исходных кодов seL4 — первого в мире ядра операционной системы с доказанной корректностью:
- бинарный код микроядра seL4 правильно реализует поведение, описанное в его абстрактной спецификации;
- данные не могут быть изменены либо прочитаны без разрешения;
- ранее, в 2009 году, разработчиками было доказано соответствие исходного кода ядра, написанного на языке Си, и его спецификации. Теперь же дополнительно показана двоичная корректность.
Исходные коды доступны для широкой публики на GitHub.
>>> Подробности
