Verificare Matematică a Software-ului — Cum se demostrează corectitudinea unui program

De la logica Hoare și model checking până la demonstrații complete cu theorem prover. Cum funcționează verificarea matematică a software-ului și ce înseamnă că seL4 e 'verificat matematic'.

Avansat 16 min 06 July 2026
verificare formală seL4 logica Hoare theorem prover model checking CompCert corectitudine software

Ce înseamnă „verificat matematic"?

Când spunem că un program e verificat matematic, nu vorbim despre teste care rulează de 10.000 de ori și nu găsesc bug-uri. Vorbim despre o demonstrație formală — la fel de riguroasă ca una de geometrie — că programul se comportă conform specificației pentru toate intrările posibile.

Un test poate doar să demonstreze prezența bug-urilor, nu și absența lor. O verificare matematică, în schimb, poate dovedi absența unor clase întregi de bug-uri. (Dijkstra, 1972)

1. Fundamente teoretice

Logica Hoare

Propusă de C. A. R. Hoare în 1969, logica Hoare oferă un sistem formal pentru raționament despre corectitudinea programelor imperativ.

Tripletul Hoare:

$${P}\ C\ {Q}$$

  • $P$ = precondiția (ce e adevărat înainte de execuție)
  • $C$ = comanda (programul)
  • $Q$ = postcondiția (ce e adevărat după execuție)

Exemplu:

$${x = 5}\ y \leftarrow x + 2\ {y = 7}$$

Reguli de inferență

Secvență: $$\frac{{P}\ C_1\ {R},\ {R}\ C_2\ {Q}}{{P}\ C_1; C_2\ {Q}}$$

Condițional: $$\frac{{P \land B}\ C_1\ {Q},\ {P \land \neg B}\ C_2\ {Q}}{{P}\ \textbf{if}\ B\ \textbf{then}\ C_1\ \textbf{else}\ C_2\ {Q}}$$

Buclă (while): $$\frac{{I \land B}\ C\ {I}}{{I}\ \textbf{while}\ B\ \textbf{do}\ C\ {I \land \neg B}}$$

$I$ este invariantul buclei — o proprietate care rămâne adevărată la fiecare iterație. Găsirea invariantului e partea creativă a verificării.

Corectitudine parțială vs. totală

  • Corectitudine parțială: dacă programul se termină, atunci postcondiția e satisfăcută.
  • Corectitudine totală: programul se termină și postcondiția e satisfăcută.

Pentru corectitudine totală, la fiecare buclă trebuie demonstrat că un variant (o măsură strict descrescătoare, de obicei un număr natural) scade la fiecare iterație.

2. Abordări ale verificării formale

2.1 Model Checking

Principiu: Explorezi exhaustiv toate stările posibile ale sistemului.

  • Sistemul e modelat ca un graf de stare (automat finit)
  • Proprietatea e exprimată în LTL (Linear Temporal Logic) sau CTL (Computation Tree Logic)
  • Algoritmul verifică dacă toate drumurile din graf satisfac formula

Avantaje: Complet automat, oferă contraexemple. Dezavantaj: Explozia stărilor — un sistem cu 100 de variabile binare are $2^{100}$ stări.

Exemplu — Spin (Gerard Holzmann):

byte x = 0;
active proctype P() {
  do :: x < 100 -> x++ od;
}
ltl { toujours (x <= 100) }

Spin verifică automat că $x$ nu depășește niciodată 100.

2.2 Theorem Proving (Demonstrație asistată)

Principiu: Scrii demonstrația într-un sistem formal (calculul construcțiilor, logica de ordin superior) și o verifici cu un theorem prover interactiv.

| Sistem | Limbaj | Folosit pentru | |---|---|---| | Isabelle/HOL | Logica de ordin superior | seL4, CakeML | | Coq | Calculul construcțiilor inductive | CompCert C | | Lean | CIC dependent | Matematica, FPV | | Z3 (SMT solver) | Logica de ordinul întâi | AWS, Azure (automat) | | Dafny | Hoare logică înglobată | Verificare programe imperativ |

Exemplu (Isabelle/HOL):

theorem add_comm: "x + y = y + x"
  apply (induction x)
   apply auto
  done

Theorem proving e semiautomat — omul scrie demonstrația, mașina verifică fiecare pas. E mai expresiv decât model checking, dar necesită expertiză.

2.3 SMT Solving (Satisfiability Modulo Theories)

Principiu: Un SMT solver combină SAT (satisfiabilitate booleană) cu teorii de fond (aritmetică, vectori, array-uri).

Exemplu (Z3 — Microsoft):

from z3 import *
x = Int('x')
solve(x > 5, x < 3)  # unsat — nu există soluție

Folosit extensiv de AWS pentru verificarea configurațiilor de rețea (AWS Zelkova) și de Azure pentru securitate.

3. Cazul emblematic: seL4

Ce este seL4?

seL4 este un microkernel — nucleu de sistem de operare de doar ~12.000 de linii de cod C și ASM. A fost primul kernel din lume verificat matematic complet (functional correctness proof), publicat în 2009 de NICTA (Australia).

Ce s-a demonstrat?

Echipa a demonstrat în Isabelle/HOL că implementarea în C a seL4 respectă perfect specificația formală:

  1. Corectitudinea funcțională: Codul C implementează corect specificația abstractă.
  2. Absența excepțiilor: Fără dereferențieri de NULL, fără buffer overflow, fără use-after-free.
  3. Absența deadlock-ului: Sistemul nu se blochează în anumite configurații.
  4. Izolarea temporală: Partițiile nu interferează una cu alta.

Arhitectura verificării

Specificație abstractă (Isabelle/HOL)
        ↑ demonstrație de rafinare
