В Австралії створено дрон з найзахищенішою операційною системою в світі

116 Views Comment Off

Таким його робить унікальна операційна система seL4, що лежить в основі апарату, яка оптимізована для максимальної безпеки. Вона була створена для використання в захищених системах найширшого спектра – від бортових комп’ютерів літаків до автоматизованих промислових комплексів.

У 2009 році австралійські дослідники зуміли математично довести, що seL4 в будь-яких обставинах буде працювати у відповідності зі строгими специфікаціями – цей принцип носить назву “формальна верифікація”. Цей математичний доказ демонструє, що seL4 не містить в собі жодної програмної уразливості. Її особливість полягає саме в суворому дотриманні закладеним в неї вказівкам. Іншими словами, якщо в специфікації не вказано переповнення буфера (поширена програмна уразливість), система ніколи не викличе переповнення буфера.

Мікроядро seL4 (фактично центральний базовий код операційної системи) має суворий поділ критичних і некритичних функцій. Завдяки цьому, якщо хакеру-зловмисникові вдасться взяти під контроль запущений в ОС додаток, всі інші частини системи залишаться для нього повністю недоступні.

Однак безпека мікроядра seL4 все ж може бути скомпрометована. Так, наприклад, це може статися, якщо апаратна платформа, на якій працює ОС, містить глибоко інтегрований шпигунський код (бекдор) або має інші програмні уразливості.

seL4_1

“Ми нічого не можемо вдіяти з апаратним бекдором, – пояснює лідер дослідницької групи Data61 Trustworthy Systems Гервін Кляйн (Gerwin Klein). – Зрештою, якщо ви не можете довіряти апаратній частини своєї системи, з цим неможливо щось зробити”.

Data61 працює в тісному контакті з американським агентством DARPA для польових випробувань своєї системи. У минулому році seL4 була встановлена на вертоліт Boeing “Little Bird” для проведення тестів на можливість його злому під час польоту. Ці випробування довели, що жодну критичну систему гелікоптера під керуванням австралійської ОС зламати неможливо.

Крім очевидного військового використання, мікроядро від Data61 може знайти застосування в цілому ряді сфер промисловості, де потрібні високозахищені системи. ОС seL4 була випущена в якості опенсорсного програмного забезпечення два роки тому, а тому доступна всім бажаючим. Основними кандидатами на її застосування є виробники автомобілів та іншої транспортної техніки. Так, наприклад, в середині минулого року дослідники Чарлі Міллер і Кріс Валасек знайшли уразливість в блоці телематики, яка дозволяла взяти під контроль гальма Jeep Cherokee. Після цього концерн Fiat Chrysler був змушений відкликати 1,4 мільйона автомобілів до повного усунення небезпеки.

На поточний момент агентство DARPA вже видало ряд грантів невеликим компаніям на застосування seL4. Однак до її появи на ринку може пройти ще кілька років. Оскільки мікроядро лежить в самій основі продукту, може піти до п’яти років на завершення його розробки.

... ... .
In : Техно

Related Articles

404