AdaCore: Зростання Ada, SPARK, Rust в оборонних програмах США

AdaCore зафіксувала суттєве зростання кількості проєктів у аерокосмічних та оборонних програмах США, які використовують мови програмування, безпечні до пам'яті, зокрема Ada, SPARK та Rust. Це зростання охоплює критично важливі застосунки, включаючи системи керування польотом авіоніки, автономні безпілотні системи, наземну інфраструктуру командування та управління, захищені комунікаційні платформи та супутникові системи нового покоління.

Перехід від небезпечних мов

Збільшення використання цих мов відображає ширшу тенденцію відмови від мов, небезпечних до пам'яті, таких як C та C++. Цей перехід зумовлений регуляторним тиском, вимогами національної безпеки та досвідом, отриманим від гучних вразливостей програмного забезпечення, що вплинули на оборонні платформи. Вразливості, пов'язані з безпекою пам'яті, такі як переповнення буфера, використання після звільнення та розіменування нульового покажчика, становлять приблизно 70 відсотків критичних вразливостей програмного забезпечення. Ці дані базуються на дослідженнях Microsoft та Google, а також відображені в рекомендаціях Агентства національної безпеки (NSA).

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

Технологічні переваги

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

Підтвердження незалежним дослідженням

Тенденція до впровадження підтверджується незалежним звітом VDC Strategy під назвою «Memory-Safe Languages Offer Protection for Devices and TCO». Дослідження, засноване на опитуванні понад 500 осіб, які приймають рішення щодо вбудованого програмного забезпечення, визначило Ada, SPARK та Rust як три найкращі мови для задоволення вимог безпеки та захисту серед 26 оцінених мов. Понад 85 відсотків респондентів заявили, що вибір мови програмування може безпосередньо впливати на безпеку та захист продукту.

Звіт також виявив потенційні переваги щодо термінів та витрат. Проєкти на Ada в чотири рази частіше завершувалися раніше запланованого терміну, ніж проєкти на C, тоді як SPARK продемонстрував найсильніші показники дотримання графіку в опитуванні. Проєкти, що використовують мови, безпечні до пам'яті, повідомили про медіанні витрати на розробку в два-чотири рази нижчі, ніж проєкти, розроблені з використанням C та C++. Протягом типового семирічного періоду експлуатації, мови, безпечні до пам'яті, також були пов'язані з економією до 60 відсотків на виправленнях та усуненні дефектів. Ці висновки особливо актуальні для аерокосмічних та оборонних програм, де сертифікація, верифікація на пізніх етапах та довгострокове обслуговування можуть бути значними факторами витрат.

Довіра до ШІ-генерованого коду

Дослідження також вивчало використання коду, згенерованого штучним інтелектом. Користувачі мов, безпечних до пам'яті, повідомили про більшу довіру до програмного забезпечення, згенерованого ШІ, ніж користувачі C або C++. Можливості формальної верифікації SPARK були названі одним із способів підвищення довіри до коду, створеного за допомогою агентних робочих процесів ШІ.

Квентін Охем, президент і генеральний директор AdaCore, зазначив, що для їхніх клієнтів в аерокосмічній та оборонній галузях "коректність має бути вбудована з самого початку", оскільки вони не можуть усувати дефекти програмного забезпечення після розгортання системи. Він підкреслив, що безпека пам'яті "все частіше розглядається як базова вимога, а не як приємна додаткова функція", і що незалежне дослідження підтверджує, що це "не тільки безпечніший шлях, але й швидший та економічніший".

Підтримка уряду США

Перехід до мов програмування, безпечних до пам'яті, також заохочується політичними рекомендаціями уряду США. Агентство національної безпеки, Агентство з кібербезпеки та безпеки інфраструктури (CISA) та Офіс національного кібердиректора Білого дому (ONCD) закликали оборонно-промислову базу перейти від мов, небезпечних до пам'яті. Ініціатива CISA "Secure by Design" та звіт ONCD "Back to the Building Blocks" визначили безпеку пам'яті як фундаментальну вимогу до програмного забезпечення, що використовується в критичній інфраструктурі та системах національної безпеки.

Що це означає для розробників

Для розробників у аерокосмічній та оборонній галузях це означає зростаючий тиск та заохочення до використання мов, безпечних до пам'яті, таких як Ada, SPARK та Rust. Ці мови пропонують інструменти для математичної верифікації (SPARK) та запобігання помилкам під час компіляції (Rust), що може призвести до значного зниження витрат на розробку та обслуговування, а також підвищення довіри до ШІ-генерованого коду.

Ключові факти

AdaCore повідомляє про значне зростання використання Ada, SPARK та Rust у аерокосмічних та оборонних програмах США.
Ці мови використовуються для місійно-критичних застосунків, включаючи авіоніку та автономні системи.
Перехід від C/C++ зумовлений регуляторним тиском, національною безпекою та вразливостями.
Вразливості безпеки пам'яті становлять ~70% критичних вразливостей ПЗ.
Незалежний звіт VDC Strategy визначив Ada, SPARK та Rust як найкращі для безпеки та захисту.