Formalna weryfikacja oprogramowania obronnego o kluczowym znaczeniu dla bezpieczeństwa: metody, narzędzia i gwarancje

Autor: Corvus Intelligence Engineering Team · O zespole →

25 czerwca 2026 13 min czytania

Każdy program weryfikacji oprogramowania napotyka w końcu ten sam strukturalny problem: testowanie jest ograniczone. Zestaw testów, niezależnie od swojej wielkości, sprawdza skończony podzbiór danych wejściowych i ścieżek wykonania. Pozostałe, niesprawdzone kombinacje stanowią domyślne założenie, że nieprzetestowane zachowanie jest poprawne. W przypadku większości komercyjnego oprogramowania założenie to jest akceptowalne; koszt wykrytego defektu jest możliwy do odzyskania. Dla bezpieczeństwa oprogramowania w systemach obronnych — kodu sterującego bronią, powierzchniami sterującymi lotu lub funkcjami podtrzymania życia — jeden defekt na nieprzetestowanej ścieżce może być katastrofalny. Formalna weryfikacja eliminuje tę lukę nie poprzez uruchamianie kolejnych testów, lecz zastępując dowody oparte na wykonaniu dowodem matematycznym.

Metody formalne obejmują rodzinę technik — model checking, dowodzenie twierdzeń i interpretację abstrakcyjną — które rozumują matematycznie nad pełną przestrzenią możliwych zachowań programu. Każda z nich oferuje inny kompromis między ekspresywnością, automatyzacją, skalowalnością i siłą udzielanej gwarancji. Niniejszy artykuł analizuje każdą technikę w kontekście opracowywania oprogramowania obronnego, wyjaśnia, jak integrują się z certyfikacją DO-178C DAL A i analizą bezpieczeństwa MIL-STD-882, oraz przedstawia realistyczną ocenę tego, gdzie metody formalne opłacają się, a gdzie nie.

Dlaczego samo testowanie nie zapewnia gwarancji bezpieczeństwa

Ograniczenia testowania jako jedynej strategii weryfikacji nie wynikają głównie z liczby testów — mają charakter strukturalny. Trzy problemy zbiegają się, czyniąc gwarancję opartą wyłącznie na testach niewystarczającą dla systemów o krytycznym znaczeniu dla bezpieczeństwa.

Pułap pokrycia. Metryki pokrycia strukturalnego — pokrycie instrukcji, pokrycie gałęzi, Modified Condition/Decision Coverage (MC/DC) — mierzą odsetek struktur kodu sprawdzonych przez zestaw testów. DO-178C wymaga pokrycia MC/DC dla oprogramowania DAL A, ponieważ zapewnia ono, że każdy wynik decyzji i każdy warunek w każdej decyzji są niezależnie demonstrowane jako wpływające na wynik. Jednak nawet 100% pokrycia MC/DC nie wyczerpuje przestrzeni wejściowej: funkcja z pięcioma 32-bitowymi parametrami całkowitoliczbowymi ma 2¹⁶⁰ możliwych kombinacji wejściowych. Zestaw testów wykazujący 100% pokrycia MC/DC może obejmować dziesiątki lub setki ścieżek wykonania, lecz nic nie mówi o poprawności wykonań łączących określone wartości wejściowe w niesprawdzony sposób. Pułap pokrycia nie jest problemem jakości testów — jest matematycznym faktem dotyczącym skończonego testowania nieskończonych przestrzeni.

Eksplozja kombinatoryczna w systemach współbieżnych. Oprogramowanie obronne o kluczowym znaczeniu dla bezpieczeństwa jest prawie zawsze współbieżne: wiele zadań wykonywanych równolegle, współdzielących pamięć, wymieniających komunikaty przez kolejki i semafory, podatnych na przerwania mogące wywłaszczać wykonanie w dowolnych punktach. Liczba możliwych przeplotów N współbieżnych zadań z K krokami każde rośnie jako O(K^N). System z trzema zadaniami po dziesięć kroków każde ma ponad miliard możliwych przeplotów. Testowanie sprawdza garstkę z nich; metryki pokrycia nic nie mówią o niesprawdzonych przeplotnach. Wyścigi danych, inwersje priorytetów i zakleszczenia ukrywają się w przeplotnach, których testowanie przypadkowo nie sprawdza.

Rola metod formalnych. Formalna weryfikacja rozwiązuje te problemy, zastępując wyliczanie dowodem. Zamiast pytać „czy system zachował się poprawnie dla tych danych wejściowych?", pyta „czy jest matematycznie niemożliwe, aby system zachował się niepoprawnie dla jakichkolwiek danych wejściowych?" To pytanie jest trudniejsze i droższe w odpowiedzi, lecz odpowiedź — gdy jest pozytywna — jest kategorycznie silniejsza. Dlatego przemysł lotniczy, jądrowy i sektor obronny nakazują lub zachęcają do stosowania metod formalnych na najwyższych poziomach gwarancji projektowej: testowanie buduje zaufanie; formalna weryfikacja ustanawia pewność w granicach modelu formalnego i jego założeń.

Dziedzina towarzysząca — statyczna analiza kodu oprogramowania obronnego — plasuje się między testowaniem a formalną weryfikacją: narzędzia analizy statycznej badają kod źródłowy bez jego wykonywania, identyfikując klasy defektów pomijane przez testowanie, ale zazwyczaj bez matematycznych gwarancji poprawności oferowanych przez metody formalne.

Model checking: wyczerpująca weryfikacja przestrzeni stanów

Model checking jest najszerzej stosowaną techniką formalnej weryfikacji oprogramowania obronnego, ponieważ jest najbardziej zautomatyzowana. Mając formalny model systemu i właściwość wyrażoną w logice temporalnej, model checker wyczerpująco bada wszystkie osiągalne stany i potwierdza, że właściwość zachodzi w każdym z nich — lub generuje kontrprzykład demonstrując naruszenie.