Specificație executabilă (Haskell prototip)
        ↑ traducere manuală verificată
Cod C optimizat
        ↑ demonstrație
Arhitectura ARM/MIPS/RISC-V

Verificarea a acoperit toate căile de execuție, toate modurile de capabilități, și a durat ~20 de persoane-ani.

Costul verificării

| Metrică | Valoare | |---|---| | Linii de cod C | ~12.000 | | Linii de demonstrație Isabelle | ~200.000 | | Persoane-ani | ~20 | | Raport demonstrație / cod | ~17:1 | | Timp CPU pentru verificare | ~30 zile | | Bug-uri găsite post-verificare | 0 (în codul verificat) |

Impact practic

  • Folosit în sisteme militare (Boeing, US Air Force)
  • Folosit în mașini autonome (vehicule fără șofer)
  • Folosit în avionică (certificare DO-178C Level A)
  • Standardul seL4 e acum fundația pentru sisteme critice unde un crash înseamnă pierderi de vieți

"seL4 is probably the most convincing example of formal verification of a non-trivial systems component." — Microsoft Research

4. Alte exemple celebre

CompCert C Compiler

CompCert e un compilator C verificat formal în Coq. Spre deosebire de GCC sau Clang, care au optimizări dovedite corecte doar prin teste, CompCert are o demonstrație că semantica programului sursă se păstrează în programul obiect.

Rezultat: CompCert elimină o întreagă clasă de bug-uri de compilator. În teste de fuzzing, GCC și Clang generează cod incorect în ~0.1% din cazuri; CompCert — 0%.

CakeML

Un compilator ML verificat — de la parser la cod mașină, totul e demonstrat corect în HOL4. Include un runtime, un garbage collector, și un REPL.

AWS s2n (TLS)

Amazon a verificat formal s2n-tls (implementarea TLS) folosind model checking (CBMC — C Bounded Model Checker). Au demonstrat că buffer-urile interne nu pot fi citite/scrise necorespunzător, prevenind atacuri de tip Heartbleed.

Amazon AWS Zelkova

Folosește Z3 (SMT solver) pentru a verifica configurațiile AWS Identity and Access Management (IAM) — verifică dacă o politică de securitate permite accesul neautorizat la resurse.

CertiKOS

Un hypervisor verificat formal la Universitatea Yale. Demonstrează izolarea completă între mașinile virtuale — o mașină virtuală nu poate accesa memoria alteia, nici măcar prin canale colaterale.

5. Tehnici avansate

Refinement (Rafinare)

Demonstrezi că o implementare concretă e o rafinare a unei specificații abstracte. Fiecare pas de rafinare adaugă detalii, păstrând proprietățile.

$$Spec \sqsubseteq Impl_1 \sqsubseteq Impl_2 \sqsubseteq \dots \sqsubseteq Cod$$

Separation Logic

Extensie a logicii Hoare pentru programe care manipulează pointeri și heap. Rezolvă problema aliasing-ului.

$${x \mapsto 5 * y \mapsto 7}\ [x] \leftarrow 6\ {x \mapsto 6 * y \mapsto 7}$$

Operatorul $*$ (separating conjunction) spune că $x$ și $y$ sunt zone disjuncte de memorie.

Ghost State

Stare „fantomă" care există doar în demonstrație, nu în programul real. Folosită pentru a urmări proprietăți abstracte.

6. Limitări și critici

  1. Costul: Raportul demonstrație/cod de ~17:1 pentru seL4 face verificarea imprcticabilă pentru majoritatea proiectelor comerciale.

  2. Specificația poate fi greșită: Verificarea demonstrează că implementarea respectă specificația. Dacă specificația e greșită, programul e "corect" dar inutil.

  3. Stack-ul de încredere (TCB): Verificarea seL4 acoperă kernelul, dar nu și hardware-ul, bootloader-ul, sau hypervisor-ul de dedesubt.

  4. Proprietăți vs. intenții: Verificarea formala poate demonstra absența anumitor bug-uri, dar nu poate demonstra că programul face "ce trebuie" din punct de vedere uman.

  5. Scalabilitate: Sistemele moderne (Linux are ~30M linii) nu pot fi verificate complet cu tehnologia actuală.

7. Viitorul verificării formale

  • Verificare incrementală: Nu verifici totul de la zero, ci doar modificările (regression verification)
  • Tooling mai bun: Rust borrow checker e o formă de verificare statică integrată; Rust e primul limbaj mainstream care aduce garantii de memory safety la nivel de compilator
  • SMT solvers mai rapizi: Z3 și cvc5 pot verifica acum în minute ce lua ore acum 10 ani
  • Integrare CI/CD: GitHub Actions cu CBMC sau Dafny pentru verificare automată la fiecare commit
  • LLM + verificare: Generarea de demonstrații asistată de AI e un domeniu activ de cercetare

Concluzie

Verificarea matematică a software-ului transformă programarea dintr-o activitate empirică ("rulează testele și vezi") într-una științifică ("demonstrează că e corect"). seL4 rămâne exemplul clasic — un sistem real, folosit în producție, cu o demonstrație completă că face exact ce trebuie.

Pentru o înțelegere mai profundă a fundațiilor, vezi articolele despre Lambda Calculus și Mașina Turing.

Referințe

  • Klein, G. et al. seL4: Formal Verification of an OS Kernel (SOSP 2009)
  • Leroy, X. Formal Verification of a Realistic Compiler (CACM 2009)
  • Hoare, C. A. R. An Axiomatic Basis for Computer Programming (CACM 1969)
  • Reynolds, J. Separation Logic: A Logic for Shared Mutable Data Structures (LICS 2002)
  • https://sel4.systems
  • https://compcert.org