Формальна верифікація програмного забезпечення критичної безпеки: методи, інструменти та гарантії

Автор: Corvus Intelligence Engineering Team · Про команду →

25 червня 2026 13 хв читання

Кожна програма верифікації програмного забезпечення зрештою стикається з однією й тією самою структурною проблемою: тестування обмежене. Набір тестів, яким би великим він не був, охоплює скінченну підмножину вхідних даних і шляхів виконання. Решта, невипробувані комбінації, є неявним припущенням про правильність невипробуваної поведінки. Для більшості комерційного ПЗ таке припущення є прийнятним; вартість невиявленого дефекту можна відшкодувати. Для програмної безпеки в оборонних системах — коду, що керує зброєю, поверхнями управління польотом або функціями критичної підтримки, — єдиний дефект у невипробуваному шляху може мати катастрофічні наслідки. Формальна верифікація усуває цю прогалину не шляхом виконання більшої кількості тестів, а заміною доказів на основі виконання математичним доведенням.

Формальні методи охоплюють сімейство технік — перевірку моделей, доведення теорем та абстрактну інтерпретацію, — які математично міркують над повним простором можливих поведінок програми. Кожна з них пропонує різні компроміси між виразністю, автоматизацією, масштабованістю та силою одержаної гарантії. У цій статті розглядається кожна техніка в контексті розробки оборонного ПЗ, пояснюється їхня інтеграція у сертифікацію DO-178C DAL A та аналіз безпеки MIL-STD-882, а також наводиться реалістична оцінка того, де формальні методи виправдовують себе, а де — ні.

Чому одне лише тестування не може забезпечити гарантії безпеки

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

Стеля покриття. Метрики структурного покриття — покриття операторів, покриття гілок, Modified Condition/Decision Coverage (MC/DC) — вимірюють частку структур коду, що охоплюються набором тестів. DO-178C вимагає MC/DC-покриття для ПЗ DAL A, оскільки воно гарантує незалежну демонстрацію впливу кожного результату рішення та кожної умови в межах кожного рішення на кінцевий результат. Та навіть 100% MC/DC-покриття не вичерпує простір вхідних даних: функція з п'ятьма 32-бітними цілочисельними параметрами має 2¹⁶⁰ можливих комбінацій вхідних даних. Набір тестів, що демонструє 100% MC/DC-покриття, може охоплювати десятки або сотні шляхів виконання, проте нічого не говорить про правильність виконань, що поєднують певні значення вхідних даних у невипробувані способи. Стеля покриття — це не проблема якості тестування; це математичний факт про скінченне тестування нескінченних просторів.

Комбінаторний вибух у конкурентних системах. Критично важливе оборонне ПЗ майже завжди є конкурентним: кілька завдань виконуються паралельно, спільно використовують пам'ять, обмінюються повідомленнями через черги та семафори, й піддаються перериванням, що можуть витіснити виконання в довільні моменти. Кількість можливих чергувань N конкурентних завдань з K кроками кожне зростає як O(K^N). Система з трьома завданнями по десять кроків має понад мільярд можливих чергувань. Тестування охоплює лише незначну частину з них; метрики покриття нічого не говорять про невипробувані чергування. Перегонові умови, інверсії пріоритетів та взаємні блокування ховаються в чергуваннях, яких тестування випадково не торкається.

Роль формальних методів. Формальна верифікація вирішує ці проблеми, замінюючи перебір доведенням. Замість того щоб запитувати «чи поводилася система правильно для цих вхідних даних?», вона запитує: «чи є математично неможливим те, що система поводитиметься неправильно для будь-яких вхідних даних?» Запитання складніше й дорожче у відповіді, але відповідь — якщо вона позитивна — є категорично сильнішою. Саме тому авіаційна, ядерна та оборонна галузі вимагають або заохочують застосування формальних методів для найвищих рівнів гарантії проектування: тестування встановлює впевненість; формальна верифікація встановлює визначеність у межах формальної моделі та її припущень.

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

Перевірка моделей: вичерпна верифікація простору станів

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