Właściwości logiki temporalnej dla systemów obronnych. Linear Temporal Logic (LTL) i Computation Tree Logic (CTL) to dwa podstawowe języki właściwości używane w model checking. Właściwości LTL wyrażają ograniczenia na poszczególnych ścieżkach wykonania. Typowa właściwość bezpieczeństwa obronnego: globalnie, ilekroć system wchodzi w stan uzbrojenia, w następnym stanie zarówno blokada bezpieczeństwa musi zostać zwolniona, jak i potwierdzenie operatora musi być obecne. Właściwości CTL rozumują o rozgałęziających się drzewach obliczeń — wyrażając na przykład, że ścieżka odtwarzania zawsze istnieje z dowolnego osiągalnego stanu. Aplikacje obronne obejmują weryfikację, czy automaty stanów protokołów komunikacyjnych nigdy nie wchodzą w niezdefiniowane stany, czy logika planowania zawsze dotrzymuje terminów przy dowolnym prawidłowym porządkowaniu zadań i czy sekwencje blokad bezpieczeństwa nie mogą zostać obejdzie przez żadną kombinację prawidłowych danych wejściowych.

Narzędzia: SPIN i NuSMV. SPIN jest model checkerem opartym na jawnych stanach, stosowanym głównie do weryfikacji współbieżnego oprogramowania i protokołów komunikacyjnych. Jego język wejściowy, Promela, modeluje współbieżne procesy komunikujące się przez kanały komunikatów; właściwości są wyrażone w LTL. SPIN weryfikuje przez przeszukiwanie w głąb z hashowym przechowywaniem stanów i generuje ślady kontrprzykładów, które można odtworzyć w symulatorze. NuSMV jest symbolicznym model checkerem używającym Binary Decision Diagrams (BDDs) i ograniczonego model checking z solwerami SAT do symbolicznego reprezentowania i eksploracji zbiorów stanów — co czyni go skutecznym dla systemów z dużymi przestrzeniami stanów, gdzie jawne wyliczenie jest niewykonalne. W przypadku protokołów i automatów stanów oprogramowania obronnego SPIN jest zazwyczaj bardziej odpowiedni; dla osadzonej logiki sterowania modelowanej na poziomie rejestrów, symboliczne podejście NuSMV jest często bardziej praktyczne.

Problem eksplozji stanów i CEGAR. Przestrzeń osiągalnych stanów rośnie wykładniczo wraz z rozmiarem systemu. Counterexample-Guided Abstraction Refinement (CEGAR) jest podstawową praktyczną techniką zarządzania tym zjawiskiem. Przepływ pracy zaczyna się od zgrubnego modelu abstrakcyjnego, który jest wystarczająco mały, by go zweryfikować, ale może wprowadzać pozorne zachowania nieobecne w konkretnym systemie. Jeśli właściwość zachodzi na modelu abstrakcyjnym, zachodzi też na systemie konkretnym dzięki poprawności abstrakcji. Jeśli znaleziono kontrprzykład, jest on sprawdzany względem modelu konkretnego: jeśli model konkretny również wykazuje kontrprzykład, jest to rzeczywisty defekt; jeśli nie, abstrakcja jest udoskonalana przez dodanie większej liczby szczegółów w obszarze, gdzie pojawił się pozorny kontrprzykład. CEGAR jest iteracyjny i może zbiegać do wyniku weryfikacji bez jawnego reprezentowania pełnej przestrzeni stanów.

/* SPIN Promela fragment: blokada zwolnienia broni */
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
}

/* Właściwość LTL: zwolnienie tylko gdy oba warunki wstępne spełnione */
ltl p1 { [] (release_state == RELEASED ->
              (safety_state == ARMED && confirm_state == RELEASED)) }

Gdy model checker wykryje naruszenie właściwości, generuje ślad kontrprzykładu — kompletną sekwencję stanów systemu od stanu początkowego do stanu naruszającego. Ślad ten jest bezpośrednio użyteczny: precyzyjnie określa, która sekwencja zdarzeń prowadzi do niebezpiecznego stanu, umożliwiając programistom deterministyczne odtworzenie awarii i zaprojektowanie poprawki. Kontrprzykłady znalezione w udokumentowanej weryfikacji protokołów C2 ujawniły obejścia uwierzytelniania możliwe tylko przy określonych kombinacjach opóźnień komunikatów i retransmisji — scenariusze nigdy niesprawdzane podczas miesięcy testów integracyjnych.

Dowodzenie twierdzeń: matematyczne dowody weryfikowane maszynowo

Tam gdzie model checking wyczerpuje ograniczoną przestrzeń stanów automatycznie, dowodzenie twierdzeń konstruuje matematyczny dowód właściwości zachodzącej w nieograniczonej lub sparametryzowanej dziedzinie — czyniąc je techniką z wyboru, gdy weryfikowana właściwość obejmuje arytmetykę liczb rzeczywistych, nieograniczone struktury danych lub sparametryzowane algorytmy, których żadna skończona przestrzeń stanów nie może reprezentować.

Coq, Isabelle/HOL i PVS w zastosowaniach obronnych. Coq jest asystentem dowodzenia opartym na teorii typów zależnych; jego mechanizm ekstrakcji może generować zweryfikowany kod wykonywalny bezpośrednio ze specyfikacji, która została dowiedziona jako poprawna, tworząc łańcuch od dowodu do działającego pliku binarnego. Był używany do weryfikacji algorytmów kryptograficznych i transformacji kompilatorów. Isabelle/HOL zapewnia środowisko logiki wyższego rzędu z potężnymi taktykami automatyzacji; jego przemysłowe zastosowanie obejmuje dowód mikrojądra seL4 — najbardziej wszechstronnie zweryfikowanego jądra systemu operacyjnego, jakie kiedykolwiek istniało — wykazując, że plik binarny wykonywalny poprawnie implementuje jego formalną specyfikację. PVS, opracowany w SRI International, został zaprojektowany specjalnie do specyfikacji oprogramowania i był stosowany do oprogramowania lotniczego NASA i logiki systemów bezpieczeństwa jądrowego. Każdy z tych systemów był używany w kontekstach obronnych: Coq do dowodów protokołów i algorytmów, Isabelle do oprogramowania systemowego i platformowego, PVS do rozumowania na poziomie specyfikacji w systemach awioniki i kosmicznych.

