Verificare formală pentru software de apărare cu criticalitate ridicată

Un defect software într-o aplicație comercială costă bani și creează inconveniente utilizatorilor. Un defect software într-un sistem de control al focului armelor, într-o unitate de management al zborului unei aeronave sau într-o componentă de autoritate de comandă nucleară poate cauza daune fizice ireversibile. Asimetria consecințelor este atât de extremă, încât abordarea standard a calității software — scriere cod, rulare teste, corectare erori găsite prin teste — este insuficientă. Testarea poate demonstra prezența defectelor; nu poate demonstra absența lor. Pentru software de apărare cu cel mai ridicat nivel de criticalitate, comunitatea ingineriei a răspuns acestei limitări cu verificarea formală: tehnici riguros matematice care demonstrează că comportamentul software este corect prin construcție, nu doar prin eșantionare.

Acest articol este un ghid practic de inginerie pentru aplicarea metodelor formale în software de apărare cu criticalitate ridicată. Acoperă cadrul de reglementare care impune verificarea formală la cele mai înalte niveluri de criticalitate, principalele instrumente și tehnici (TLA+, SPARK Ada, CBMC, Frama-C), provocarea specifică a verificării protocoalelor prin model checking și integrarea artefactelor formale în dovezile de conformitate DO-178C. Se încheie cu o analiză cost-beneficiu care oferă managerilor de program un cadru pentru a decide când verificarea formală merită costul suplimentar — și când este pur și simplu obligatorie.

Când este obligatorie verificarea formală în software de apărare

Mandatul pentru verificarea formală în software de apărare apare la intersecția a două cadre de reglementare: standardul de siguranță a sistemelor MIL-STD-882E, care clasifică pericolele după severitatea consecințelor și probabilitate, și standardele de dezvoltare software care traduc aceste clasificări în obligații de inginerie software.

MIL-STD-882E atribuie fiecărei funcții software un Indice de Criticalitate Software (SCI) bazat pe produsul severității consecințelor (Catastrofal — pierdere de vieți sau sistem; Critic — vătămare gravă sau daune majore de sistem; Marginal — vătămare minoră sau daune de sistem; Neglijabil) și probabilitate. Funcțiile evaluate cu severitate Catastrofală primesc SCI Categoria I indiferent de probabilitate, deoarece nicio probabilitate de a provoca un rezultat catastrofal prin neglijență inginerească nu este acceptabilă. Funcțiile din Categoria I trebuie supuse celor mai riguroase tehnici de analiză de siguranță software disponibile — ceea ce astăzi înseamnă analiză formală.

Pentru sistemele de armament aeriene și adiacente (rachete, muniții ghidate cu software de control al zborului), standardul de certificare este DO-178C. DO-178C definește cinci Niveluri de Asigurare a Proiectării (DAL A până la E), cu Nivelul A rezervat pentru software a cărui defecțiune ar putea cauza sau contribui la o condiție de defecțiune catastrofală. Nivelul A impune 66 de obiective de dezvoltare și verificare software, inclusiv:

• 100% acoperire MC/DC (Modified Condition/Decision Coverage) — fiecare efect independent al unei condiții asupra unei decizii trebuie demonstrat
• Independența activităților de verificare față de activitățile de dezvoltare
• Calificarea instrumentelor conform DO-330 pentru orice instrument utilizat pentru eliminarea activităților de verificare obligatorii
• Analiza formală (prin suplimentul DO-333) ca mijloc alternativ de conformitate pentru obiectivele de acoperire structurală

Suplimentul DO-333 la DO-178C abordează explicit metodele formale ca mijloc de satisfacere a obiectivelor de verificare. Când un program aplică verificarea formală folosind DO-333, trebuie să producă un Plan de Metode Formale care să descrie formalismul ales, proprietățile verificate, instrumentele utilizate și modul în care dovezile de verificare formală se mapează la obiectivele din Tabelele A-3 până la A-7 ale DO-178C.

Pentru sistemele de armament terestre și navale care nu sunt supuse DO-178C, calea analogă trece prin cerințele MIL-STD-882E Categoria I în Planuri de Dezvoltare Software specifice programului, care fac din ce în ce mai mult referire la tehnicile de analiză formală ca dovadă a rigorii proporționale cu severitatea consecințelor. Deciziile de arhitectură software cu criticalitate ridicată care determină care componente ating Categoria I sau DAL A trebuie luate devreme în proiectarea sistemului — ele reprezintă factorul principal al costului de verificare.

