Австралийские ученые создали микроядро операционной системы, отсутствие в
котором различных типов ошибок подтверждено математически. Данная разработка
нацелена на создание "безопасного программного обеспечения беспрецедентного
уровня надежности" для самолетов и автомобилей.
Созданное командой центра NICTA (Information and Communications
Technology Centre of Excellence) микроядро получило название "secure
embedded L4" (seL4). По словам ученых, оно представляет собой первый
"образец ядра операционной системы общего назначения, прошедшего строгую
машинную проверку".
По итогам четырех лет работы было написано и проверено 7500 строк кода на
языке C. В ходе проверок разработчики доказали свыше 10 000 промежуточных
теорем, написав более двухсот тысяч строк четких доказательств, которые затем
были проверены с использованием интерактивной программы Isabelle,
предназначенной специально для доказательства теорем.
Вся эта тяжелая математическая работа означает, что созданное ядро должно
обладать иммунитетом к распространенным типам атак, таким как переполнение
буфера. Данная разработка – пример самых ранних проектов, однако ученые намерены
двигаться дальше.
По словам главного научного сотрудника NICTA доктора Гервина Кляйна, ранее
опыты такого рода были направлены на проверку отдельных компонентов ПО, однако
на этот раз его команде удалось разработать целостную методику проверки общего
назначения, предназначенную для сложного и объемного высокопроизводительного ПО,
чего до этого не удавалось добиться никому.
NICTA планирует передать интеллектуальные права на свою разработку фирме Open
Kernel Labs, которая разрабатывает гипервизоры для виртуализации.