Generowanie zobowiązań dowodowych. Nowoczesne przepływy pracy metod formalnych automatycznie generują zobowiązania dowodowe z adnotowanego kodu źródłowego, zmniejszając obciążenie związane z pisaniem specyfikacji od zera. Narzędzia takie jak Frama-C z wtyczką WP (Weakest Precondition) analizują kod C adnotowany kontraktami ACSL (ANSI/ISO C Specification Language) i generują zobowiązania dowodowe, które mogą być rozwiązywane przez automatyczne prowersy (Alt-Ergo, CVC4, Z3) lub przez interaktywne prowersy twierdzeń, gdy automatyzacja zawodzi. Język SPARK dla Ada zapewnia podobny zintegrowany przepływ pracy: kod SPARK jest pisany z kontraktami pre/postcondition, a GNATprove generuje i próbuje automatycznie rozwiązać zobowiązania dowodowe, eskalując do interaktywnego dowodzenia tylko dla zobowiązań, których automatyzacja nie może obsłużyć. To hybrydowe podejście — maksymalizacja automatyzacji przy jednoczesnym zachowaniu dowodzenia prowadzonego przez człowieka dla trudnych przypadków — jest praktycznym modelem dla programów obronnych, które nie mogą zatrudnić zespołu teoretyków dowodów.

Kompromis związany z krzywą uczenia się. Przepaść między wartością, jaką dowodzenie twierdzeń może dostarczyć, a inwestycją organizacyjną jest głównym wyzwaniem przy wdrażaniu tej techniki. Pisanie specyfikacji w Coq lub Isabelle wymaga biegłości w logice wyższego rzędu i teorii typów, których standardowe wykształcenie inżynierskie nie zapewnia. Tworzenie dowodów mierzone jest w miesiącach inżynierskich dla nietrywialnych komponentów. Programy, które nie doceniają tej inwestycji, systematycznie przekraczają harmonogram. Realistyczna ścieżka to zakup specjalistycznych prac nad dowodzeniem twierdzeń od organizacji, które już posiadają tę zdolność, i ograniczenie zakresu do komponentów, gdzie żadna inna technika nie jest wystarczająca — zazwyczaj algorytmów, na których opiera się przypadek bezpieczeństwa.

Interpretacja abstrakcyjna i poprawna analiza statyczna

Interpretacja abstrakcyjna zajmuje praktyczne miejsce pośrednie między konwencjonalną analizą statyczną (która typowo generuje niepewne wyniki — może pomijać błędy) a dowodzeniem twierdzeń (które jest poprawne, lecz wymaga wysiłku manualnego). Narzędzie do interpretacji abstrakcyjnej oblicza poprawne nadprzyliżenie: jeśli nie zgłasza żadnego błędu, konkretny program jest gwarantowany jako wolny od błędów tej klasy. Jeśli zgłasza potencjalny błąd, program może, lecz nie musi go zawierać — zgłoszenie jest konserwatywnym alarmem, który należy zbadać.

Astrée. Astrée (opracowane w ENS Paris/INRIA i skomercjalizowane przez AbsInt) jest najbardziej prominentnym narzędziem do interpretacji abstrakcyjnej w kontekstach obronnych i lotniczych. Analizuje kod C pod kątem następujących klas błędów wykonania: przepełnienie i niedomiar liczb całkowitych (ze znakiem i bez znaku), dzielenie przez zero, wyłuskanie wskaźnika NULL, dostęp do tablicy poza granicami, nieprawidłowe liczby przesunięć bitowych i odczyty niezainicjalizowanych zmiennych. Zostało użyte do dowiedzenia braku błędów wykonania w podstawowym oprogramowaniu lotniczym Airbusa A380 — około 132 000 linii C z zerową liczbą nierozwiązanych alarmów po analizie. W przypadku osadzonego oprogramowania obronnego Astrée jest stosowane na poziomie modułu; każdy moduł musi osiągnąć zero rzeczywistych alarmów, zanim zostanie uznany za formalnie zweryfikowany pod kątem braku błędów wykonania.

Polyspace firmy MathWorks. Polyspace Bug Finder i Polyspace Code Prover zapewniają podobne możliwości interpretacji abstrakcyjnej, z ściślejszą integracją z łańcuchem narzędzi MathWorks (MATLAB/Simulink model-based development) powszechnie stosowanym w osadzonych systemach obronnych. Code Prover używa interpretacji abstrakcyjnej opartej na przedziałach do dowiedzenia — nie tylko wykrycia — braku określonych klas błędów i klasyfikuje każde sprawdzenie jako Proven (żaden błąd nie jest możliwy), Unproven (nie można określić) lub Error (defekt potwierdzony). Zarówno Astrée, jak i Polyspace dostarczają zestawy do kwalifikacji narzędzi zgodnie z DO-330, zmniejszając obciążenie artefaktami programu dla kredytu regulacyjnego.

Klasa błędu	Astrée	Polyspace Code Prover	Poprawność
Przepełnienie / niedomiar liczb całkowitych	Tak	Tak	Poprawny (brak pominięć)
Wyłuskanie wskaźnika NULL	Tak	Tak	Poprawny (brak pominięć)
Dzielenie przez zero	Tak	Tak	Poprawny (brak pominięć)
Dostęp do tablicy poza granicami	Tak	Tak	Poprawny (brak pominięć)
Odczyty niezainicjalizowanych zmiennych	Tak	Tak	Poprawny (brak pominięć)

