Чи дозволить формальна верифікація коду мікроядра створювати наднадійні ОС

У 2015 році американська компанія Rockwell Collins спільно з Boeing і 3D-Robotics провела випробування стійких до злому квадрокоптера Iris і безпілотного вертольота Little Bird з «наднадійною» операційною системою.

Розробка захищених від злому дронів ведеться на замовлення Агентства перспективних оборонних проектів (DARPA) Міністерства оборони США, яке зацікавлене в захисті перспективних безпілотних і опціонально пілотованих літальних апаратах від можливих вразливостей.

Існує як мінімум три способи злому безпілотних літальних апаратів: перший - отримання доступу до управління за допомогою злому каналу зв'язку або підміни даних авторизації, другий - використання вразливостей програмного забезпечення, третій - використання інтерфейсів і каналів даних оригінального програмного забезпечення для завантаження шкідливого коду.

Розроблена Rockwell Collins операційна система на базі мікроядра seL4 стійка до всіх трьох типів злому. Операційна система на базі seL4 спочатку орієнтована в першу чергу на безпеку. Англійською це називається красивим словосполученням «hackproof» (зломостійка).

Її особливістю є стійке до підмінів коду ядро, яке використовує математичні алгоритми і контрольні суми для перевірки запущених служб, а також забезпечує роздільне виконання процесів.

Система дозволяє запустити віртуальну машину, в якій гостьова програма не отримує доступу до основних процесів або апаратної частини. Під час запуску програми повідомляють ядру контрольні суми, на основі яких проводиться виправлення помилок або закриття несанкціонованих процесів.

Випробування пройшли успішно: фахівцям з кібербезпеки не вдалося запустити шкідливий код на безпілотних апаратах з захищеною операційною системою, а також перехопити управління дроном або викликати системний збій.

Мікроядро seL4 використовується не тільки в авіації, але і в медицині, фінансовому секторі, енергетиці та інших областях, де необхідна гарантія відсутності збоїв.

Важлива особливість архітектури seL4 - винос частин для управління ресурсами ядра в простір користувача і застосування для цих ресурсів тих же засобів розмежування доступу, що і для ресурсів користувальницьких. Мікроядро не надає готових високорівневих абстракцій для керування файлами, процесами, мережевими з'єднаннями тощо.

Замість цього воно надає лише мінімальні механізми для управління доступом до фізичного адресного простору, переривань і ресурсів процесора.

Високорівневі абстракції та драйвери для взаємодії з обладнанням реалізуються окремо - поверх мікроядра у формі завдань, що виконуються на користувальницькому рівні. Доступ таких завдань до наявних у мікроядра ресурсів організовується через визначення правил.

Для програмістів існує компоненто-орієнтована платформа розробки програм CAmkES, що дозволяє моделювати і створювати системи на основі seL4 у вигляді колекції взаємодіючих між собою компонентів.

З seL4 генетично пов'язаний проект L4.verified - формально верифіковане ядро на архітектурі L4.

L4 - мікроядро другого покоління, розроблене Йохеном Лідтке в 1993 році.

Архітектура мікроядра L4 виявилася успішною. Було створено безліч реалізацій ABI і API мікроядра L4. Всі реалізації стали називати «сімейством мікроядер L4». Так з'явився і seL4. А реалізація Лідтке неофіційно була названа «L4/x86».

Основна ідея L4.verified, як і seL4, - математично довести коректність реалізації ядра. Справа в тому, що мікроядра на відміну від монолітно-модульних монстрів типу GNU/Linux, вельми мініатюрні за розміром. А раз так, то вони можуть бути формально верифіковані. Кожній сходинці коду ставиться у відповідність математичне твердження, яке потрібно довести.

У мікроядрі L4.verified доводиться відповідність реалізації моделі, відсутність вічних циклів і ще деяких речей. Вартість цього дослідження склала близько 6 мільйонів, а проект тривав 7 років. Обсяг роботи досяг 25 осіб еко-років.