Властивості темпоральної логіки для оборонних систем. Лінійна темпоральна логіка (LTL) та логіка дерева обчислень (CTL) є двома основними мовами властивостей, що використовуються під час перевірки моделей. Властивості LTL виражають обмеження на окремі шляхи виконання. Типова оборонна властивість безпеки: завжди, коли система переходить у збройний стан, в наступному стані мають бути присутніми як знятий запобіжник, так і підтвердження оператора. Властивості CTL міркують про розгалужені дерева обчислень — виражаючи, наприклад, що шлях відновлення завжди існує з будь-якого досяжного стану. Оборонні застосування включають верифікацію того, що скінченні автомати протоколів зв'язку ніколи не переходять у невизначені стани, що логіка планування завжди дотримується дедлайнів при будь-якому порядку завдань, і що послідовності запобіжника не можна обійти жодною комбінацією допустимих вхідних даних.

Інструменти: SPIN і NuSMV. SPIN — це перевірник моделей із явним станом, що використовується переважно для верифікації конкурентного ПЗ та протоколів зв'язку. Його вхідна мова, Promela, моделює конкурентні процеси, що комунікують через канали повідомлень; властивості виражаються в LTL. SPIN виконує верифікацію через пошук у глибину з хеш-сховищем станів і видає трасування контрприкладів, які можна відтворити в симуляторі. NuSMV — символічний перевірник моделей, що використовує Binary Decision Diagrams (BDDs) та обмежену перевірку моделей із SAT-вирішувачами для символічного представлення та дослідження множин станів, — що робить його ефективним для систем із великим простором станів, де явне перерахування неможливе. Для протоколів і скінченних автоматів оборонного ПЗ SPIN зазвичай більш застосовний; для вбудованої керуючої логіки, змодельованої на рівні регістрових передач, символічний підхід NuSMV часто є більш прийнятним.

Проблема вибуху простору станів та CEGAR. Досяжний простір станів зростає експоненціально з розміром системи. Уточнення абстракції на основі контрприкладів (CEGAR) є основною практичною технікою управління цим явищем. Робочий процес починається з грубої абстрактної моделі, достатньо малої для верифікації, але такої, що може вводити хибні поведінки, відсутні в конкретній системі. Якщо властивість виконується на абстрактній моделі, вона виконується й на конкретній системі завдяки звуковості абстракції. Якщо знайдено контрприклад, він перевіряється на конкретній моделі: якщо конкретна модель також демонструє контрприклад, це реальний дефект; якщо ні, абстракція уточнюється шляхом додавання деталей у тій галузі, де виник хибний контрприклад. CEGAR є ітеративним і може сходитися до результату верифікації, ніколи не представляючи явно повний простір станів.

/* SPIN Promela fragment: weapon release interlock */
mtype = { SAFE, ARMED, RELEASED };
mtype safety_state = SAFE;
mtype confirm_state = SAFE;
mtype release_state = SAFE;

active proctype safety_controller() {
  do
  :: safety_state == ARMED && confirm_state == RELEASED ->
       atomic { release_state = RELEASED; }
  :: else -> skip
  od
}

/* LTL property: release only when both preconditions hold */
ltl p1 { [] (release_state == RELEASED ->
              (safety_state == ARMED && confirm_state == RELEASED)) }

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

Доведення теорем: машинно-перевірені математичні докази

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

Coq, Isabelle/HOL та PVS в обороні. Coq — це помічник із доведення, побудований на теорії залежних типів; його механізм вилучення може генерувати перевірений виконуваний код безпосередньо зі специфікації, яку доведено правильною, створюючи ланцюжок від доказу до виконуваного бінарного файлу. Він застосовувався для верифікації криптографічних алгоритмів та трансформацій компіляторів. Isabelle/HOL надає середовище логіки вищих порядків із потужними тактиками автоматизації; найбільш відоме промислове застосування — доказ мікроядра seL4, найбільш досконало верифікованого ядра операційної системи з усіх коли-небудь створених, що довів правильність бінарного виконуваного файлу відповідно до його формальної специфікації. PVS, розроблений в SRI International, спеціально призначений для специфікації ПЗ і застосовувався до польотного ПЗ NASA та логіки систем ядерної безпеки. Кожен із них використовувався в оборонних контекстах: Coq — для протоколів і алгоритмів, Isabelle — для ОС і платформного ПЗ, PVS — для міркувань на рівні специфікацій в авіоніці та космічних системах.