Zarządzanie fałszywymi alarmami. Narzędzia poprawne raportują konserwatywnie: gdy niepewne, alarmują. W dużych bazach kodu C ze złożoną arytmetyką wskaźników, stubami środowiska dla niezmodelowanych interfejsów sprzętowych lub rozszerzeniami kompilatora specyficznymi dla platformy, wskaźniki fałszywych alarmów mogą być wysokie — 30–70% w pierwszym uruchomieniu nie jest niczym niezwykłym. Dyscypliną jest adnotowanie każdego fałszywego alarmu maszynoczytelnym uzasadnieniem, które narzędzie akceptuje jako tłumienie, tak aby stłumiony alarm nie pojawiał się w kolejnych uruchomieniach. Każde tłumienie jest twierdzeniem — „ten alarm nie może wystąpić w czasie wykonania, ponieważ [powód]" — i twierdzenia muszą być przeglądane podczas inspekcji kodu jako część argumentu bezpieczeństwa. Dziennik tłumień sam w sobie jest artefaktem bezpieczeństwa; moduł z wysoką liczbą tłumień wymaga dodatkowej kontroli.

Stosowanie metod formalnych do oprogramowania DO-178C DAL A

DO-178C, podstawowy standard certyfikacji oprogramowania lotniczego i standard najczęściej stosowany przez analogię do innych platform obronnych o kluczowym znaczeniu dla bezpieczeństwa, zawiera suplement metod formalnych — DO-333 (Formal Methods Supplement to DO-178C and DO-278A) — który definiuje, w jaki sposób działania w zakresie analizy formalnej mogą spełniać cele weryfikacji DO-178C.

Suplement a zastępstwo testowania. Powszechnym nieporozumieniem jest to, że formalna weryfikacja eliminuje potrzebę testowania w ramach DO-178C. DO-333 nie wspiera tego poglądu. Metody formalne są suplementem: mogą zapewniać kredyt dla określonych celów weryfikacji, które w przeciwnym razie spełniałoby testowanie, zmniejszając zakres testowania, ale nie zastępują całego wymagania testowego. Typowym zastosowaniem jest użycie analizy formalnej do spełnienia celów pokrycia strukturalnego — poprawny dowód interpretacji abstrakcyjnej, że żaden błąd wykonania nie jest osiągalny w module, zapewnia równoważną gwarancję z wykonaniem każdej gałęzi tego modułu i może być uznany jako kredyt pokrycia — podczas gdy konwencjonalne testowanie nadal spełnia cele testowania opartego na wymaganiach. Efektem netto jest zmniejszony rozmiar zestawu testów dla modułów DAL A przy zwiększonej głębokości gwarancji dla właściwości, które celuje analiza formalna.

Dokumentacja PSAC i SAS. Plan dotyczący aspektów certyfikacji oprogramowania (PSAC) musi opisywać podejście do metod formalnych od początku programu: jakie metody formalne są stosowane, jakie cele DO-178C adresują, jakich narzędzi się używa i jak narzędzia zostaną zakwalifikowane. Ten artefakt planowania jest przeglądany przez organ certyfikujący przed rozpoczęciem prac nad formalną weryfikacją — przedstawianie roszczenia dotyczącego metod formalnych certyfikatorowi dopiero po zakończeniu jest błędem procesu, który może unieważnić kredyt. Podsumowanie osiągnięć oprogramowania (SAS) dokumentuje działania formalnej weryfikacji jako zakończone i zapewnia możliwość śledzenia od każdego formalnego wyniku do celu DO-178C, który spełnia. Dowody formalnej weryfikacji — wyniki uruchomień narzędzi, pliki właściwości, pliki modeli, rejestry dyspozycji alarmów — są zachowywane w systemie zarządzania konfiguracją jako część danych cyklu życia certyfikacji.

Kwalifikacja narzędzi. DO-330 definiuje wymagania kwalifikacyjne dla narzędzi programowych używanych w tworzeniu oprogramowania lotniczego. Narzędzia generujące wyniki używane bez niezależnej weryfikacji w rekordzie zgodności wymagają kwalifikacji stosownej do DAL i roli narzędzia. Narzędzia do interpretacji abstrakcyjnej używane do spełnienia celów weryfikacji DAL A wymagają kwalifikacji TQL-1 — najbardziej rygorystycznego poziomu. Komercyjne narzędzia, takie jak Astrée i Polyspace, dostarczają zestawy wsparcia kwalifikacji obejmujące wymagania operacyjne narzędzi, procedury testów kwalifikacyjnych i wyniki testów kwalifikacyjnych. Odpowiedzialnością programu jest ustalenie, że zestaw ma zastosowanie do jego kontekstu użycia: konkretnego kompilatora, systemu operacyjnego i podzbioru języka w użyciu. Narzędzia open-source bez istniejących zestawów kwalifikacyjnych wymagają od programu wygenerowania wszystkich artefaktów kwalifikacyjnych od zera — co jest znacznym kosztem programu, który musi być uwzględniony w planie projektu od pierwszego dnia.

Kluczowa zasada DO-178C / DO-333: Kredyt metod formalnych w rekordzie zgodności jest uzyskiwany dzięki jakości argumentu identyfikowalności — wykazaniu, że zweryfikowana właściwość formalna odpowiada dokładnie wymaganiu bezpieczeństwa, które ma spełniać. Formalnie zweryfikowana właściwość, która tylko w przybliżeniu ujmuje wymaganie, nie zapewnia kredytu regulacyjnego i może osłabiać, a nie wzmacniać przypadek bezpieczeństwa.

Eliminacja zagrożeń MIL-STD-882 a formalna weryfikacja

MIL-STD-882E (System Safety) definiuje preferowaną hierarchię kontroli zagrożeń w malejącej kolejności skuteczności: eliminacja zagrożenia, zmniejszenie prawdopodobieństwa wystąpienia, dodanie wykrywania lub ostrzeżenia i akceptacja ryzyka szczątkowego z udokumentowanym uzasadnieniem. Formalna weryfikacja bezpośrednio przyczynia się do pierwszych dwóch poziomów i zapewnia najbardziej uzasadniony argument bezpieczeństwa, gdy tak się dzieje.

