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

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

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

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

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

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

• [Перевод] Как забытый парсер ссылок привел к XSS на Reddit: Уязвимость на $5000, которая скрывалась в редакторе постов Reddit
• AlinaTen: Сделка между OpenAI и Windsurf сорвалась — глава стартапа уходит в Google
• Kubernetes на базе Deckhouse в облаке Linx Cloud: встроенный мониторинг, безопасность и управление сертификатами
• Без(д)воз(д)мездно, то есть даром
• Настраиваем роутер и WiFi с VLAN в тоннель
• Новости кибербезопасности за неделю с 7 по 13 июля 2025
• Vladimir: TSMC может понести убытки из-за возможных пошлин США на тайваньские чипы
• VLESS+Reality и Multi-hop: Архитектура VPN-цепочки для нового поколения блокировок
• Laravel: электронная подпись на сервере с PDF визуализацией
• Perplexity запускает Comet — собственный AI-браузер, бросающий вызов Google