[Перевод] Микроядро seL4. Формальная верификация программ в реальном мире

Научная статья опубликована в журнале Communications of the ACM, октябрь 2018, том 61, номер 10, стр. 68−77, doi: 10.1145/3230627

В феврале 2017 года со взлётной площадки «Боинга» в Аризоне поднялся вертолёт с обычным заданием: облёт ближайших холмов. Он летел полностью автономно. Согласно требованиям по технике безопасности Федерального управления авиации США, пилот не прикасался к органам управления. Это был не первый автономный полёт AH-6, которого в компании называют Беспилотной Птичкой (Unmanned Little Bird, ULB). Он так летает уже много лет. Однако на этот раз посреди полёта вертолёт подвергся кибератаке. Бортовой компьютер атаковало вредоносное программное обеспечение видеокамеры, а также вирус, доставленный через заражённую флэшку, которую вставили во время техобслуживания. Атака поставила под угрозу некоторые подсистемы, но не смогла повлиять на безопасную эксплуатацию воздушного судна.
Читать дальше →

Источник: Хабрахабр

Перейти на сайт

Похожие новости

• Что делать, если ваш слон думает, что он баг?
• Как не потерять свои контейнеры у себя в инфраструктуре?
• Киберугрозы в первом полугодии 2025 года: анализ векторов атак на облачные и гибридные инфраструктуры
• Лицо, голос и тело по-датски
• Все тонкости GPG подписей
• Половина работающих в найме россиян хотят уйти в собственный бизнес в ближайшие два года
• «Сделано в России»: цифровые экосистемы МАЕР получили сертификат РЭЦ
• Бренд как медиа: что меняется, когда компания становится источником смыслов
• Foreman в изоляции: как мы построили отказоустойчивую и безопасную систему для массового деплоя ОС
• Пароли не там, где вы их оставили. Как работает DOM Clickjacking