Eliminacja zagrożeń poprzez dowód niemożliwości. Gdy dowód model checking wykazuje, że właściwość temporalna zachodzi dla wszystkich osiągalnych stanów — na przykład, że obwód zapalnika nigdy nie może być pobudzony, gdy flaga blokady bezpieczeństwa jest potwierdzona — stanowi twierdzenie o eliminacji zagrożenia dla ścieżki przyczynowej oprogramowania tego zagrożenia. Wpis w rejestrze zagrożeń dla odpowiedniego zagrożenia może być zaktualizowany, aby odzwierciedlić, że ścieżka przyczynowa oprogramowania została wyeliminowana przez dowód formalny, a ocena ryzyka szczątkowego odzwierciedla tylko ścieżki przyczynowe sprzętu, które pozostają nierozwiązane. Jest to kategorycznie silniejsze niż argument redukcji ryzyka z testowania, który może jedynie ustalić, że zagrożenie nie zostało wywołane podczas przebiegów testowych.

Kredyt redukcji prawdopodobieństwa z poprawnej analizy. Tam gdzie eliminacja nie jest osiągalna — ponieważ zagrożenie zależy od warunków poza kontrolą oprogramowania — analiza formalna zapewnia ograniczenie wkładu oprogramowania w prawdopodobieństwo awarii. Dowód interpretacji abstrakcyjnej, że przepełnienie liczby całkowitej nie może wystąpić w algorytmie nawigacyjnym, ogranicza wskaźnik cichego uszkodzenia danych do zera dla tej klasy błędów, bezpośrednio zmniejszając składnik wskaźnika awarii oprogramowania w probabilistycznej ocenie ryzyka. To ograniczenie jest bardziej uzasadnione niż szacunek wskaźnika awarii oparty na testach, ponieważ formalne ograniczenie jest dokładne w granicach założeń modelu, podczas gdy szacunek oparty na testach jest przedziałem ufności dla skończonej próby.

Śledzenie formalnych dowodów do przyczyn zagrożeń. Argument bezpieczeństwa jest kompletny tylko wtedy, gdy każdy formalny wynik jest jawnie powiązany z przyczyną zagrożenia, którą adresuje. Łańcuch identyfikowalności przebiega: właściwość formalna → wymaganie oprogramowania → przyczyna zagrożenia oprogramowania → wpis w Analizie zagrożeń systemu. Łańcuch ten musi być udokumentowany w dokumencie Analizy bezpieczeństwa oprogramowania i wzajemnie odesłany w pakiecie dowodów formalnej weryfikacji. Formalny dowód istniejący bez tej identyfikowalności jest aktywem zapewnienia jakości, ale nie argumentem bezpieczeństwa — wykazuje działanie weryfikacyjne bez wykazania wpływu na bezpieczeństwo.

Łączenie wyników formalnej weryfikacji z szerszą dziedziną DevSecOps dla rurociągów obronnych oznacza, że uruchomienia analizy formalnej mogą być zintegrowane z rurociągiem ciągłej integracji jako automatyczne bramy — blokujące integrację każdego modułu, który wprowadza nowe nierozwiązane alarmy — zamiast być wykonywane tylko jako działania certyfikacyjne na późnym etapie.

Praktyczna integracja w projekcie oprogramowania obronnego

Głównym wyzwaniem przy wprowadzaniu formalnej weryfikacji do projektu oprogramowania obronnego nie jest kwestia techniczna — narzędzia istnieją, a techniki są dojrzałe. Jest to kwestia alokacji zasobów: metody formalne wymagają inwestycji, która musi być uzasadniona wobec konkurujących priorytetów programu, a inwestycja jest skoncentrowana na początku, podczas gdy korzyści są realizowane późno.

Gdzie inwestować: algorytmy krytyczne a opakowania. Zwrot z inwestycji w formalną weryfikację jest najwyższy tam, gdzie komponent jest matematycznie precyzyjny, wystarczająco mały, aby być modelowanym w sposób praktyczny, i niesie zagrożenie o wysokiej wadze. Algorytmy prawa sterowania, logika planowania, sekwencjonowanie blokad bezpieczeństwa i implementacje kryptograficznych prymitywów są kanonicznymi celami. I odwrotnie, duże komponenty warstwy integracyjnej, kod interfejsu użytkownika, warstwy porządkowania danych i logika zarządzania konfiguracją mają złożone interfejsy i niską precyzję matematyczną — wysiłek pisania specyfikacji zbliża się do wysiłku implementacji, a model formalny musi być utrzymywany równolegle z kodem. Praktyczna zasada: stosuj metody formalne tam, gdzie zachowanie komponentu można określić na mniejszej liczbie stron niż je zaimplementować, i gdzie określona właściwość odpowiada bezpośrednio przyczynie zagrożenia w Analizie zagrożeń systemu.

Wymagania dotyczące umiejętności zespołu. Narzędzia do interpretacji abstrakcyjnej są punktem wejścia o najniższej barierze i powinny być wprowadzane jako pierwsze. Inżynierowie ze środowisk osadzonych C/C++ mogą produktywnie obsługiwać Astrée lub Polyspace po kilku dniach szkolenia; podstawową umiejętnością jest sortowanie alarmów — rozróżnianie rzeczywistych defektów od fałszywych alarmów. Model checking wymaga inżynierów, którzy potrafią pisać modele Promela lub SMV i wyrażać właściwości w LTL/CTL; ta umiejętność zajmuje tygodnie lub miesiące do rozwinięcia, nie jest powszechnie nauczana i powinna być uwzględniana w planach rekrutacyjnych lub szkoleniowych od początku programu. Dowodzenie twierdzeń wymaga wiedzy specjalistycznej z zakresu logiki formalnej i teorii dowodów, którą większość programów będzie musiała zlecać specjalistycznym organizacjom, a nie rozwijać wewnętrznie. Planowanie obsady metod formalnych jako afterthought — „zobaczymy, kto zajmie się formalną weryfikacją, gdy będzie potrzebna" — jest jedyną najczęstszą przyczyną niewykonywania planów metod formalnych.

