seL4

0
Ваша оценка: Нет

seL4 — первое в мире ядро операционной системы с доказанной корректностью.

Принцип работы платформы сводится к полной изоляции работы групп приложений за счёт использования низкоуровневого гипервизора, задачи которого выполняет микроядро seL4. В отличие от классических систем виртуализации, микроядро seL4 является предельно минималистичным и его надёжность доказана математически.

  • бинарный код микроядра seL4 правильно реализует поведение, описанное в его абстрактной спецификации;
  • данные не могут быть изменены либо прочитаны без разрешения;
  • ранее, в 2009 году, разработчиками было доказано соответствие исходного кода ядра, написанного на языке Си, и его спецификации. Теперь же дополнительно показана двоичная корректность.

Сайт разработчика: http://ssrg.nicta.com.au/software/TS/seL4/
Страница приложения на: https://github.com/seL4/l4v
Что почитать?


Разместил: vikos 1 Август 2014 в 21:10