Позволит ли формальная верификация кода микроядра создавать сверхнадежные ОС
В 2015 году американская компания Rockwell Collins совместно с Boeing и 3D-Robotics провела испытания устойчивых ко взлому квадрокоптера Iris и беспилотного вертолёта Little Bird со «сверхнадежной» операционной системой.
Разработка защищённых от взлома дронов ведётся по заказу Агентства перспективных оборонных проектов (DARPA) Министерства обороны США, которое заинтересовано в защите перспективных беспилотных и опционально пилотируемых летательных аппаратах от возможных уязвимостей.
Существует как минимум три способа взлома беспилотных летательных аппаратов: первый — получение доступа к управлению посредством взлома канала связи или подмены данных авторизации, второй — использование уязвимостей программного обеспечения, третий — использование интерфейсов и каналов данных оригинального программного обеспечения для загрузки вредоносного кода.
Разработанная Rockwell Collins операционная система на базе микроядра seL4 устойчива ко всем трём типам взлома. Читать дальше →
Источник: Хабрахабр