Генерація зобов'язань доведення. Сучасні робочі процеси формальних методів автоматично генерують зобов'язання доведення з анотованого вихідного коду, зменшуючи навантаження від написання специфікацій з нуля. Такі інструменти, як Frama-C із плагіном WP (Weakest Precondition), аналізують вихідний код C, анотований контрактами ACSL (ANSI/ISO C Specification Language), та генерують зобов'язання доведення, які можуть бути розряджені автоматизованими доводчиками (Alt-Ergo, CVC4, Z3) або інтерактивними доводчиками теорем, коли автоматизація не справляється. Мова SPARK для Ada надає схожий інтегрований робочий процес: код SPARK пишеться з контрактами передумов/постумов, а GNATprove генерує та намагається автоматично розрядити зобов'язання доведення, переходячи до інтерактивного доведення лише для зобов'язань, з якими автоматизація не може впоратися. Цей гібридний підхід — максимальна автоматизація із залишенням людського керованого доведення для складних випадків — є практичною моделлю для оборонних програм, які не можуть укомплектувати цілу команду теоретиків доведення.

Компроміс із кривою навчання. Розрив між цінністю, яку може принести доведення теорем, та організаційними інвестиціями, що для цього потрібні, є центральною проблемою при впровадженні цієї техніки. Написання специфікацій у Coq або Isabelle вимагає вільного знання логіки вищих порядків та теорії типів — знань, яких стандартна освіта в галузі програмної інженерії не дає. Розробка доказів для нетривіальних компонентів вимірюється людино-місяцями. Програми, які недооцінюють ці інвестиції, неодмінно виходять за межі графіка. Реалістичний шлях — залучати спеціалізованих доводчиків теорем із організацій, що вже мають таку можливість, обмежуючи область її застосування компонентами, для яких жодна інша техніка не є адекватною, — зазвичай це алгоритми, на яких будується кейс безпеки.

Абстрактна інтерпретація та звуковий статичний аналіз

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

Astrée. Astrée (розроблений у ENS Paris/INRIA та комерціалізований AbsInt) є найвидатнішим інструментом абстрактної інтерпретації в оборонних та аерокосмічних контекстах. Він аналізує вихідний код C щодо таких класів помилок часу виконання: переповнення та неповне заповнення цілих чисел (знакових і беззнакових), ділення на нуль, розіменування нульового покажчика, вихід за межі масиву, недійсна кількість бітового зсуву та читання неініціалізованих змінних. Він використовувався для доведення відсутності помилок часу виконання в основному польотному ПЗ Airbus A380 — приблизно 132 000 рядків C із нульовою кількістю нерозвинених сигналів тривоги після аналізу. Для вбудованого оборонного ПЗ Astrée застосовується на рівні модуля; кожен модуль повинен досягти нуля справжніх сигналів тривоги, перш ніж вважатиметься формально верифікованим щодо відсутності помилок часу виконання.

Polyspace від MathWorks. Polyspace Bug Finder та Polyspace Code Prover надають схожі можливості абстрактної інтерпретації з більш тісною інтеграцією в інструментальний ланцюжок MathWorks (розробка на основі моделей MATLAB/Simulink), поширений у вбудованих оборонних системах. Code Prover використовує абстрактну інтерпретацію на основі інтервалів для доведення — не просто виявлення — відсутності певних класів помилок і класифікує кожну перевірку як Proven (помилка неможлива), Unproven (неможливо визначити) або Error (дефект підтверджено). Як Astrée, так і Polyspace постачають набори кваліфікації інструментів DO-330, зменшуючи навантаження на програмні артефакти для регуляторного визнання.

Клас помилки	Astrée	Polyspace Code Prover	Звуковість
Переповнення / неповне заповнення цілих чисел	Так	Так	Звуковий (без пропусків)
Розіменування нульового покажчика	Так	Так	Звуковий (без пропусків)
Ділення на нуль	Так	Так	Звуковий (без пропусків)
Вихід за межі масиву	Так	Так	Звуковий (без пропусків)
Читання неініціалізованих змінних	Так	Так	Звуковий (без пропусків)

