seL4
Подробнее
- Создатель
- NICTA (ныне CSIRO Data61)
- Год
- Тип
- Микроядро
- Лицензия
- GPLv2
- Официальный сайт
- sel4.systems
Микроядро семейства L4 с машинно проверенным доказательством того, что его код на C делает ровно то, что сказано в спецификации.
Команда австралийской NICTA опубликовала доказательство в 2009 году: около 8700 строк на C, проверенных в системе доказательств Isabelle/HOL относительно формальной спецификации. Это заняло примерно 20 человеко-лет — раз в двадцать больше усилий, чем написание самого кода. Позднее доказали, что скомпилированный бинарник соответствует исходникам и что ядро обеспечивает изоляцию между компонентами.
Само ядро почти ничего не делает — потоки, адресные пространства, IPC и возможности (capabilities), — а всё остальное работает изолированными процессами в пространстве пользователя. Это подходит системам, где ошибка обходится дороже верификации: в программе DARPA HACMS ядро летало на беспилотном вертолёте, который не смогла захватить «красная команда». Код открыт в 2014 году.