Влітку 2015 року команда хакерів, найнятих військовими, спробувала перехопити контроль за безпілотним гелікоптером Little Bird виробництва Boeing. На момент початку операції хакери вже мали частковий доступ до комп’ютерної системи дрону. Їм потрібно було лише зламати технологію управління польотом, встановлену на самому пристрої, щоб повністю перехопити керування.
Зазначимо, що інструменти угрупування Red Team надавали змогу так само легко втрутитись в керування гелікоптером, як і в будь-яку домашню WiFi-мережу. Якби до цього інженери DARPA не вбудували в «пташку» новий вид захисного механізму — програмне забезпечення, яке блокує спроби перехоплення управління гелікоптером. Red Team мала цілих 6 тижнів і навіть доступ до комп’ютерної мережі дрону, щоб зламати його, але так і не пробилась через захист Little Bird.
Кейтлін Фішер (Kathleen Fisher), професор комп’ютерних наук з Університету Тафтса та менеджер проекту HACMS (High-Assurance Cyber Military Systems), пояснює важливість показового експерименту з гелікоптером:
— Спеціалісти могли використовувати будь-які свої інструменти, мали внутрішній доступ, однак, їм не вдалось перехопити гелікоптер. Тому, в DARPA можуть із впевненістю заявляти: вони винайшли технологію, яка насправді захищає систему від зламу. Тепер можна встановлювати її в найважливіших військових розробках.
Технологія, що не піддалась хакерам, відома серед спеціалістів як формальна верифікація. На відміну від більшості програмних кодів, які базуються лише на принципі, працює чи не працює програма, формальна верифікація використовує математичний принцип доказів. Кожне положення логічно слідує з попереднього, а вся програма може бути протестована за тією ж схемою, яку використовують математики для доведення теорем. «Ви пишете математичну формулу, яка описує задану роботу програми і використовуєте певний інструмент, який дає змогу перевірити правильність такого твердження», — пояснює Брайан Парно (Bryan Parno), який проводить дослідження систем формальної верифікації в Microsoft Research.
Інженери прагнули створити програму з формальною верифікацією практично від самого початку розвитку комп’ютерних наук. Довгий час вважалось, що винайти спосіб для побудови такого ПЗ неможливо, однак за останнє десятиріччя т.з. «формальні методи» активно розвивались і тепер наблизились до практичного використання. Сьогодні експерименти з подібними технологіями проводяться в найкращих умовах. Примітно, що для належної фінансової та ресурсної підтримки об’єднались суперники ринку: військові США та IT-сектор, представлений, зокрема, Microsoft й Amazon.
Blog Imena.UA за матеріалами: Quanta Magazine
ТВОРЧІ КОНКУРСИ
Також цікаво і корисно: міжнародні фахові двотурові конкурси талантів:• Конкурс Алея Зірок
• Конкурс Сузір’я Україна-Європа
• Конкурс Зірки Європи | Stars of Europe
• Конкурс Сила Музики | The Power of Music
• Конкурс Constellation: World Vision
• Конкурс Майстер Концерт | Master Concert
• Конкурс New York Starlights
• Конкурс London Stars
• Конкурс Tokyo Art Ninja
• Послуга для творчих людей: Новини і статті про вас
Курс підвищення кваліфікації вчителів на 60 годин: "Музична освіта і музична індустрія: Україна, Європа, світ" ↓
Музика:
Я відчувала те саме
Дівчинка з Місяця
→ Купити якісний трек Girl from the Moon
Ти зруйнував
→ Купити якісний трек "Ти зруйнував"
Ілон Маск - марсіанин
→ Купити якісний трек Elon is a Martian
Повторить
→ Купити якісний трек "Повторить"
Наче вогонь
→ Купити якісний трек "Наче вогонь"
On a Sunday Morning
→ Купити якісний трек On a Sunday Morning