Управління хибними спрацьовуваннями. Звукові інструменти повідомляють консервативно: якщо невпевнені — дають сигнал тривоги. У великих кодових базах C зі складною арифметикою покажчиків, заглушками середовища для невідмодельованих апаратних інтерфейсів або специфічними для платформи розширеннями компілятора рівень хибних спрацьовувань може бути високим — 30–70% при першому запуску є не незвичним. Дисципліна полягає в анотуванні кожного хибного спрацьовування машинозчитуваним обґрунтуванням, яке інструмент приймає як придушення, щоб придушений сигнал не з'являвся в наступних запусках. Кожне придушення є твердженням — «цей сигнал тривоги не може виникнути під час виконання, тому що [причина]» — і твердження мають перевірятися під час інспекцій коду як частина аргументу безпеки. Журнал придушень сам по собі є артефактом безпеки; модуль із великою кількістю придушень заслуговує додаткового ретельного розгляду.

Застосування формальних методів до ПЗ DO-178C DAL A

DO-178C, основний стандарт сертифікації бортового ПЗ і стандарт, що найчастіше застосовується за аналогією до інших критично важливих оборонних платформ, включає додаток з формальних методів — DO-333 (Formal Methods Supplement to DO-178C and DO-278A), — що визначає, як заходи формального аналізу можуть задовольняти цілі верифікації DO-178C.

Додаток, а не заміна тестування. Поширеною помилкою є думка, що формальна верифікація виключає потребу в тестуванні відповідно до DO-178C. DO-333 не підтримує цього. Формальні методи є доповненням: вони можуть надавати кредит для конкретних цілей верифікації, які інакше задовольнялося б тестуванням, зменшуючи обсяг тестування, але не замінюючи всю вимогу тестування. Типовим застосуванням є використання формального аналізу для задоволення цілей структурного покриття — звуковий доказ абстрактної інтерпретації про те, що жодна помилка часу виконання недосяжна в модулі, надає еквівалентну гарантію виконання кожної гілки цього модуля і може бути заявлений як кредит покриття, — тоді як звичайне тестування продовжує задовольняти цілі тестування на основі вимог. Чистий ефект — зменшений розмір набору тестів для модулів DAL A з підвищеною глибиною гарантії для властивостей, на які орієнтується формальний аналіз.

Документація PSAC та SAS. Plan for Software Aspects of Certification (PSAC) повинен описувати підхід до формальних методів із самого початку програми: які формальні методи використовуються, які цілі DO-178C вони адресують, які інструменти використовуються та як інструменти будуть кваліфіковані. Цей плановий артефакт переглядається сертифікуючим органом до початку роботи з формальної верифікації — представлення заявки на формальний метод сертифікатору лише після завершення є провалом процесу, що може анулювати кредит. Software Accomplishment Summary (SAS) документує виконані заходи формальної верифікації та забезпечує простежуваність від кожного формального результату до цілі DO-178C, яку він задовольняє. Свідчення формальної верифікації — виводи запусків інструментів, файли властивостей, файли моделей, записи розпоряджень сигналами тривоги — зберігаються в системі управління конфігурацією як частина даних життєвого циклу сертифікації.

Кваліфікація інструментів. DO-330 визначає вимоги до кваліфікації програмних інструментів, що використовуються при розробці бортового ПЗ. Інструменти, що видають результати, які використовуються без незалежної верифікації в записі відповідності, вимагають кваліфікації відповідно до DAL та ролі інструменту. Інструменти абстрактної інтерпретації, що використовуються для задоволення цілей верифікації DAL A, вимагають кваліфікації TQL-1 — найбільш суворого рівня. Комерційні інструменти, як-от Astrée та Polyspace, надають комплекти підтримки кваліфікації, що включають вимоги до роботи інструменту, процедури кваліфікаційних тестів і результати кваліфікаційних тестів. Відповідальність програми — встановити, що комплект застосовується до контексту її використання: конкретного компілятора, операційної системи та підмножини мови, що застосовується. Інструменти з відкритим кодом без наявних комплектів кваліфікації вимагають від програми самостійного генерування всіх артефактів кваліфікації — суттєві програмні витрати, які мають бути включені в план проекту із самого першого дня.

Ключовий принцип DO-178C / DO-333: Кредит формального методу в записі відповідності заробляється якістю аргументу простежуваності — демонстрацією того, що верифікована формальна властивість точно відповідає вимозі безпеки, задоволення якої вона заявляє. Формально верифікована властивість, яка лише наближено відображає вимогу, не дає регуляторного кредиту і може послабити, а не посилити кейс безпеки.

