В 2015 году американская компания Rockwell Collins совместно с Boeing и 3D-Robotics провела испытания устойчивых ко взлому квадрокоптера Iris и беспилотного вертолёта Little Bird со «сверхнадежной» операционной системой.
Разработка защищённых от взлома дронов ведётся по заказу Агентства перспективных оборонных проектов (DARPA) Министерства обороны США, которое заинтересовано в защите перспективных беспилотных и опционально пилотируемых летательных аппаратах от возможных уязвимостей.
Существует как минимум три способа взлома беспилотных летательных аппаратов: первый — получение доступа к управлению посредством взлома канала связи или подмены данных авторизации, второй — использование уязвимостей программного обеспечения, третий — использование интерфейсов и каналов данных оригинального программного обеспечения для загрузки вредоносного кода.
Разработанная Rockwell Collins операционная система на базе микроядра seL4 устойчива ко всем трём типам взлома. Операционная система на базе seL4 изначально ориентирована в первую очередь на безопасность. По-английски это называется красивым словосочетанием «hackproof» (взломоустойчивая).
Её особенностью является устойчивое к подменам кода ядро, которое использует математические алгоритмы и контрольные суммы для проверки запущенных служб, а также обеспечивает раздельное выполнение процессов.
Система позволяет запустить виртуальную машину, в которой гостевая программа не получает доступа к основным процессам или аппаратной части. При запуске программы сообщают ядру контрольные суммы, на основе которых производится исправление ошибок или закрытие несанкционированных процессов.
Испытания прошли успешно: специалистам по кибербезопасности не удалось запустить вредоносный код на беспилотных аппаратах с защищённой операционной системой, а также перехватить управление дроном или вызвать системный сбой.
Микроядро seL4 используется не только в авиации, но и в медицине, финансовом секторе, энергетике и других областях, где необходима гарантия отсутствия сбоев.
Важная особенность архитектуры seL4 — вынос частей для управления ресурсами ядра в пространство пользователя и применения для этих ресурсов тех же средств разграничения доступа, что и для ресурсов пользовательских. Микроядро не предоставляет готовых высокоуровневых абстракций для управления файлами, процессами, сетевыми соединениями и так далее.
Вместо этого оно предоставляет лишь минимальные механизмы для управления доступом к физическому адресному пространству, прерываниям и ресурсам процессора.
Высокоуровневые абстракции и драйверы для взаимодействия с оборудованием реализуются отдельно — поверх микроядра в форме задач, выполняемых на пользовательском уровне. Доступ таких задач к имеющимся у микроядра ресурсам организуется через определение правил.
Для программистов существует компоненто-ориентированная платформа разработки приложений CAmkES, позволяющая моделировать и создавать системы на основе seL4 в виде коллекции взаимодействующих между собой компонентов.
С seL4 генетически связан проект L4.verified — формально верифицированное ядро на архитектуре L4.
L4 — микроядро второго поколения, разработанное Йохеном Лидтке в 1993 году.Архитектура микроядра L4 оказалась успешной. Было создано множество реализаций ABI и API микроядра L4. Все реализации стали называть «семейством микроядер L4». Так появился и seL4. А реализация Лидтке неофициально была названа «L4/x86».
Основная идея L4.verified, как и seL4, – математически доказать корректность реализации ядра. Дело в том, что микроядра в отличие от монолитно-модульных монстров типа GNU/Linux, весьма миниатюрные по размеру. А раз так, то они могут быть формально верифицированы. Каждой строчке кода ставится в соответствие математическое утверждение, которое нужно доказать.
В микроядре L4.verified доказывается соответствие реализации модели, отсутствие вечных циклов и еще некоторых вещей. Стоимость этого исследования составила порядка $6 миллионов, а проект длился 7 лет. Объем работы достиг 25 человеко-лет.
Помимо своего основного применения (безопасность, как и у seL4) L4 используется и в других сферах. Так, фирма Qualcomm запустила реализацию микроядра L4, разработанную фирмой NICTA, на наборе микросхем, называемом «Mobile Station Modem» (MSM). Об этом в ноябре 2005 года сообщили представители фирмы NICTA, а в конце 2006 года наборы микросхем MSM поступили в продажу. Так реализация микроядра L4 оказалась в сотовых телефонах.
Вопрос создания сверхнадежного ПО стал особенно актуальным, когда подавляющее большинство приложений стало работать в сети и оперировать с большим количеством данных. А данные эти зачастую конфиденциальны.
В сети не так много материалов о роли формальной верификации в создании сверхнадежных ОС. Еще меньше обстоятельных дискуссий. Поэтому ниже приведем основные мысли и аргументы одной из бесед по поводу статьи на эту тему:
- Распространение средств верификации и грамотное их внедрение позволит избавиться от целого класса ошибок в любом программном обеспечении. Например, такая ошибка, как «переполнение буфера», может быть предотвращена, если достаточно просто организовать проверку необходимых параметров.
Баги там все-таки есть, делает вывод один из комментаторов, ссылаясь на этот материал.
- Утверждается, что код seL4 обладает некоторой степенью надежности. Если создание абсолютно защищенной от взлома ОС – утопия, то почему этим продолжают заниматься такие крутые команды, как DARPA?
- Что будет, если хакеры подсунут туда верифицированный код? Или это невозможно? Почему во всех ОС есть баги, которые обязательно могут использовать хакеры?
- Почему верификация кода обязательно должна быть связана с защитой от взлома? Что, проще нельзя? Верификация кода и защита от взлома – это две разные задачи, которые всего лишь иногда пересекаются.
Трояны, кибервымогательство, фишинг, кликджекинг – это виды атак, которые работают независимо от наличия ошибок в программном коде приложений или операционной системы в целом. А если пользователи выбирают слабые пароли? Это тоже вина разработчиков ПО?
- Эксперимент расходится с реальностью, так как доступ, который дали хакерам исследователи, в жизни им никто не откроет. В таких системах просто нужно внимательно следить за тем, чтобы запрещать вставлять код всем, кроме администратора.
- Надо же! Хорошо написанные и протестированные приложения очень трудно взломать. Кто бы мог подумать… Вообще-то, программный код и так состоит из математически верифицированных конструкций.
- Разработка верифицированного кода – роскошь, которую могут позволить себе немногие. А его сопровождение и постоянное внесение изменений – еще большая роскошь.
- С точки зрения менеджмента, программисты часто ведут себя биполярно. Когда их просишь разбить большую задачу по разработке на подзадачи, они легко соглашаются. Но когда предлагаешь им заранее подумать над возможными ошибками и планомерно их предотвращать – реакция совсем другая: «это непрактично», «всего не предусмотришь», «а как же то?», «как же это?»… Далеко не все хотят думать о качестве кода заранее.
- А что делать, если средства верификации сами содержат ошибки? Кто будет верифицировать верификаторы?
- В чистой математике нет «багов». Если есть правило, что делить на ноль нельзя, значит, случаи, когда в знаменателе оказывается ноль, просто не рассматриваются. В реальной жизни этот прием не работает. Если речь идет о разработке ПО, то там приходится работать даже с теми значениями, которые программе «не нравятся». Результат от деления на ноль – это бесконечность. И с ней нужно что-то делать, а не заявлять, что такого результата не может быть.
P.S. Конечно же, дискутировать можно бесконечно. Но если такие крупные организации, как DARPA, делают конкретные шаги по реализации этих проектов, за этой историей как минимум стоит последить и как максимум — поучаствовать.
Исходный код seL4 все еще доступен на GitHub.
Комментарии (27)
sshikov
29.09.2016 19:35Тема защиты каналов данных нифига не раскрыта. Скажем, если мы поддерживаем обычный протокол типа SSL, и в нем найдены какие-то уязвимости by design — у нас в ОС они тоже есть? А если нет — то как верифицированное микроядро от них защитит?
Кроме того, слабое место всех без исключения подобных проектов — это периферия вообще. Т.е. грубо говоря, как только у вас появились устройства — у вас появились драйвера. Драйвера в пользовательском пространстве ограничены, потому что переключение контекста — иногда слишком дорогая штука, чтобы часто позволять ее себе.
А драйвера в пространстве ядра, с привилегиями ядра — это дырища, и это так во всех системах. Исключениями являются разве что системы типа IOS — у которых фактически не бывает сторонней периферии. Кроме того, нынешние железяки сами по себе содержат кучу закрытого софта.
Т.е., можно сделать сверхнадежную ОС — но она будет ограничена поддержкой узкого набора периферии, и плохой совместимостью с внешними системами. Как-то так.
rumkin
29.09.2016 21:23Ну, в сверхнадежных ОС нуждаются организации, которые вероятнее всего заказывают переферию. И это лишь вопрос времени, когда появится необходимое количество переферии для комфортабельного персонального использования.
sshikov
29.09.2016 21:36+1Так это не вопрос. Вопрос в том, что это (т.е. верификацию кода ядра) нельзя рассматривать как технологию, которая позволить достичь безопасности массово.
Периферия — вопрос времени? А ничего, что производителей некоторых видов периферии считанное число в мире вообще? Т.е. например, типовой HDD или SSD, или видеокарта содержат внутри гигабайты кода, который никем не верифицирован, который вообще никто не видел, и при этом он имеет доступ ко всему железу (например к памяти, потому что архитектура-то компьютера у нас все равно может быть обычная, например x86). А ОС для дронов — почему нет, можно наверное.
leotsarev
30.09.2016 17:04Драйвера в пользовательском пространстве ограничены, потому что переключение контекста — иногда слишком дорогая штука, чтобы часто позволять ее себе
У L4 нет драйверов в ядре. У нее даже диспетчера памяти в ядре нет. Ядро в L4 сверхмаленькое, такие ядра даже называются наноядрами (чтобы отличать от микроядер, подобных Mach, которые по сравнению с L4 просто гиганты).
И переключение контекста в L4 на порядок или на два порядка дешевле мейнстримных ОС. Пересылка данных между процессами может быть в режиме «взял страницу памяти, убрал из памяти 1 процесса, заммэппил другому».
sshikov
30.09.2016 17:26Дешевые переключения это хорошо. Впрочем, то про что я писал, это как правило нужно только в ограниченных случаях, типа гигабитных потоков данных. С остальными должны справляться более традиционные решения.
bARmaleyKA
02.10.2016 23:49Искал ссылку на статью на канувшей в лета Компьюленте, увы не нашёл. Там разработчики этой операционки рассматривали вариант, если так можно сказать, установки драйверов в систему на основании теории игр. В черне — ядро системы должно было опрашивать новый девайс и уже на основании ответов от него формировать драйвер для этого устройства. К сожалению, ссылки нет для полного описания.
Saffron
29.09.2016 19:49+1> В чистой математике нет «багов». Если есть правило, что делить на ноль нельзя, значит, случаи, когда в знаменателе оказывается ноль, просто не рассматриваются.
От вас несёт уринотерапией и прочим ГМО. Математика никогда не отказывается рассматривать все возникающие случаи. Просто она рассматривает специальные случаи отдельно. Вы ещё скажите, что математика не умеет оперировать полем характеристики 2. Ещё как умеет, просто этот случай описан отдельно, а для множества других теорем внесён как исключение. И так везде.ZyXI
30.09.2016 01:14+1Это не так, все математические операции определены на некоторых множествах. Если вы видите «деление на ноль» как специальный случай, то вы определяете деление так, что второй операнд должен принадлежать множеству, включающему в себя ноль.
Отсутствие определения деления на ноль в ряде случаев — это явление того же порядка, как отсутствие определения деления, к примеру, на поле. Вот у нас есть поле
?(в котором, кстати, деление на ноль не определяется) и с ним мы можем написатьa/bи что?то с этим делать дальше. К вам пришёл студент и написалa/?. Значит ли это, что вам внезапно нужно начать рассматривать «специальный случай» «деление числа на поле», добавив его во все теоремы, где вы что?то на что?то делите или нужно послать такого человека куда подальше, потому что поле?не входит в множество рациональных чисел, на котором у вас определено деление (кроме деления на ноль, которое не определено вполне себе официально)?Saffron
30.09.2016 03:21+1математика — это не про написать формулы, а про сформулировать теоремы. Если студент даст валидное описание для объектов a/? и оно будет рождать интересные и нетривиальные утверждения, то почему бы не рассматривать и это обозначения?
ZyXI
30.09.2016 10:32Но пока студент не дал «валидное описание для объектов
a/?» эта ситуация именно что «просто не рассматривается». И с делением на ноль то же самое: оно может быть не определено и, соответственно, не рассматриваться. Возможно, это приведёт к возникновению специального случая в другом месте (пример: решениеa * x = b, когдаa = 0: мы не будем рассматривать неопределённоеb / a, мы скажем, что еслиa = 0, тоx— любое число, еслиb = 0и укажем на отсутствие решения, когдаb ? 0), возможно мы доопределим операцию деления, но случай за границами области определения рассматриваться не будет.Saffron
04.10.2016 00:08+1Вы явно не видели математиков за работой. Зачем вообще деление? Допустим, мы решаем СЛАУ. Что является решением? Назвать множество значений переменных, удовлетворяющих системе. Мно-жес-тво! Оно может быть пустым, если система несовместна, как например, будет 0*x = 2. Может содержать единственное решение, может содержать целое линейное подпространство решений. В отличие от вас, математики держат свой ум в строгости и всяческие неоднозначности явно разрешают.
Кстати, они ещё и подстраиваются под разные применения. Если ожидается постоянное деление на ноль, то они готовы ввести теорию, которая будет разделять разные типы возникающих в задаче нулей, задействуют более сильные абстракции вроде актуальных бесконечно малых и неархимедовы поля.
Математический подход в корне отличается от того, что вы написали — давайте сделаем какую-нибудь запись алгоритма, и проигнорируем все возможные ошибки выполнения. В математике записи и формулы ничего не стоят, если за ними не стоит какой-то теории, доказательств существования и корректности объектов, упомянутых в этих записях. Написать (назвать) можно всё что угодно, хоть треугольник с четырьмя углами. Объектом рассмотрения математики эта бессмыслица не станет.
Andriyevski
29.09.2016 22:11-2Лично мое мнение, такой адский невроз от компании создавшей и обсуживающий данный дрон есть только в том случае, если сходный код или его части попали в чужие руки и компания стараеться всеми силами выправить ситуацию до здачи дрона в експлуатацию заказчику, дёргая за сиськи такие серьезные компании кака Boeing и DARPA!
Скорее всего кодом или частью когда кто то уже располагает, иначе они б не офишировали то что пробуют создать самую крутую для дронов ОС или исправить уязвимости коих нет, как выходит из статьи тем более что услуги данных компаний стоят как ВВП некоторых стран!
Если ее действительно тестили то ошибки точно были найдены и убраны, так как никто не будет писать что в дронах специального(военного) назначение нашли уязвимости… кто их купит после того ?)
2.Теперь тупая идея с ПЗУ от third112:
(ПЗУ) предназначены для постоянного хранения информации, которая записывается туда при изготовлении и не подлежит изменению. Следовательно, прочитать эту информацию можно, а изменить нельзя. Даже при выключении питания информация в ПЗУ остается, в этом состоит отличие ПЗУ от ОЗУ. — Отличный повод сбить дрон, снять ПЗУ считать все ПО и дизесимблировать или изменить под себя! Поверте самый тугой способ защиты!
Для разницы и контраста:
(ОЗУ) предназначены для записи, хранения и считывания информации при запуске и работе системы;
При выключении питания вся информация из ОЗУ разрушается. — следовательно противник может похвастаться что у него есть чистый ОЗУ отжатый у дрона на котором нифига нет :)Karpion
29.09.2016 23:52+12. Если ПО системы не открытое, то такому ПО доверять не следует, за исключением особых случаев. А если ПО открытое — то сбивать дрон нет смысла.
Вопрос в том, является ли дрон тем случаем, когда надо закрыть ПО. Ну, наверно, закрыть его от произвольного доступа — надо: доступ д.б. только у тех, кто разрабатывает дрон. Осталось понять, сколько людей будут иметь доступ к ПО, и какова вероятность того, что ПО утечёт через одного из людей, имеющих доступ.
Если ПО дрона в ОЗУ, то как оно там окажется? Заливать его туда перед запуском?
Кстати, интересная идея. Ведь задачу (координаты цели) всё равно надо будет заливать.Andriyevski
30.09.2016 00:031.Если дрон над охраняемой територией то смысл сбить есть еще какой, не теребить же флашками ему что мол проход закрыт, ты нарушил воздушное пространство)))
2.ПО для военных разработок — сугубо закрытое, глупо спорить почему оно не должно быть ОПЕН СОРС)))
3.Есть смысл заливать через каналы, так как он будет заточен именно под конкретные задачи и например набор программ для операторов дрона будет сугубо для выполнения миссии! Не нужно знать операторам всевозможные программы и интерфейсы дрона (я в том смысле на заданиях, что бы не отвликать внимание и не иметь возможность превышать полномочия)bARmaleyKA
02.10.2016 23:542.ПО для военных разработок — сугубо закрытое, глупо спорить почему оно не должно быть ОПЕН СОРС)))
Они уже года два как полностью открыли код операционки https://www.opennet.ru/opennews/art.shtml?num=40297
third112
30.09.2016 03:58Если ПО дрона в ОЗУ, то как оно там окажется? Заливать его туда перед запуском?
Такой метод очень уязвим. Если в дроне стоит носитель информации, нпр., HDD или ПЗУ, то бортовой компьютер можно сделать в виде единого невскрываемого блока залитого эпоксидкой, с устройством саморазрушения. В этом случае у технического персонала, обслуживающего дрон, не будет возможности скопировать систему. А если заливать систему с компа перед запуском, нпр., через USB, то оператор-шпион может легко записать ее на флешку с минимальным риском для себя.
third112
30.09.2016 03:28Отличный повод сбить дрон, снять ПЗУ считать все ПО и дизесимблировать или изменить под себя!
Чтобы секретная информация не попала в руки противника борт снабжают системой саморазрушения. Если не весь дрон, то ПЗУ разрушить не так уж сложно. Зачем читать ПЗУ? Чтобы сделать копию дрона? У противника для этого должен быть неслабый индустриальный уровень. Но учитывая нарастающую скорость прогресса подобное копирование становится все более и более сомнительным — пока противник делает копию, появятся более совершенные дроны и копия окажется устаревшей. Если я правильно понял статью, речь идет о другой защите — о защите от перехвата управления дроном в полете, когда противник по каналам связи внедряет в систему свои компоненты. В ПЗУ такое внедрение невозможно. ОЗУ уязвимо не только внедрением осмысленного кода, но, что гораздо проще сделать, внедрением случайного кода, который просто нарушит работу системы и дрон упадет. Если дрон сбит и попал в руки противника источник питания (а значит и информация в ОЗУ) может уцелеть. Если противнику так нужна система дрона, то он будет сбивать так, чтобы ОЗУ и питание уцелели, нпр., стрелять по винтам и двигателям, но не по корпусу. ИМХО над этими вопросами не могли не думать разработчики и если они не использовали столь простое и очевидное решение, как ПЗУ, значит на это есть веские основания. К сожалению, статья их не приводит.
third112
30.09.2016 03:38Небольшое уточнение:
(ПЗУ) предназначены для постоянного хранения информации, которая записывается туда при изготовлении и не подлежит изменению.
Само ПЗУ (микросхему) обычно делают на заводе пустой. А зашить туда инфу можно где угодно (хоть в полевых условиях) для этого нужен ПК с картой программатора. Столь же просто, как DVD-R прожечь.
PaulAtreides
29.09.2016 23:52+3Формальная верификация это проверка соответствия алгоритма его математической модели. Она с некоторой (высокой) вероятностью защищает от уязвимостей в реализации, но от уязвимостей в самом алгоритме она помочь не в состоянии.
Кстати, я совершенно не понимаю, зачем тут приведено три «типа атак». Все они сводятся к «уязвимостям в ПО».third112
30.09.2016 04:36Если говорить о мат.модели отдельного алгоритма, нпр., алгоритма перемножения двух матриц, то построение такой модели особых проблем обычно не вызывает. А вот построение полной мат.модели ОС представляется трудновыполнимым, если вообще выполнимым. Тут, видимо, нужно говорить о наборе моделей, с неизбежными в этом случае конфликтами между ними. Не уверен, что даже микроядро (о котором говорится в статье) возможно адекватно смоделировать. Будет ли модель адекватной без моделирования CPU? — О проблеме моделирования CPU писал такой лидер, как Интел в своих публикациях.
Т.о. ИМХО можно говорить только о частичной и очень ограниченной верификации.bARmaleyKA
02.10.2016 23:58Т.о. ИМХО можно говорить только о частичной и очень ограниченной верификации.
Они вначале нашли способ формального подтверждения 100% отсутствия ошибок в программе http://www.opennet.ru/opennews/art.shtml?num=23011third112
03.10.2016 08:37Спасибо за ссылку, но это предварительное сообщение, в котором предпоследняя фраза:
Полное изложение работы исследователей будет озвучено на 22-ом симпозиуме, посвященном принципам работы операционных систем (SOSP).
Год сообщения 2009. Работу признали?
Работой по формулировке алгоритма математического доказательства в течение четырех лет занималась команда из 12 исследователей NICTA, аспирантов и техников. Они успешно проверили более 10 тыс. промежуточных теорем, изучив более чем 200 тыс. строк кода.
При таких объемах возникают большие сомнения.
Falstaff
30.09.2016 14:54Обычно под формальной верификацией понимают скорее проверку соответствия формальной модели (не конкретной конечной реализации) некоторым требованиям (например, нет гонок, нет бесконечных циклов, нет выходов за границы массивов и так далее). То есть, например, я пишу некий алгоритм, и хочу формально доказать, что он ни при каких условиях — любые комбинации собственного состояния, входных данных, переключений контекста потоков — не сможет писать/читать не свою память, не зависнет, всегда выполнится за ограниченное количество шагов… вот такого плана задачи. Хотя, судя по их публикациям, корректность реализации они тоже проверяли.
mikolalex
30.09.2016 00:24реакция совсем другая: «это непрактично», «всего не предусмотришь»
А ведь так и есть, собственно, из идеи «всего не предусмотришь» и выросла философия аджайл. Другое дело, когда программисты просто ленятся или не могут(в силу неразвитости абстрактного мышления) качественно продумать концепцию во всех аспектах перед реализацией. То есть им, грубо говоря, проще сначала вырыть траншею, а потом уже посмотреть, ровная ли она и подровнять(или подг***ять), если не очень. Работаю в среднестатистической веб-конторе, таких большинство.
third112
Если я правильно понял, то описанная система (в том числе и микроядро) грузятся в ОЗУ. Если говорить только о дронах, то в этом случае можно достичь неизменность микроядра системы гораздо проще и надежнее: зашить его в ПЗУ. Серьезный минус такой системы — для обновления нужно физически менять ПЗУ, в случае дрона не существенен — если дрон в полете обновлять микроядро не нужно.
bARmaleyKA
Давным давно существуют перепраграммируемые ПЗУ — предшественники флэш памяти.
third112
Да. Я знаю. ИМХО в случае дрона лучше использовать ПЗУ, а не ППЗУ. Но это не столь важно.