Влітку 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.
Зацікавленість у створенні надійно захищених програм зростає прямо пропорційно до перенесення в онлайн-простір найважливіших процесів. Раніше, коли комп’ютери були встановлені в офісах або домогосподарствах, і не були пов’язані між собою, певний баг міг принести хіба що побутові незручності. Сьогодні ж ми маємо сотні підключених і з’єднаних між собою приладів, і найменша помилка може призвести до вразливості всієї системи. За таких умов будь-хто з належними знаннями та навичками зможе ззовні отримати контроль не тільки за приладами, але і за інформацією.
Ендрю Аппель (Andrew Appel), професор з Принстонського університету, що керує програмою досліджень верифікації, пояснює: «В минулому столітті програмний баг означав, що програма не працюватиме належним чином. Що ж, так і буде. Але в XXI столітті баг практично вмикає «зелене світло» зловмисникам для викрадення ваших персональних даних чи виведення з ладу мережі. З прийнятної помилки в програмі баг перетворився на чинник вразливого місця в системі. А це вже набагато гірше і непередбачуваніше.»
Мрія про досконалі програми
Кейтлін Фішер керує експериментальним проектом HACMS
В жовтні 1973 року Едсґейр Дайкстра (Edsger Dijkstra), голландський науковець у галузі комп’ютерних наук, захопився розробкою безпомилкового коду, який не допускатиме зовнішнього втручання. Ідея привнести в програмування більше математичних правил прийшла до вченого зненацька: як згадував сам Дайкстра, він прокинувся посеред ночі і понад годину безперервно записував свою теорію. Матеріал став основою для книги «Дисципліна програмування» (1976 р.), яка в свою чергу, започаткувала новий принцип розробки програм. Разом із працями сера Тоні Хоара (Tony Hoare), ця книга сформулювала концепцію доказів правильності роботи коду, які повинні бути вписані в саму програму. Обидва вчені отримали Премію Т’юрінга за свою діяльність в галузі комп’ютерних технологій.
Однак концепція, яку сформували науковці, довгий час не застосовувалась в комп’ютерній науці. Професійна спільнота вважала за неможливе чітко описати функції та роботу програми, використовуючи математичні правила формальної логіки.
Формальна специфікація — це спосіб описати, що саме робить програма, а формальна верифікація — спосіб довести, що програмний код повністю відповідає заданій специфікації. Уявімо процес написання програми для безпілотного автомобіля, що має доправити пасажира до супермаркету. На операційному рівні, розробнику потрібно визначити перелік дій, які може виконувати машина, щоб виконати поставлене завдання: повороти ліворуч/ праворуч, прискорення чи зменшення швидкості, зупинка транспорту в пункті призначення. Програма, яку вбудують в комп’ютер машини, буде являти собою комбінацію всіх можливих дій у тій послідовності, яка забезпечить прибуття пасажира саме туди, куди потрібно — в супермаркет, а не на вокзал.
Найпростіший спосіб перевірити працездатність програми — провести тестування. Зазвичай розробники проводять велику кількість модульних тестів з різними вихідними даними. Так можна отримати програмний продукт, який працює належним чином майже у 100% випадків — показник, цілком прийнятний для більшості програм. Але модульне, або автономне, тестування не може гарантувати, що програма буде працювати належним чином кожного разу, тому що неможливо передбачити та перевірити виконання дії в усіх комбінаціях додаткових умов. Навіть якщо ви перевірили здатність безпілотного авто довести вас до супермаркету в декількох десятках різних умов, не виключено, що в нестандартній ситуації, яка не потрапила в програму тестів, машинне керування дасть збій і спричинить помилку в системі безпеки. Наприклад, в кінцевій програмі може проявитись незначна помилка: алгоритм копіює трохи більший об’єм даних, аніж був заданий, і через це в пам’яті комп’ютера одні дані записуються на інші. Цю помилку важко виявити і ліквідувати, однак вона дає можливість хакерам отримати доступ до всієї системи — все одно, що залишити відчиненими бічні двері до захищеної фортеці.
«Одна слабка ланка в програмі перетворюється на вразливість захисної системи. А заздалегідь перевірити всі можливі варіанти вихідних даних просто нереально», — констатує Парно. Фактичні специфікації для ПЗ, як правило, вимогливіші за приклад, наведений вище. Наприклад, потрібно написати програму для патентного бюро, яка буде засвідчувати документи та присвоювати їм дату в тому порядку, в якому вони надійшли до бази. В специфікації слід вказати, що номери повинні присвоюватись в порядку зростання (найменші — старішим файлам, а найбільші номери — новішим надходженням), а також, що програма має зберігати ключ для посвідчення документів.
Все це доволі легко можна передати словами, але важко перекласти на формальну мову, яку зрозуміє комп’ютер — в цьому і полягає основна складність в процесі написання ПЗ. Парно роз’яснює: «Легко наказати комусь не розголошувати мій пароль. Але щоб перетворити таку команду на математичне визначення потрібно добре напружитись.»
Візьмемо інший приклад: потрібно написати програму для сортування списку чисел. Розробник намагається уточнити запит для майбутнього коду в формулі:
Переконатись, що кожне число j в переліку відповідає твердженню j ≤ j+1
Однак ця умова, що кожне число в списку повинно бути менше або дорівнювати наступному числу — також містить помилку: розробник припускає, що програма просто виконає перестановку чисел в заданому списку, відповідно до специфікації. Однак, програма може видати впорядкований список з числами, яких не було в вихідних даних, але вони відповідають вимозі й тому були додані до списку.
Іншими словами, у формальній специфікації важко описати всі ті вимоги, при цьому, передбачити допустимі, але непотрібні в конкретному випадку значення. Приклад з сортуванням чисел доволі зрозумілий, але ж бувають абстрактніші специфікації, той самий захист паролю. Як пояснити цю умову з математичної точки зору? Щоб чітко поставити задачу, доведеться скласти математичне визначення поняття «зберігати в секреті», в контексті паролю, а також описати, як визначається надійність алгоритму шифрування. «Ми довго шукали відповіді на подібні запитання, як і багато інших спеціалістів. Але чіткі визначення знайти вкрай важко», — зауважує Парно.
ЧИТАЙТЕ ТАКОЖ:
Безпека на основі блоків
Програма з прописаною формальною верифікацією, в кодовому визначенні, може бути в 5 разів довшою за традиційну, яка була написана для виконання тієї ж дії. Причина полягає у тому, що перші мають в собі не тільки специфікації, але й додаткові анотації, необхідні для правильної імплементації задачі. Цього ускладнення можна позбутись з допомогою відповідних інструментів — мов програмування та систем автоматичного доведення теорем. Вони створені спеціально, щоб інженери могли побудувати стійкий до зовнішніх загроз код. Але в 1970-х роках таких засобів ще не винайшли. Професор Аппель сьогодні очолює групу розробників DeepSpec, які працюють з формально верифікованими системами. Він пояснює, що через незрілість комп’ютерних наук і технологій у 1980 році більшість спеціалістів припинили пошуки математичного вирішення питань безпеки в коді.
Подальше вдосконалення технологій не вирішило всіх питань, з’явилась нова серйозна перешкода: дослідники не були впевнені в беззаперечній необхідності верифікації програм. В той час як ентузіасти формального методу описували найменший баг в коді, як потенційну катастрофу, всі інші розробники бачили лише системи, які досить нормально працювали. Звичайно, інколи програми «падали», але це призводило лише до втрати останніх незбережених даних, а вирішенням був перезапуск системи. Заради виправлення таких незначних помилок не хотілось витрачати час щоб ретельно, знак за знаком, перекладати кожен фрагмент коду на мову формальної логіки. Поступово навіть прихильники методу верифікації програм почали сумніватись в його доцільності. В 1990-х навіть Тоні Хоар, чия іменна «логіка Хоара» стала науковим підґрунтям для конструювання коректних програм, визнавав, що трудомісткий процес визначення специфікацій в коді програм може бути складним вирішенням для проблеми, якої взагалі не існує. В 1995 році він написав:
«— 10 років тому дослідники формального методу (серед яких був і я) помилково стверджували, що програмісти майбутнього будуть вдячні за ту допомогу в роботі, яку обіцяв нам метод формалізації написання коду… Але виявилось, що ніхто насправді не переймався проблемою, яку ми так затято взялись вирішувати за допомогою формальної верифікації.»
Аж тут з’явився інтернет, який дозволив програмним помилкам в коді розповсюдитись по всьому світу. Ефект можна порівняти з поширенням інфекційних захворювань між континентами, завдяки розвитку авіаційного сполучення. Коли кожен окремий комп’ютер по єдиній Мережі під’єднаний до іншого, «незручна, але терпима» помилка в коді може спричинити ланцюгову реакцію падіння систем безпеки даних по всьому світу.
«Тоді ми не врахували факту, що деякі системи захисту інформації мають важливішу роль, тому що забезпечують зовнішній захист від хакерів, — зізнається Аппель. — І неточність в такій програмі гарантовано спричинює вразливість всієї системи безпеки». Коли ж спеціалісти усвідомили ступінь загрози даним в інтернеті, настав час для повернення до методу верифікації програм. В першу чергу, спеціалісти взялись за розробку допоміжних технологій для формальних методів:
- вдосконалення систем автоматичного доведення теорем, на зразок Coq та Isabelle;
- розвиток нових логічних систем (теорії залежного типу даних), які встановлюють межі поля для розробки коду;
- модернізація т.з. «операційної семантики» — по суті, це мова, в якій є всі необхідні слова для опису того, що повинна виконувати програма.
«Якщо ви беретесь за визначення специфікації англійською мовою, умовно, ви працюєте з невизначеною або ж багатозначною специфікацією», — роз’яснює Жанет Вінг (Jeannette Wing), корпоративний віце-президент в Microsoft Research. «Будь-яка природня мова є, по своїй суті, багатозначною, неконкретною. Використовуючи формальну специфікацію, ви описуєте чіткі характеристики, що базуються на математичному поясненні належної роботи програми.»
В Microsoft Research Жанет Вінг працює над створенням протоколу формальної верифікації для інтернету
Окрім вищевказаних змін в технологіях, вчені також переглянули власні цілі, з якими розробляли формальний метод. В 1970-1980-х рр. вони намагались досягти створення повністю перевірених комп’ютерних систем, від етапу написання схеми керування до кінцевої програми. Тепер дослідники формального методу сфокусувались на менших, але найбільш вразливих до зовнішнього втручання, або ж найважливіших для безпеки даних фрагментах. До таких критично важливих програм належать операційні системи, криптографічні протоколи тощо. Вінг уточнює, що дослідники вже розуміють: неможливо гарантувати коректну роботи програми на 100% в кожній ланці написаного коду.
«— Сьогодні ми чіткіше усвідомлюємо власні можливості — що ми можемо, і що не можемо зробити.»
Проект HACMS став доказом того, як можна посилити безпеку системи, встановивши особливу специфікацію для окремого фрагменту програми. Першочергово, в рамках проекту планували створити незламний квадрокоптер. Програмне забезпечення тих дронів, які вже доступні на масовому ринку, було неподільним — якщо хакеру вдасться зламати один з фрагментів коду, він отримає доступ до усієї системи. Тож, протягом двох років команда HACMS працювала над розділенням системи управління апаратом на окремі фрагменти. Окрім того, була переписана архітектура ПЗ — за словами проектного менеджера Фішер, програмісти почали використовувати т.з. «високонадійні будівельні блоки», що дозволяють підтвердити правильність передачі інформації написаним кодом. Один з таких будівельних блоків гарантує, що хакер, отримавши доступ до однієї частини програми, не зможе використати аналогічні інструменти для зламу інших складових системи.
Саме таке розподілене на частини ПЗ було встановлено на гелікоптер Little Bird. Хакери з Red Team отримали від розробників доступ до однієї зі складових частин програми — вони управляли камерою безпілотника, але не його основними функціями. Програмісти зробили математичний розрахунок, відповідно до якого хакери точно не зможуть дістатись до інших фрагментів програми. Практичний експеримент підтвердив вірність застосування математичного підходу. «Це не стало для нас несподіванкою, — констатує Кейтлін Фішер, — але завжди краще отримати наочне підтвердження теорії.»
За рік, що минув з часу успішних випробувань Little Bird, фахівці DARPA встановили розробки HACMS в інші військові системи, супутники й безпілотні вантажівки. Поява нових проектів узгоджується із значним проривом в дослідженні формальної верифікації, що стався за останнє десятиліття. І кожна нова розробка підбадьорює наступну команду фахівців працювати в тому ж напрямку.
Фішер підсумовує: «— Тепер вже ніхто не може виправдовуватись тим, що системи формальної верифікації — занадто складні.»
Перевірка інтернету
Безпека та надійність — два показники, на які орієнтуються розробники формальних методів в програмуванні. Щодня необхідність у підсиленні надійного захисту інформації стає все більш очевидною. В 2014 році помилка в криптографічному програмному забезпеченні OpenSSL (Heartbleed), теоретично, могла спричинити глобальний збій в роботі Мережі. Однак вбудований механізм формальної специфікації зміг би завчасно виявити цей баг. А 2015-го IT-спільнота вражено спостерігала, як ентузіасти онлайн-безпеки дистанційно перехопили керування автомобілем Jeep Cherokee.
Ціна помилки в системах безпеки постійно зростає, разом із збільшенням ролі онлайн-технологій в сучасному світі. Тому деякі розробники, зокрема Аппель і команда DeepSpec, знову повертаються до ідеї створення гарантовано безпечної системи, від початкового коду до кінцевого продукту. Цього разу, на відміну від спроб 1970-х років, фахівці працюють над аналогом безпечного веб-сервера, в якому об’єднаються розрізнені методи формальної верифікації, дієвість яких вже доведена експериментально, на кшталт згаданої вище програми в гелікоптері. Найголовніше завдання, що стоїть перед дослідниками сьогодні, — створення специфікованого єдиного інтерфейсу для всіх працездатних технологій верифікації. Шанси на успіх проекту доволі переконливі, зважаючи на той факт, що Національний науковий фонд США виділив на реалізацію задуму грант у розмірі $10 млн.
В Microsoft Research будують власні плани на подальшу розробку формальної верифікації. Один із проектів зветься Everest і полягає в створенні верифікованої версії HTTPS. Жанет Вінг вважає цей протокол Ахіллесовою п’ятою інтернету, а тому його підсилення є стратегічно важливим кроком. Інший напрямок діяльності фахівців — розробка верифікованих специфікацій для систем, що керуються апаратами. Додаткові ускладнення спричинені тим, що алгоритм, який керує тим же дроном, використовує машинне навчання. Ця технологія відповідає за прийняття рішень щодо маршруту безпілотника, на основі даних про умови навколишнього середовища, які надходять в режимі реального часу. Всі алгоритми потрібно захистити від зовнішнього втручання, і Вінг, яка керує дослідженнями, впевнена у спроможності сучасних інструментів гарантувати безпеку даних. Адже за останнє десятиліття формальні методи значно прогресували, і все більше першокласних спеціалістів розвивають цей напрямок.
За матеріалами: Quanta Magazine