Усунення небезпек MIL-STD-882 та формальна верифікація

MIL-STD-882E (System Safety) визначає переважну ієрархію засобів контролю небезпек у порядку зменшення ефективності: усунути небезпеку, знизити ймовірність виникнення, додати виявлення або попередження та прийняти залишковий ризик із задокументованим обґрунтуванням. Формальна верифікація безпосередньо сприяє двом першим рівням і забезпечує найбільш обґрунтований аргумент безпеки, коли це відбувається.

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

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

Простежування формальних доказів до причин небезпек. Аргумент безпеки є повним лише тоді, коли кожен формальний результат явно прив'язаний до причини небезпеки, яку він адресує. Ланцюжок простежуваності виглядає так: формальна властивість → вимога до ПЗ → програмна причина небезпеки → запис аналізу небезпеки системи. Цей ланцюжок має бути задокументований у документі аналізу безпеки ПЗ та перехресно посилатися в пакеті свідчень формальної верифікації. Формальний доказ, що існує без цієї простежуваності, є активом забезпечення якості, але не аргументом безпеки — він демонструє верифікаційну діяльність, не демонструючи вплив на безпеку.

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

Практична інтеграція в оборонний програмний проект

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

Куди інвестувати: критичні алгоритми проти оберток. Прибуток від інвестицій у формальну верифікацію найвищий там, де компонент є математично точним, достатньо малим, щоб бути прийнятно змодельованим, і несе небезпеку з високим ступенем тяжкості. Алгоритми закону управління, логіка планування, послідовності запобіжників та реалізації криптографічних примітивів є канонічними цілями. Навпаки, великі компоненти рівня інтеграції, код інтерфейсу користувача, шари маршалізації даних та логіка управління конфігурацією мають складні інтерфейси та низьку математичну точність — зусилля з написання специфікацій наближаються до зусиль із реалізації, і формальна модель має підтримуватися паралельно з кодом. Обґрунтоване правило: застосовуйте формальні методи там, де поведінку компонента можна специфікувати в менше сторінок, ніж реалізувати, і де специфікована властивість безпосередньо відповідає причині небезпеки в аналізі небезпеки системи.

Вимоги до навичок команди. Інструменти абстрактної інтерпретації є найпростішою точкою входу і повинні впроваджуватися першими. Інженери з досвідом вбудованого C/C++ можуть продуктивно працювати з Astrée або Polyspace після кількох днів навчання; основна навичка — сортування сигналів тривоги: розрізнення справжніх дефектів від хибних спрацьовувань. Перевірка моделей вимагає інженерів, які можуть писати моделі Promela або SMV та виражати властивості в LTL/CTL; ця навичка потребує тижнів або місяців для розвитку, широко не викладається і має бути врахована в планах найму або навчання із самого початку програми. Доведення теорем вимагає досвіду в формальній логіці та теорії доведення, який більшість програм потребуватиме залучати від спеціалізованих організацій, а не розвивати власними силами. Планування кадрового забезпечення формальними методами як запізнілий захід — «ми розберемося з тим, хто виконуватиме формальну верифікацію, коли вона знадобиться» — є найпоширенішою причиною невиконання планів формальних методів.

Реалістичні очікування щодо співвідношення витрат і вигод. Реалістичне очікування для програми, що впроваджує абстрактну інтерпретацію до модулів DAL A, — це зменшення необхідних тест-кейсів для структурного покриття на 15–30%, у рахунок приблизно 5–10% додаткових зусиль інженера на сортування сигналів тривоги та документацію придушень у першому циклі програми. У другому циклі знайомство з патернами сигналів тривоги інструменту для конкретної кодової бази зменшує навантаження на сортування, і чиста вигода покращується. Перевірка моделей для скінченних автоматів додає 10–20% витрат до фази проектування конкретних цільових компонентів, але усуває цілий клас дефектів — порушення скінченних автоматів, помилки протоколів, — які інакше виявлялися б під час інтеграційного тестування або в полі. Доведення теорем є технікою з найвищими витратами та найвищою цінністю і має оцінюватися на покомпонентній основі з явною документацією співвідношення витрат і вигод перед прийняттям зобов'язання.