Realistyczne oczekiwania dotyczące kosztów i korzyści. Realistyczne oczekiwanie dla programu wprowadzającego interpretację abstrakcyjną do modułów DAL A to 15–30% redukcja wymaganych przypadków testowych dla pokrycia strukturalnego, zrównoważona przez około 5–10% dodatkowego wysiłku inżynierskiego na sortowanie alarmów i dokumentację tłumień w pierwszym cyklu programu. W drugim cyklu znajomość wzorców alarmów narzędzia dla konkretnej bazy kodu zmniejsza obciążenie sortowaniem, a korzyść netto poprawia się. Model checking dla automatów stanów dodaje 10–20% kosztów do fazy projektowania określonych komponentów docelowych, ale eliminuje całą klasę defektów — naruszenia automatów stanów, błędy protokołów — które w przeciwnym razie byłyby wykrywane w testach integracyjnych lub w terenie. Dowodzenie twierdzeń jest techniką o najwyższym koszcie i najwyższej wartości i powinno być oceniane na zasadzie per-komponent z jawną dokumentacją kosztów i korzyści przed zobowiązaniem.

Interpretacja abstrakcyjna (Astrée, Polyspace): najniższa bariera, dojrzałe narzędzia, dostępne zestawy DO-330 — stosuj do wszystkich modułów DAL A C/C++
Model checking (SPIN, NuSMV): stosuj do automatów stanów, protokołów i logiki przejść trybu, gdzie przestrzeń stanów jest praktyczna
Dowodzenie twierdzeń (Coq, Isabelle/HOL, PVS, SPARK/GNATprove): rezerwuj dla algorytmów, gdzie matematyczna poprawność jest głównym argumentem bezpieczeństwa i żadna inna technika nie jest wystarczająca
Kwalifikacja narzędzi: planuj DO-330 TQL w PSAC; używaj komercyjnych zestawów kwalifikacyjnych tam, gdzie są dostępne; wyraźnie budżetuj kwalifikację narzędzi open-source
Identyfikowalność MIL-STD-882: śledź każdy formalny wynik do przyczyny zagrożenia przed zgłoszeniem kredytu bezpieczeństwa — nieidentyfikowalna weryfikacja nie jest argumentem bezpieczeństwa

Programy, które z powodzeniem integrują formalną weryfikację, traktują ją jako pierwszorzędną dyscyplinę inżynierską z dedykowanym personelem, planowaną kwalifikacją narzędzi, jawną identyfikowalnością wymagań i realistycznym zakresem ograniczonym do komponentów, gdzie metody formalne zmieniają klasyfikację bezpieczeństwa zagrożenia. Programy, które traktują formalną weryfikację jako pole wyboru zgodności do dodania na końcu opracowywania, konsekwentnie stwierdzają, że analiza formalna nie wspiera roszczenia o zgodność, ponieważ kod nie był projektowany z myślą o analizie formalnej. Projekt i model formalny muszą być współrozwijane — dyscyplina specyfikacji, której wymagają metody formalne, jest równie cenna jak sam dowód.

Zintegruj formalną weryfikację z programem oprogramowania obronnego

Corvus Intelligence stosuje metody formalne — interpretację abstrakcyjną, model checking i dowodzenie twierdzeń — do programów oprogramowania obronnego o kluczowym znaczeniu dla bezpieczeństwa działających w ramach DO-178C i MIL-STD-882. Jeśli Twój program wymaga gwarancji DAL A lub musi wzmocnić argument bezpieczeństwa oprogramowania, jesteśmy dostępni, aby omówić Twoje wymagania weryfikacyjne.

Tworzenie oprogramowania obronnego → Zarezerwuj spotkanie

Ta analiza została przygotowana przez inżynierów Corvus Intelligence, którzy tworzą i weryfikują oprogramowanie o kluczowym znaczeniu dla bezpieczeństwa dla organizacji obronnych i rządowych. Dowiedz się więcej o naszym zespole →

Często zadawane pytania

Czym jest formalna weryfikacja i czym różni się od testowania oprogramowania?

Formalna weryfikacja używa technik dowodu matematycznego do wykazania, że system oprogramowania spełnia precyzyjnie określoną specyfikację, podczas gdy testowanie wykonuje program dla skończonego zestawu danych wejściowych i obserwuje wyniki. Fundamentalna różnica polega na zupełności: testowanie może wykazać obecność błędów, ale nie może udowodnić ich braku, ponieważ żaden skończony zestaw testów nie obejmuje wszystkich możliwych danych wejściowych i stanów. Formalna weryfikacja rozumuje nad kompletną przestrzenią możliwych zachowań — gdy się powiedzie, zapewnia gwarancję obowiązującą dla każdego wykonania, nie tylko dla tych, które zostały sprawdzone. W praktyce oznacza to, że metody formalne uzupełniają testowanie, a nie zastępują je: są stosowane do najbardziej krytycznych właściwości, gdzie koszt niewykrytych błędów jest najwyższy i gdzie pokrycie testami jest strukturalnie niemożliwe do osiągnięcia. W przypadku oprogramowania obronnego o kluczowym znaczeniu dla bezpieczeństwa nawet jedna niesprawdzona ścieżka zawierająca tryb awarii może stanowić niedopuszczalne ryzyko dla bezpieczeństwa — i właśnie tę lukę adresują metody formalne.

Czym jest model checking i jakie właściwości może weryfikować?

