Австралийские ученые создали микроядро с формально подтвержденным уровнем защиты

Австралийские ученые нашли способ формального доказательства отсутствия ошибок в ядре операционной системы. Согласно их заявлению, это первый случай, когда удалось математически строго показать корректность ядра для операционных систем общего назначения – ранее подобные проверки осуществлялись только для небольших ядер, пригодных только для теоретических исследований.

Ядро seL4 (secure embedded L4), которое первым прошло формальную проверку защищенности, создано в австралийской частной исследовательской организации NICTA. В разработке ядра, состоящего из 7500 строк на языке C, и методов доказательства его корректности также приняли участие сотрудники университета Нового Южного Уэльса (Австралия). Вдобавок к этому, сама методика проверки корректной работы ядра основана на технологии Isabelle, которую Лоуренс Полсон (Lawrence Paulson), профессор вычислительной логики из Кембриджского университета (Великобритания), разработал для проверки корректности программ общего назначения.

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

Следует заметить, что формальной проверкой программных систем занимаются множество научных коллективов в разных странах мира. Например, в Германии подобную задачу решает проект Verisoft. Новизна разработок NICTA заключается в отходе от традиционной методики формального подтверждения конкретных свойств системы на примере отдельных фрагментов ядра. В новой работе используется методика генерализованного, универсального доказательства корректной реализации всех заявленных в системе функций.

Благодаря новой методике проверки корректности новое ядро seL4 для встраиваемых систем устойчиво к большинству известных видов атак, в том числе к атакам на переполнение буфера, как утверждают разработчики. Работа над этим ядром и критериями формальной проверки заняла четыре года, а результаты переданы фирме Open Kernel Labs, специально созданной для дальнейшего развития этих результатов и создания защищенных ядер и микроядер для критически важных систем.

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