Абстрактна інтерпретація (Astrée, Polyspace): найнижчий поріг входу, зрілий інструментарій, доступні комплекти DO-330 — застосовувати до всіх модулів DAL A C/C++
Перевірка моделей (SPIN, NuSMV): застосовувати до скінченних автоматів, протоколів та логіки переходів режимів, де простір станів є прийнятним
Доведення теорем (Coq, Isabelle/HOL, PVS, SPARK/GNATprove): резервувати для алгоритмів, де математична правильність є основним аргументом безпеки і жодна інша техніка не є адекватною
Кваліфікація інструментів: планувати DO-330 TQL у PSAC; використовувати комерційні комплекти кваліфікації, де вони доступні; явно бюджетувати кваліфікацію інструментів із відкритим кодом
Простежуваність MIL-STD-882: прив'язувати кожен формальний результат до причини небезпеки перед тим, як заявляти кредит безпеки — непростежувана верифікація не є аргументом безпеки

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

Інтегруйте формальну верифікацію у вашу програму оборонного ПЗ

Corvus Intelligence застосовує формальні методи — абстрактну інтерпретацію, перевірку моделей та доведення теорем — до програм критично важливого оборонного ПЗ, що працюють відповідно до DO-178C та MIL-STD-882. Якщо ваша програма потребує гарантії DAL A або необхідно посилити аргумент безпеки ПЗ, ми готові обговорити ваші вимоги до верифікації.

Розробка оборонного ПЗ → Замовити консультацію

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

Поширені запитання

Що таке формальна верифікація і чим вона відрізняється від тестування ПЗ?

Формальна верифікація використовує техніки математичного доведення для демонстрації того, що програмна система задовольняє точно сформульовану специфікацію, тоді як тестування виконує програму для скінченного набору вхідних даних та спостерігає за виходами. Фундаментальна різниця полягає в повноті: тестування може показати наявність помилок, але не може довести їхню відсутність, оскільки жоден скінченний набір тестів не охоплює всі можливі вхідні дані та стани. Формальна верифікація міркує над повним простором можливих поведінок — коли вона вдається, вона надає гарантію, що виконується для кожного виконання, а не лише для тих, що були перевірені. На практиці це означає, що формальні методи доповнюють тестування, а не замінюють його: вони застосовуються до найбільш критичних властивостей, де вартість невиявлених помилок є найвищою і де структурно неможливо досягти повного тестового покриття. Для критично важливого оборонного ПЗ навіть єдиний невипробуваний шлях, що містить режим відмови, може становити неприйнятний ризик безпеки — і саме цю прогалину адресують формальні методи.

Що таке перевірка моделей і які властивості вона може верифікувати?

Перевірка моделей — це техніка формальної верифікації, яка вичерпно досліджує всі досяжні стани скінченно-автоматної моделі системи, перевіряючи в кожному стані, чи виконується дана властивість, виражена в темпоральній логіці. Властивості лінійної темпоральної логіки (LTL) виражають вимоги щодо послідовностей станів з часом — наприклад, «коли б не був встановлений прапорець увімкнення зброї, запобіжник має бути знятий у попередньому стані». Властивості CTL міркують про розгалужені майбутні — «з будь-якого досяжного стану завжди можна досягти безпечного стану». Типові оборонні застосування включають верифікацію скінченних автоматів протоколів зв'язку, перевірку того, що всі шляхи через граф потоку управління задовольняють даний інваріант безпеки, та підтвердження того, що жодна послідовність допустимих вхідних даних не може привести систему в заборонену конфігурацію. Перевірники моделей, як-от SPIN і NuSMV, видають трасування контрприкладу при невдачі властивості, що робить CEGAR практичним ітеративним робочим процесом.

Що таке проблема вибуху простору станів при перевірці моделей?

Проблема вибуху простору станів — це експоненційне зростання простору станів, який необхідно досліджувати в міру збільшення кількості конкурентних компонентів або змінних даних. Система з N булевими змінними має 2^N можливих станів; система з N конкурентними потоками, кожен з яких має K станів, має K^N комбінованих станів. На практиці навіть невеликі вбудовані системи можуть виробляти простори станів з мільярдами досяжних станів, що вичерпують доступну пам'ять до завершення дослідження. Сучасні перевірники моделей вирішують цю проблему за допомогою Binary Decision Diagrams (BDDs), що символічно представляють множини станів; CEGAR, що уточнює абстракції лише там, де з'являються хибні контрприклади; зменшення часткового порядку, що відсікає еквівалентні чергування конкурентних подій; та обмеженої перевірки моделей, що використовує SAT-вирішувачі для перевірки властивостей до фіксованої довжини шляху — достатньої для більшості властивостей безпеки. Для оборонного ПЗ обмеження обсягу перевірки моделей конкретними критичними підсистемами зберігає простір станів прийнятним, концентруючи верифікаційні зусилля там, де це найбільш важливо.