Model checking jest techniką formalnej weryfikacji, która wyczerpująco eksploruje wszystkie osiągalne stany modelu skończonego automatu systemu, sprawdzając w każdym stanie, czy dana właściwość wyrażona w logice temporalnej zachodzi. Właściwości Linear Temporal Logic (LTL) wyrażają wymagania dotyczące sekwencji stanów w czasie — na przykład „ilekroć flaga uzbrojenia broni jest ustawiona, blokada bezpieczeństwa musi była zwolniona w poprzednim stanie". Właściwości CTL rozumują o rozgałęziających się przyszłościach — „zawsze możliwe jest osiągnięcie bezpiecznego stanu z dowolnego osiągalnego stanu". Typowe aplikacje obronne obejmują weryfikację automatów stanów protokołów komunikacyjnych, sprawdzanie, że wszystkie ścieżki przez graf przepływu sterowania spełniają daną niezmienność bezpieczeństwa, i potwierdzanie, że żadna sekwencja prawidłowych danych wejściowych nie może doprowadzić systemu do zakazanej konfiguracji. Model checkery takie jak SPIN i NuSMV generują ślad kontrprzykładu, gdy właściwość jest naruszona, czyniąc CEGAR praktycznym iteracyjnym przepływem pracy.

Na czym polega problem eksplozji stanów w model checking?

Problem eksplozji stanów to wykładniczy wzrost przestrzeni stanów, która musi być eksplorowana wraz ze wzrostem liczby współbieżnych komponentów lub zmiennych danych. System z N zmiennymi boolowskimi ma 2^N możliwych stanów; system z N współbieżnymi wątkami, każdy mający K stanów, ma K^N połączonych stanów. W praktyce nawet małe systemy osadzone mogą generować przestrzenie stanów z miliardami osiągalnych stanów, które wyczerpują dostępną pamięć przed zakończeniem eksploracji. Nowoczesne model checkery rozwiązują to za pomocą Binary Decision Diagrams (BDDs) reprezentujących zbiory stanów symbolicznie, CEGAR udoskonalającego abstrakcje tylko tam, gdzie pojawiają się pozorne kontrprzykłady, redukcji częściowego porządku przycinającej równoważne przeplatania zdarzeń współbieżnych i ograniczonego model checking używającego solwerów SAT do sprawdzania właściwości do ustalonej długości ścieżki — wystarczającej dla większości właściwości bezpieczeństwa. W przypadku oprogramowania obronnego ograniczenie zakresu model checking do określonych podsystemów krytycznych utrzymuje przestrzeń stanów w zarządzalnych granicach, jednocześnie skupiając wysiłek weryfikacyjny tam, gdzie ma to największe znaczenie.

Czym są prowersy twierdzeń i które są stosowane w weryfikacji oprogramowania obronnego?

Prowersy twierdzeń to narzędzia wspomagające inżynierów w konstruowaniu weryfikowanych maszynowo matematycznych dowodów właściwości oprogramowania. W przeciwieństwie do model checkerów, prowersy twierdzeń nie są ograniczone rozmiarem przestrzeni stanów i mogą rozumować o nieskończonych dziedzinach — w tym liczbach rzeczywistych, nieograniczonych liczbach całkowitych i sparametryzowanych algorytmach. Trzy prowersy najczęściej spotykane w formalnej weryfikacji obronnej i lotniczej to Coq, Isabelle/HOL i PVS. Mechanizm ekstrakcji Coq może generować certyfikowany kod wykonywalny bezpośrednio ze zweryfikowanych specyfikacji. Isabelle/HOL doczekał się dużego zastosowania przemysłowego, najbardziej znany jest dowód mikrojądra seL4. PVS został zaprojektowany specjalnie do specyfikacji oprogramowania i był stosowany do oprogramowania lotniczego NASA i logiki systemów bezpieczeństwa jądrowego. Wszystkie trzy wymagają znacznej wiedzy specjalistycznej i znacznych nakładów początkowych na pisanie specyfikacji, dlatego programy zazwyczaj rezerwują je dla algorytmów o najwyższej krytyczności, gdzie żadna inna technika nie zapewnia wystarczającej gwarancji.

Czym jest interpretacja abstrakcyjna i jak Astrée ją wykorzystuje?

Interpretacja abstrakcyjna jest matematyczną ramą do obliczania poprawnych nadprzyliżeń semantyki programu. Zamiast śledzić dokładne wartości, które zmienna może przechowywać, abstrakcyjny interpreter śledzi abstrakcję — taką jak przedział, w którym zmienna ma gwarantowanie się mieścić. Jeśli obliczenie abstrakcyjne zakończy się bez wykrycia błędu w żadnym abstrakcyjnym stanie, narzędzie gwarantuje, że konkretny program jest również wolny od tej klasy błędów. Astrée stosuje interpretację abstrakcyjną do dowiedzenia braku błędów wykonania w programach C — przepełnienia liczb całkowitych, dzielenia przez zero, wyłuskań wskaźnika NULL, dostępów do tablic poza granicami i odczytów niezainicjalizowanych. Zostało użyte do weryfikacji podstawowego oprogramowania lotniczego Airbusa A380 z zerową liczbą nierozwiązanych alarmów. W przypadku osadzonego oprogramowania obronnego Astrée i MathWorks Polyspace Code Prover są stosowane do dowiedzenia, że moduły o kluczowym znaczeniu dla bezpieczeństwa nigdy nie będą generować wyjątków wykonania przy żadnych danych wejściowych, spełniając kluczowe wymagania dla DO-178C DAL A i eliminacji zagrożeń oprogramowania MIL-STD-882.

W jaki sposób DO-178C uwzględnia metody formalne?

DO-178C zawiera suplement metod formalnych — DO-333 (Formal Methods Supplement to DO-178C and DO-278A) — który definiuje, w jaki sposób działania w zakresie analizy formalnej mogą spełniać cele weryfikacji DO-178C. W ramach DO-333 metoda formalna może zapewniać kredyt dla wymagań pokrycia strukturalnego: dowód, że właściwość zachodzi dla wszystkich osiągalnych stanów, zapewnia równoważną gwarancję jak pokrycie MC/DC odpowiednich ścieżek kodu, o ile metoda formalna jest poprawna i wykazano, że właściwość implikuje wymaganie bezpieczeństwa. Suplement wymaga, aby model formalny dokładnie reprezentował implementację, wszystkie założenia były jawnie określone i uzasadnione, a narzędzia były zakwalifikowane zgodnie z DO-330. Metody formalne uzupełniają, a nie zastępują testowanie w ramach DO-178C — zmniejszają obciążenie testowaniem dla określonych celów, jednocześnie zwiększając głębokość gwarancji dla formalnie analizowanych właściwości. PSAC musi opisywać podejście do metod formalnych od początku programu.