Specificarea înaintea codului: modelul formal

TLA+ (Temporal Logic of Actions, dezvoltat de Leslie Lamport) este cel mai adoptat limbaj de specificare formală pentru sisteme distribuite și protocoale de mașini de stare în software de apărare. O specificație TLA+ descrie un sistem ca un set de variabile de stare și un set de acțiuni — tranziții care schimbă starea — exprimate într-o notație matematică neambiguă și verificabilă automat.

Perspectiva critică este că specificațiile TLA+ se scriu înainte de a începe implementarea. Aceasta nu este doar o bună practică; este mecanismul prin care metodele formale găsesc defectele pe care testarea le ratează. Testele exercită comportamentele pe care testerul le-a anticipat. Un model formal, verificat exhaustiv de model checker-ul TLC, exercită toate comportamentele pe care specificația le permite — inclusiv comportamentele pe care specificatorul nu le-a considerat în mod conștient.

Luați în considerare un exemplu simplificat al unui protocol de autorizare a lansării de armament. Protocolul impune că o comandă de lansare este executată numai atunci când ambii membri ai echipajului s-au autentificat independent și ambii au autorizat explicit lansarea în cadrul unei ferestre de timp definite. O cerință în limbaj natural poate afirma clar acest lucru. Dar specificația formală trebuie să facă explicită fiecare tranziție de stare:

VARIABLES pilot_auth, copilot_auth, pilot_authorized,
          copilot_authorized, release_executed, time_window_open

TypeInvariant ==
    /\ pilot_auth       \in BOOLEAN
    /\ copilot_auth     \in BOOLEAN
    /\ pilot_authorized \in BOOLEAN
    /\ copilot_authorized \in BOOLEAN
    /\ release_executed \in BOOLEAN
    /\ time_window_open \in BOOLEAN

SafetyInvariant ==
    release_executed =>
        (pilot_auth /\ copilot_auth /\
         pilot_authorized /\ copilot_authorized /\
         time_window_open)

Init ==
    /\ pilot_auth       = FALSE
    /\ copilot_auth     = FALSE
    /\ pilot_authorized = FALSE
    /\ copilot_authorized = FALSE
    /\ release_executed = FALSE
    /\ time_window_open = FALSE

Când TLC verifică acest model, explorează toate stările accesibile din Init sub toate tranzițiile Next posibile. Dacă orice secvență de tranziții valide poate atinge o stare în care release_executed = TRUE în timp ce invariantul de siguranță este încălcat, TLC produce o urmă contraexemplu — o secvență pas cu pas de tranziții de stare care duce la starea nesigură. Acest contraexemplu nu este un caz de test care s-a întâmplat să eșueze; este o dovadă că specificația are un gap, iar gap-ul trebuie închis în cerințe înainte de a începe implementarea.

Ceea ce TLA+ găsește și testarea ratează se împarte în trei categorii. În primul rând, condiții de cursă în mașini de stare concurente — două evenimente independente care se pot intercala într-un mod pe care niciun test secvențial nu îl poate exercita. În al doilea rând, violări ale vivacității — scenarii în care sistemul rămâne blocat într-o stare care satisface toți invarianții de siguranță, dar nu progresează niciodată spre un obiectiv necesar. În al treilea rând, presupuneri implicite — proprietăți pe care echipa de proiectare le deținea implicit și prin urmare nu le-a testat niciodată, pe care TLC le violează explorând tranziții pe care echipa nu le-a considerat în mod conștient.

SPARK Ada: subset al Ada pentru corectitudine demonstrabilă

SPARK Ada este un subset formal definit al limbajului de programare Ada, conceput astfel încât programele scrise în SPARK să poată fi verificate static de setul de instrumente GNATprove. SPARK restricționează limbajul Ada complet în moduri care fac semantica amenabilă pentru demonstrație automată: fără aliasare prin tipuri de acces (pointeri), fără dispatch dinamic în subsetul relevant pentru demonstrație, fără tasking în ținta demonstrației și declararea explicită a întregii stări globale prin specificații de aspect.

