В DARPA винайшли технологію, яка насправді захищає комп’ютерну систему від зламу

Влітку 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