Австралийское национальное исследовательское агентство Data61 представило результат своей длительной разработки — самый защищенный дрон в мире. Таким его делает лежащая в основе аппарата уникальная операционная система seL4, оптимизированная для максимальной безопасности. Она была создана для использования в защищенных системах самого широкого спектра — от бортовых компьютеров самолетов до автоматизированных промышленных комплексов.

В 2009 году австралийские исследователи сумели математически доказать, что seL4 в любых обстоятельствах будет работать в соответствии со строгими спецификациями — этот принцип носит название "формальная верификация". Это математическое доказательство демонстрирует, что seL4 не содержит в себе ни единой программной уязвимости. Ее особенность заключается именно в строгом следовании заложенным в нее указаниям. Другими словами, если в спецификации не указано переполнение буфера (распространенная программная уязвимость), система никогда не вызовет переполнение буфера.

Микроядро seL4 (фактически центральный базовый код операционной системы) имеет строгое разделение критических и некритических функций. Благодаря этому, если хакеру-злоумышленнику удастся взять под контроль запущенное в ОС приложение, все остальные части системы останутся для него полностью недоступны.

Однако безопасность микроядра seL4 все же может быть скомпрометирована. Так, например, это может произойти, если аппаратная платформа, на которой работает ОС, содержит глубоко интегрированный шпионский код (бэкдор) или имеет другие программные уязвимости.

"Мы ничего не можем поделать с аппаратным бэкдором, — поясняет лидер исследовательской группы Data61 Trustworthy Systems Гервин Кляйн (Gerwin Klein). — В конце концов, если вы не можете доверять аппаратной части своей системы, с этим невозможно что-либо сделать".

Data61 работает в тесном контакте с американским агентством DARPA для полевых испытаний своей системы. В прошлом году seL4 была установлена на вертолет Boeing "Little Bird" для проведения тестов на возможность его взлома во время полета. Эти испытания доказали, что ни одну критическую систему геликоптера под управлением австралийской ОС взломать невозможно.

Помимо очевидного военного использования, микроядро от Data61 может найти применение в целом ряде сфер промышленности, где требуются высокозащищенные системы. ОС seL4 была выпущена в качестве опенсорсного программного обеспечения два года назад, а потому доступна всем желающим. Основными кандидатами на ее применение являются производители автомобилей и другой транспортной техники. Так, например, в середине прошлого года исследователи Чарли Миллер и Крис Валасек нашли уязвимость в блоке телематики, которая позволяла взять под контроль тормоза Jeep Cherokee. После этого концерн Fiat Chrysler был вынужден отозвать 1,4 миллиона автомобилей до полного устранения опасности.

На текущий момент агентство DARPA уже выдало ряд грантов небольшим компаниям на применение seL4. Однако до ее появления на рынке может пройти еще несколько лет. Поскольку микроядро лежит в самой основе продукта, может уйти до пяти лет на завершение его разработки.

Очищающая салфетка

Электрообогреватель