[#] Позволит ли формальная верификация кода микроядра создавать сверхнадежные ОС
habrabot(difrex,1) — All
2016-09-29 20:30:04



В 2015 году американская компания [Rockwell Collins][1] совместно с Boeing и 3D-Robotics провела испытания устойчивых ко взлому квадрокоптера Iris и беспилотного вертолёта Little Bird со «сверхнадежной» операционной системой.

Разработка защищённых от взлома дронов ведётся по заказу Агентства перспективных оборонных проектов (DARPA) Министерства обороны США, которое заинтересовано в защите перспективных беспилотных и опционально пилотируемых летательных аппаратах от возможных уязвимостей.

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

Разработанная Rockwell Collins операционная система на базе микроядра [seL4][2] устойчива ко всем трём типам взлома. [Читать дальше →][3]

[1]: https://www.rockwellcollins.com/
[2]: https://sel4.systems/
[3]: https://habrahabr.ru/post/311366/?utm_source=habrahabr&utm_medium=rss&utm_campaign=feed_posts#habracut