W jaki sposób MIL-STD-882 łączy formalną weryfikację z kredytem redukcji zagrożeń?

MIL-STD-882E definiuje macierz ryzyka opartą na wadze zagrożenia i prawdopodobieństwie wystąpienia, z preferowaną hierarchią ograniczania: eliminacja zagrożenia, zmniejszenie prawdopodobieństwa, dodanie wykrywania i ostrzegania, a następnie akceptacja ryzyka szczątkowego. Formalna weryfikacja przyczynia się do pierwszych dwóch poziomów. Dowód model checking, że logika zwolnienia broni nigdy nie może być wyzwolona bez zarówno zwolnienia blokady bezpieczeństwa, jak i potwierdzenia operatora w prawidłowej kolejności, stanowi eliminację zagrożenia dla ścieżki przyczynowej oprogramowania tego zagrożenia. Tam gdzie eliminacja nie jest osiągalna, poprawny dowód interpretacji abstrakcyjnej ograniczający wskaźnik awarii wywołanej przez oprogramowanie dostarcza dowodów dla kredytu redukcji prawdopodobieństwa zgłoszonego w analizie zagrożeń. Kluczowym krokiem dokumentacyjnym jest śledzenie każdego formalnego wyniku do określonej przyczyny zagrożenia w Analizie zagrożeń systemu — ta identyfikowalność przekształca działanie weryfikacyjne w uznany argument bezpieczeństwa.

Jaki jest realistyczny kompromis kosztów i korzyści formalnej weryfikacji w programie obronnym?

Formalna weryfikacja niesie znaczące koszty początkowe: budowanie modeli formalnych, pisanie specyfikacji, szkolenie inżynierów i kwalifikowanie narzędzi dla kredytu regulacyjnego. Korzyści są wysokie, ale nierównomiernie rozłożone: metody formalne zapewniają dużą wartość dla małych, matematycznie precyzyjnych komponentów — algorytmów planowania, automatów stanów, logiki blokad bezpieczeństwa — i niską wartość dla dużego kodu integracyjnego, gdzie specyfikacja byłaby równie złożona jak implementacja. Realistyczne oczekiwania: interpretacja abstrakcyjna dodaje 5–10% wysiłku inżynierskiego zrównoważonego przez 15–30% redukcję wymaganych przypadków testowych; model checking dodaje 10–20% kosztów fazy projektowania dla docelowych automatów stanów, ale eliminuje całą klasę defektów wykrywanych w przeciwnym razie w teście integracyjnym; dowodzenie twierdzeń niesie najwyższy koszt i powinno być oceniane per-komponent z jawnym uzasadnieniem przed zobowiązaniem. Programy stosujące metody formalne selektywnie do właściwych komponentów odzyskują swoją inwestycję; programy stosujące je bez różnicy przekraczają harmonogram i budżet.

Jaka kwalifikacja narzędzi jest wymagana przy stosowaniu narzędzi do analizy formalnej dla kredytu DO-178C?

DO-178C §12.2 wymaga kwalifikowania narzędzi programowych, gdy ich wyniki są używane bez niezależnej weryfikacji. DO-330 definiuje Poziomy Kwalifikacji Narzędzi (TQL-1 do TQL-5) na podstawie roli narzędzia i poziomu gwarancji projektowej. Narzędzie do analizy formalnej używane do spełnienia celu weryfikacji DO-178C DAL A plasuje się na TQL-1 lub TQL-2, wymagając najbardziej rygorystycznych artefaktów kwalifikacyjnych: wymagań operacyjnych narzędzi, planu kwalifikacji narzędzi, podsumowania osiągnięć kwalifikacji i dowodów prawidłowych wyników dla odpowiedniego przypadku użycia. Komercyjne narzędzia takie jak Astrée i Polyspace dostarczają istniejące zestawy kwalifikacyjne, które zmniejszają obciążenie programu do wykazania, że zestaw ma zastosowanie do ich konkretnego kontekstu użycia i konfiguracji kompilatora. Narzędzia open-source zazwyczaj wymagają pełnej kwalifikacji od zera — znaczny koszt programu, który musi być uwzględniony w planie projektu od samego początku.

Jakich umiejętności zespołu potrzeba, aby wprowadzić formalną weryfikację do zespołu oprogramowania obronnego?

Narzędzia do interpretacji abstrakcyjnej, takie jak Astrée i Polyspace, są punktem wejścia o najniższej barierze i mogą być obsługiwane przez inżynierów ze środowiskiem C/C++ po kilku dniach szkolenia — podstawową umiejętnością jest sortowanie alarmów: rozróżnianie rzeczywistych defektów od fałszywych alarmów spowodowanych niedokładnością abstrakcji. Model checking z SPIN lub NuSMV wymaga inżynierów, którzy potrafią pisać specyfikacje w Promela lub SMV i wyrażać właściwości w LTL/CTL — umiejętność, której opanowanie zajmuje tygodnie lub miesiące i nie jest nauczana w standardowych programach nauczania. Dowodzenie twierdzeń z Coq, Isabelle/HOL lub PVS wymaga głębokiej wiedzy specjalistycznej z zakresu logiki formalnej i teorii dowodów — umiejętności, które większość programów będzie musiała rekrutować lub zlecać specjalistycznym organizacjom. Najbardziej praktyczna ścieżka obsady to wprowadzenie najpierw interpretacji abstrakcyjnej, przeszkolenie inżynierów specjalnie w model checking do weryfikacji automatów stanów i zarezerwowanie dowodzenia twierdzeń dla zleconych specjalistycznych prac nad komponentami o najwyższej krytyczności.