Valoarea de verificare a SPARK provine din două niveluri distincte de analiză:

Analiza fluxului verifică proprietățile fluxului de date fără a încerca demonstrația: confirmă că fiecare variabilă citită a fost inițializată înainte de citire, că subprogramele accesează numai starea globală pe care o declară în aspectul lor Global și că fluxurile de informații sunt consistente cu aspectul Depends (care indică de ce ieșiri depind de ce intrări). Analiza fluxului rulează rapid — în secunde până la minute pentru baze de cod mari — și elimină o întreagă categorie de erori de execuție pe care testarea convențională le-ar găsi numai cu acoperire adecvată.

Modul de demonstrație încearcă să descarce toate condițiile de verificare a erorilor de execuție ca teoreme matematice folosind solverii SMT de backend ai GNATprove (Alt-Ergo, CVC5, Z3). O condiție de verificare a erorilor de execuție în SPARK este generată pentru fiecare operație care ar putea ridica o eroare de execuție: accesuri la indexul unui tablou, aritmetică de întregi, conversii de tip, verificări de precondiție. Când GNATprove demonstrează o condiție de verificare, a stabilit că nicio execuție a subprogramului nu poate declanșa acea eroare de execuție, pentru toate intrările posibile care satisfac precondiția. Aceasta este o garanție fundamental mai puternică decât testarea.

-- Exemplu: buffer limitat verificat pentru coada de mesaje C2
package Message_Queue
  with SPARK_Mode => On