Що таке доводчики теорем і які з них використовуються у верифікації оборонного ПЗ?

Доводчики теорем — це інструменти, що допомагають інженерам будувати машинно-перевірені математичні докази властивостей ПЗ. На відміну від перевірників моделей, доводчики теорем не обмежені розміром простору станів і можуть міркувати про нескінченні домени — включаючи дійсні числа, необмежені цілі числа та параметризовані алгоритми. Трьома доводчиками, що найчастіше зустрічаються у формальній верифікації в обороні та аерокосмічній галузі, є Coq, Isabelle/HOL та PVS. Механізм вилучення Coq може генерувати сертифікований виконуваний код безпосередньо з верифікованих специфікацій. Isabelle/HOL отримав широке промислове застосування, найбільш помітно в доказі мікроядра seL4. PVS спеціально призначений для специфікації ПЗ і застосовувався до польотного ПЗ NASA та логіки систем ядерної безпеки. Всі три вимагають значної спеціалізованої експертизи та суттєвих початкових інвестицій у написання специфікацій, тому програми, як правило, резервують їх для алгоритмів найвищої критичності, де жодна інша техніка не забезпечує адекватних гарантій.

Що таке абстрактна інтерпретація і як Astrée її використовує?

Абстрактна інтерпретація — це математична основа для обчислення звукових надмірних наближень семантики програм. Замість відстеження точних значень, які може мати змінна, абстрактний інтерпретатор відстежує абстракцію — наприклад, інтервал, в якому гарантовано знаходиться змінна. Якщо абстрактне обчислення завершується без виявлення помилки в будь-якому абстрактному стані, інструмент гарантує, що конкретна програма також вільна від того класу помилок. Astrée застосовує абстрактну інтерпретацію для доведення відсутності помилок часу виконання в програмах на C — переповнення цілих чисел, ділення на нуль, розіменування нульового покажчика, вихід за межі масиву та читання неініціалізованих змінних. Він використовувався для верифікації основного польотного ПЗ Airbus A380 із нульовою кількістю нерозвинених сигналів тривоги. Для вбудованого оборонного ПЗ Astrée та MathWorks Polyspace Code Prover застосовуються для доведення того, що критично важливі модулі ніколи не генерують виняток часу виконання при будь-яких вхідних даних, задовольняючи ключові вимоги DO-178C DAL A та усунення програмних небезпек MIL-STD-882.

Як DO-178C враховує формальні методи?

DO-178C включає додаток з формальних методів — DO-333 (Formal Methods Supplement to DO-178C and DO-278A), — що визначає, як заходи формального аналізу можуть задовольняти цілі верифікації DO-178C. Відповідно до DO-333, формальний метод може надавати кредит для вимог структурного покриття: доказ того, що властивість виконується для всіх досяжних станів, надає еквівалентну гарантію MC/DC-покриттю відповідних шляхів коду, за умови, що формальний метод є звуковим, а властивість показана як така, що передбачає вимогу безпеки. Додаток вимагає, щоб формальна модель точно представляла реалізацію, всі припущення були явно сформульовані та обґрунтовані, а інструменти, що використовуються, були кваліфіковані відповідно до DO-330. Формальні методи доповнюють, а не замінюють тестування відповідно до DO-178C — вони зменшують навантаження тестування для конкретних цілей, збільшуючи глибину гарантії для формально аналізованих властивостей. PSAC повинен описувати підхід до формальних методів із самого початку програми.

Як MIL-STD-882 пов'язує формальну верифікацію із кредитом зниження небезпеки?