Крім свого основного застосування (безпека, як і у seL4) L4 використовується і в інших сферах. Так, фірма Qualcomm запустила реалізацію мікроядра L4, розроблену фірмою NICTA, на наборі мікросхем, званому «Mobile Station Modem» (MSM). Про це в листопаді 2005 року повідомили представники фірми NICTA, а наприкінці 2006 року набори мікросхем MSM надійшли в продаж. Так реалізація мікроядра L4 опинилася в стільникових телефонах.

Питання створення наднадійного ПЗ стало особливо актуальним, коли переважна більшість додатків стала працювати в мережі і оперувати з великою кількістю даних. А дані ці часто конфіденційні.

У мережі не так багато матеріалів про роль формальної верифікації у створенні наднадійних ОС. Ще менше ґрунтовних дискусій. Тому нижче наведемо основні думки та аргументи однієї з бесід з приводу статті на цю тему:

• Розповсюдження засобів верифікації та грамотне їх впровадження дозволить позбутися цілого класу помилок у будь-якому програмному забезпеченні. Наприклад, таку помилку, як «переповнення буфера», можна запобігти, якщо достатньо просто організувати перевірку необхідних параметрів.

Баги там все-таки є, робить висновок один з коментаторів, посилаючись на цей матеріал.

• Стверджується, що код seL4 володіє деяким ступенем надійності. Якщо створення абсолютно захищеної від злому ОС - утопія, то чому цим продовжують займатися такі круті команди, як DARPA?
• Що буде, якщо хакери підсунуть туди верифікований код? Чи це неможливо? Чому у всіх ОС є баги, які обов'язково можуть використовувати хакери?
• Чому верифікація коду обов'язково повинна бути пов'язана із захистом від злому? Що, простіше не можна? Верифікація коду і захист від злому - це два різні завдання, які всього лише іноді перетинаються.

Трояни, кібервимогательство, фішинг, клікджекінг - це види атак, які працюють незалежно від наявності помилок в програмному коді додатків або операційної системи в цілому. А якщо користувачі вибирають слабкі паролі? Це теж вина розробників ПЗ?

• Експеримент розходиться з реальністю, оскільки доступ, який дали хакерам дослідники, в житті їм ніхто не відкриє. У таких системах просто потрібно уважно стежити за тим, щоб забороняти вставляти код всім, крім адміністратора.
• Треба ж! Добре написані і протестовані додатки дуже важко зламати. Хто б міг подумати... Взагалі-то, програмний код і так складається з математично верифікованих конструкцій.
• Розробка верифікованого коду - розкіш, яку можуть дозволити собі деякі. А його супровід і постійне внесення змін - ще більша розкіш.
• З точки зору менеджменту, програмісти часто поводяться біполярно. Коли їх просиш розбити велике завдання з розробки на підзадачі, вони легко погоджуються. Але коли пропонуєш їм заздалегідь подумати над можливими помилками і планомірно їм запобігати - реакція зовсім інша: «це непрактично», «всього не передбачиш», «а як же те?», «як же це?»... Далеко не всі хочуть думати про якість коду заздалегідь.
• А що робити, якщо засоби верифікації самі містять помилки? Хто буде верифікувати верифікатори?
• У чистій математиці немає «багів». Якщо є правило, що ділити на нуль не можна, значить, випадки, коли в знаменнику виявляється нуль, просто не розглядаються. У реальному житті цей прийом не працює. Якщо мова йде про розробку ПЗ, то там доводиться працювати навіть з тими значеннями, які програмі «не подобаються». Результат від поділу на нуль - це нескінченність. І з нею потрібно щось робити, а не заявляти, що такого результату не може бути.

Звичайно ж, дискутувати можна нескінченно. Але якщо такі великі організації, як DARPA, роблять конкретні кроки з реалізації цих проектів, за цією історією як мінімум варто піти і як максимум - взяти участь.

Початковий код seL4 все ще доступний на GitHub.