is
   Max_Messages : constant := 256;
   subtype Index_Type is Natural range 0 .. Max_Messages - 1;
   subtype Count_Type is Natural range 0 .. Max_Messages;

   type Queue_T is private;

   function Is_Full  (Q : Queue_T) return Boolean;
   function Is_Empty (Q : Queue_T) return Boolean;
   function Length   (Q : Queue_T) return Count_Type;

   procedure Enqueue (Q   : in out Queue_T;
                      Msg :        Message_T)
     with Pre  => not Is_Full (Q),
          Post => Length (Q) = Length (Q'Old) + 1;

   procedure Dequeue (Q   : in out Queue_T;
                      Msg :    out Message_T)
     with Pre  => not Is_Empty (Q),
          Post => Length (Q) = Length (Q'Old) - 1;

private
   type Queue_T is record
      Data  : Message_Array (Index_Type);
      Head  : Index_Type := 0;
      Tail  : Index_Type := 0;
      Count : Count_Type := 0;
   end record;
end Message_Queue;

GNATprove verifică că implementarea Enqueue și Dequeue respectă postcondițiile lor pentru toate intrările care satisfac precondiția și că nu poate apărea niciun acces în afara limitelor tabloului, nicio depășire a întregilor și nicio citire neinițializată. Pentru o coadă de mesaje utilizată într-o aplicație C2 certificată, aceasta înlocuiește zeci de cazuri de test cu valori limită cu o singură demonstrație care acoperă întregul spațiu de intrări.

Integrarea cu GNAT în pipeline-ul CI/CD pentru software de apărare este simplă: GNATprove este invocat ca pas de compilare cu fișierul de proiect specificând nivelul de demonstrație (0 până la 4, unde 4 încearcă demonstrații cu cel mai mare efort). Rezultatele demonstrației sunt emise ca JSON lizibil de mașini, permițând integrarea cu instrumente de urmărire a defectelor și de trasabilitate a certificării.

Instrumente de analiză formală pentru C/C++

Majoritatea software-ului de apărare implementat este scris în C și C++, nu Ada. Pentru această bază instalată, două instrumente de analiză formală sunt cel mai frecvent utilizate în programele certificate: CBMC (C Bounded Model Checker) pentru verificarea accesibilității limitate și Frama-C cu pluginul său WP (weakest precondition) pentru verificarea deductivă completă.

CBMC traduce programele C în probleme SAT/SMT și le rezolvă pentru a determina dacă o proprietate dată poate fi violată într-un număr limitat de pași de execuție. CBMC verifică nativ depășirile de buffer, utilizarea după eliberare, depășirile de întregi, dereferențele de pointer nul și violările de aserțiuni — categoriile de defecte care cauzează majoritatea vulnerabilităților de securitate în codul C. Punctul său forte principal este un efort de adnotare redus: CBMC poate verifica o funcție C pentru erori de execuție cu modificare minimă a sursei. Limitarea sa principală este că furnizează garanții numai până la limita specificată de desfășurare a buclei — pentru bucle nesfârșite, absența unui contraexemplu CBMC nu este o demonstrație a corectitudinii.

Frama-C cu WP este un cadru modular de analiză C care suportă verificarea deductivă completă a codului C adnotat cu contracte ACSL (ANSI/ISO C Specification Language). Contractele ACSL specifică precondiții de funcție, postcondiții, invarianți de buclă și amprente de memorie într-un limbaj formal încorporat ca comentarii C. Pluginul WP generează condiții de verificare (VC) din codul C adnotat și le descarcă folosind solverii backend ai Why3 (Alt-Ergo, CVC5, Coq). Condițiile de verificare nedemonstrate reprezintă fie defecte reale, fie invarianți de buclă lipsă, fie proprietăți care necesită demonstrații manuale Coq.

Relația dintre MISRA C și verificarea formală este complementară: regulile MISRA C elimină constructele de limbaj (conversii implicite de întregi, aliasare a pointerilor prin cast-uri, alocare dinamică de memorie) care fac codul C ambiguu semantic și prin urmare dificil de verificat formal. Aplicarea conformității MISRA C:2012 — în special regulile Obligatorii din categoriile Conversii de tipuri pointer, Stocare suprapusă și Model de tip esențial — stabilește fundația semantică bine definită pe care analizele WP ale Frama-C o necesită pentru a produce rezultate corecte. O verificare de conformitate MISRA C este prin urmare pasul corect înainte de aplicarea Frama-C, nu o alternativă la aceasta.

Instrument	Tehnică	Efort de adnotare	Puterea garanției	DO-330 TQL
CBMC	Model checking limitat (SAT)	Redus	Până la limită	TQL-3 (suplimentar)
Frama-C / WP	Verificare deductivă (SMT)	Ridicat (contracte ACSL)	Complet (pentru obiective demonstrate)	TQL-1 (cu kit de calificare)
Polyspace Verifier	Interpretare abstractă	Redus–mediu	Corect (poate supra-aproxima)	TQL-1 (kit de calificare disponibil)
GNATprove (SPARK)	Deductiv + analiză flux	Ridicat (contracte Ada+SPARK)	Complet (pentru obiective demonstrate)	TQL-1 (kit de calificare disponibil)

Model checking pentru verificarea protocoalelor

Model checking-ul explorează exhaustiv spațiul de stări al unui model cu stări finite pentru a determina dacă o proprietate de logică temporală se menține în toate stările accesibile. Pentru protocoalele C2 de apărare — handshake-uri de autentificare, secvențierea mesajelor, convergența stării legăturii, corectitudinea protocoalelor criptografice — model checking-ul este calea cea mai directă spre asigurare, deoarece comportamentul protocolului este inerent concurrent și modurile de eșec sunt exact erorile dependente de intercalare pe care testarea nu le poate expune în mod fiabil.

Provocarea fundamentală este explozia stărilor: dimensiunea spațiului de stări crește exponențial cu numărul de componente concurente. Un sistem C2 cu 8 noduri, fiecare menținând 16 biți de stare, are un spațiu de stări teoretic de 2^128 — aproximativ 3,4 × 10^38 stări, pe care niciun model checker cu stări explicite nu le poate enumera în timp finit. Programele de apărare abordează explozia stărilor prin patru strategii complementare:

Abstractizare. Înlocuiți valorile concrete ale datelor cu domenii abstracte care păstrează proprietățile verificate. În loc să modelați un număr de secvență pe 32 de biți, modelați-l ca un element abstract al unui set ordonat {INITIAL, NEXT, WRAP} care captează semantica de secvențiere fără intervalul numeric complet. Rafinamentul ghidat de contraexemple (CEGAR) automatizează acest proces: model checker-ul rafinează abstracțiunea ori de câte ori produce un contraexemplu care este imposibil în modelul concret.

Reducerea prin simetrie. Exploatați echivalențele structurale între componente. Dacă 8 noduri dintr-o rețea C2 sunt structural identice, model checker-ul trebuie să exploreze un singur reprezentant al fiecărei clase de echivalență a stărilor sistemului sub grupul de permutare al celor 8 noduri. Aceasta poate reduce spațiul efectiv de stări cu un factor de N! (8! = 40.320 pentru 8 noduri).

Reducerea parțială a ordinii. Multe execuții concurente care diferă numai în ordinea evenimentelor independente (evenimente care nu partajează stare) duc la aceeași stare. Reducerea parțială a ordinii comprimă aceste ordonări echivalente într-un singur reprezentant fără pierderea completitudinii verificării proprietăților.

Model checking limitat. În loc să exploreze toate căile de lungime arbitrară, verificați toate căile până la lungimea k folosind un solver SAT sau SMT. Majoritatea defectelor de protocol se manifestă în urme contraexemplu scurte (4–20 pași); model checking-ul limitat cu k=30 este suficient pentru a găsi marea majoritate a erorilor de protocol, rămânând totodată tractabil din punct de vedere computațional.

Când un model checker găsește o violare a unei proprietăți, produce o urmă contraexemplu — o secvență completă de stări de sistem de la starea inițială până la starea de violație. Această urmă este direct acționabilă: specifică exact care secvență de evenimente duce la starea nesigură, permițând dezvoltatorilor să reproducă eșecul determinist și să proiecteze o remediere a protocolului. Într-o verificare documentată a unui protocol C2 de apărare, o urmă contraexemplu de 12 pași a dezvăluit că o ocolire a autentificării era posibilă dacă apărea o combinație specifică de întârziere a mesajelor și retransmitere — un scenariu care nu fusese exercitat în 18 luni de testare a integrării.

Integrarea metodelor formale în conformitatea DO-178C

Suplimentul DO-333 la DO-178C stabilește cadrul pentru utilizarea metodelor formale ca mijloace alternative de conformitate pentru obiectivele specifice de verificare DO-178C. Utilizarea DO-333 necesită un Plan de Metode Formale care să abordeze:

• Metoda (metodele) formală selectată și baza pentru selecția acesteia
• Proprietățile care urmează să fie verificate formal și maparea lor la cerințele software DO-178C
• Instrumentul (instrumentele) de utilizat, statutul lor de calificare DO-330 și planul de calificare dacă nu sunt pre-calificate
• Modul în care dovezile de verificare formală vor fi prezentate în Rezumatul Realizărilor Software
• Ce combinație de verificare formală și testare realizează acoperirea completă a obiectivelor

Trasabilitatea este mecanismul critic de integrare. Lanțul de trasabilitate DO-178C rulează de la Cerințele de Sistem prin Cerințele de Nivel Înalt (HLR), Cerințele de Nivel Scăzut (LLR), Codul Sursă și Cazurile de Verificare. Artefactele formale trebuie inserate în acest lanț la puncte definite:

Cerinte Sistem (SRD)
    └─► Cerinte Nivel Inalt (HLR)    ◄── proprietati specificatie TLA+
            └─► Cerinte Nivel Scazut (LLR) ◄── contracte SPARK / adnotari ACSL
                    └─► Cod Sursa  ◄── tinta GNATprove / CBMC / Frama-C
                            └─► Cazuri de Verificare (SVCP/SVR)
                                    └─► rapoarte de demonstratie, output model checker,
                                        jurnale de verificare fara contraexemple

Calificarea instrumentelor conform DO-330 este a doua provocare de integrare. Un instrument care elimină un proces de verificare software DO-178C obligatoriu — cum ar fi un prover formal care elimină necesitatea testării acoperirii structurale — trebuie calificat la TQL-1. Calificarea TQL-1 necesită un Plan de Calificare a Instrumentului, un Rezumat al Realizărilor Instrumentului, Cerințe Operaționale ale Instrumentului și dovezi de testare generate în mediul de compilare al programului. Pachetele de instrumente pre-calificate de la AdaCore (GNATprove), MathWorks (Polyspace) și LDRA reduc substanțial acest efort față de calificarea internă, dar programul trebuie totuși să verifice că calificarea furnizorului se aplică versiunii specifice a instrumentului și contextului de utilizare.

Discuția privind etica AI pentru sistemele militare este din ce în ce mai relevantă pe măsură ce programele iau în considerare verificarea formală asistată de AI — instrumente care folosesc rețele neuronale pentru a sugera invarianți de buclă sau strategii de demonstrație. Statutul de certificare al unor astfel de componente de asistență AI este nerezolvat sub ghidajul actual DO-178C; programele ar trebui să trateze sugestiile asistate de AI ca necesitând revizuire umană independentă înainte de includerea în dovezile de certificare.

Analiza cost-beneficiu: când merită verificarea formală

Costul verificării formale este real și substanțial. Adnotarea unui modul SPARK Ada de 10.000 de linii până la nivelul demonstrației complete a erorilor de execuție necesită 3–6 luni de timp al unui inginer expert. Calificarea unui instrument de verificare formală conform DO-330 TQL-1 necesită 3–6 luni de efort suplimentar prima dată. Scrierea și verificarea unei specificații TLA+ a unui protocol complex durează săptămâni. Niciun cost din acestea nu dispare.

Calculul beneficiilor trebuie făcut față de alternativa corectă. Alternativa la verificarea formală la DO-178C Nivelul A nu este lipsa verificării; este testarea exhaustivă la acoperire MC/DC, care pentru o mașină de stare complexă cu N condiții într-o decizie are O(2N) cazuri de test, potențial cu analiza formală necesară oricum pentru a demonstra adecvarea MC/DC. Pentru funcțiile cu criticalitate ridicată netriviale, costul testării pentru atingerea obiectivelor de Nivel A fără metode formale este adesea mai mare decât costul verificării formale — și oferă o formă mai slabă de asigurare.

Datele din industrie susțin în mod consistent trei concluzii:

Costul descoperirii defectelor. Defectele găsite în timpul specificației formale costă aproximativ 1× pentru reparare. Defectele găsite în timpul revizuirii codului costă de 10× față de baza de referință. Defectele găsite în testarea de integrare costă de 100×. Defectele găsite după certificare costă de 1.000× sau mai mult, inclusiv costul recertificării. Specificația formală, care expune defectele în cel mai timpuriu stadiu posibil, are cel mai bun profil de cost al defectelor din orice tehnică — în special pentru defectele la nivel de arhitectură (proiectare incorectă a mașinilor de stare, condiții de cursă ale protocoalelor) pe care metodele formale sunt unic de eficiente în a le găsi.

Reducerea costului de verificare pe ciclu de viață. Pentru programele care aplică SPARK Ada la componentele de Nivel A, reducerea costului de verificare în aval este de 50–70%. Prover-ul formal descarcă obiectivele de acoperire structurală care altfel ar necesita o dezvoltare extensivă a harnaiamentului de test, instrumentare de acoperire și măsurarea acoperirii pe o matrice de test combinatorie.

Când verificarea formală nu merită. Pentru software la DO-178C Nivelul C sau mai jos și MIL-STD-882 Categoria III sau IV, costul suplimentar al metodelor formale depășește de obicei beneficiul. Nivelul C necesită 100% acoperire a instrucțiunilor și deciziilor — realizabil cu practici standard de dezvoltare bazate pe teste și instrumente de acoperire. Aplicarea metodelor formale la Nivelul C adaugă cost fără a adăuga valoare proporțională de asigurare. Judecata inginerească este simplă: aplicați metode formale acolo unde cerințele de reglementare o impun (Nivelul A, Nivelul B pentru mașini de stare complexe) sau acolo unde consecința defectelor nedetectate — pierderea de vieți, eșecul sistemului în luptă — justifică investiția independent de obligația de reglementare.

Calea practică pentru majoritatea programelor de apărare este o abordare stratificată: specificație formală TLA+ pentru toate mașinile de stare și protocoalele cu criticalitate ridicată; SPARK Ada pentru componentele noi sau rescrise de Nivel A; CBMC și MISRA C pentru componentele C existente care nu pot fi rescrise; și Frama-C/WP pentru funcțiile C cu cel mai înalt nivel de criticalitate unde verificarea deductivă completă este justificată. Fiecare strat adaugă asigurare dincolo de ceea ce oferă testarea singură, iar ieșirea fiecărui strat generează dovezi de certificare care reduc efortul de testare la nivelurile componentelor și testarea integrării.