MIL-STD-882E визначає матрицю ризику на основі тяжкості небезпеки та ймовірності виникнення, з переважною ієрархією пом'якшення: усунути небезпеку, знизити ймовірність, додати виявлення та попередження, а потім прийняти залишковий ризик. Формальна верифікація сприяє двом першим рівням. Доказ перевірки моделей про те, що логіка випуску зброї ніколи не може спрацювати без одночасного знятого запобіжника та підтвердження оператора у правильному порядку, становить усунення небезпеки для програмного причинного шляху тієї небезпеки. Де усунення неможливе, звуковий доказ абстрактної інтерпретації, що обмежує рівень збоїв, спричинених ПЗ, надає докази кредиту зниження ймовірності, заявленого в аналізі небезпеки. Ключовим кроком документування є простежування кожного формального результату до конкретної причини небезпеки в аналізі небезпеки системи — ця простежуваність перетворює верифікаційну діяльність у визнаний аргумент безпеки.

Яке реалістичне співвідношення витрат і вигод від формальної верифікації в оборонній програмі?

Формальна верифікація несе значні початкові витрати: побудова формальних моделей, написання специфікацій, навчання інженерів та кваліфікація інструментів для регуляторного кредиту. Переваги є значними, але нерівномірно розподіленими: формальні методи мають велику цінність для невеликих, математично точних компонентів — алгоритмів планування, скінченних автоматів, логіки запобіжників, — і низьку цінність для великого коду інтеграції, де специфікація була б такою ж складною, як і реалізація. Реалістичні очікування: абстрактна інтерпретація додає 5–10% зусиль інженера, відшкодовуючи зниження необхідних тест-кейсів на 15–30%; перевірка моделей додає 10–20% витрат фази проектування для цільових скінченних автоматів, але усуває цілий клас дефектів, що виявляються інакше під час інтеграційного тесту; доведення теорем несе найвищі витрати і має оцінюватися покомпонентно з явним обґрунтуванням перед прийняттям зобов'язання. Програми, що вибірково застосовують формальні методи до правильних компонентів, окупають свої інвестиції; програми, що застосовують їх безрозбірно, перевищують графік і бюджет.

Яка кваліфікація інструментів потрібна при використанні інструментів формального аналізу для кредиту DO-178C?

§12.2 DO-178C вимагає кваліфікації програмних інструментів, коли їхній вихід використовується без незалежної верифікації. DO-330 визначає рівні кваліфікації інструментів (TQL-1 — TQL-5) залежно від ролі інструменту та рівня гарантії розробки. Інструмент формального аналізу, що використовується для задоволення цілі верифікації DO-178C DAL A, відповідає TQL-1 або TQL-2, вимагаючи найбільш суворих артефактів кваліфікації: вимог до роботи інструменту, плану кваліфікації інструменту, резюме виконання кваліфікації та свідчень правильних результатів для відповідного випадку використання. Комерційні інструменти, як-от Astrée та Polyspace, постачають наявні комплекти кваліфікації, що зменшують навантаження програми до демонстрації того, що комплект застосовується до їхнього конкретного контексту використання та конфігурації компілятора. Інструменти з відкритим кодом зазвичай вимагають повної кваліфікації з нуля — суттєвих програмних витрат, що мають бути включені в план проекту із самого початку.

Які навички команди потрібні для впровадження формальної верифікації в оборонну команду з розробки ПЗ?

Інструменти абстрактної інтерпретації, як-от Astrée та Polyspace, є найпростішою точкою входу і можуть використовуватися інженерами з досвідом C/C++ після кількох днів навчання — основна навичка полягає в сортуванні сигналів тривоги: розрізненні справжніх дефектів від хибних спрацьовувань через неточність абстракції. Перевірка моделей за допомогою SPIN або NuSMV вимагає інженерів, які можуть писати специфікації в Promela або SMV та виражати властивості в LTL/CTL — навичка, що потребує тижнів або місяців для розвитку, не викладається в стандартних навчальних програмах та має бути врахована в планах найму або навчання із самого початку програми. Доведення теорем з Coq, Isabelle/HOL або PVS вимагає глибокої експертизи в формальній логіці та теорії доведення — навичок, які більшість програм потребуватиме залучати від спеціалізованих організацій. Найбільш практичний шлях кадрового забезпечення — спершу впровадити абстрактну інтерпретацію, навчити інженерів перевірці моделей для верифікації скінченних автоматів та зарезервувати доведення теорем для залученої спеціалізованої роботи з компонентами найвищої критичності.