Avancerad

Formell verifiering

Verifiering av programkorrekthet med logiska metoder.

Hoare-logik precondition postcondition loop invariant verifiering

Tänk dig att du bygger en bro. Du skulle aldrig bara hoppas att den håller - du beräknar noggrant belastningar, kontrollerar materialsegenskaper och följer strikta säkerhetsprotokoll. Formell verifiering gör något liknande för datorsystem: istället för att bara testa och hoppas att programmet fungerar, bevisar vi matematiskt att det uppfyller sina specifikationer. När NASA:s rymdsoneder landar på Mars eller när en pacemaker reglerar ett hjärta, är 'det verkar funka' inte tillräckligt - vi behöver absolut säkerhet. Formell verifiering ger oss verktyg för att bevisa korrekthet, säkerhet och tillförlitlighet hos kritiska system.

Fördjupning

Formell verifiering använder matematiska metoder för att bevisa att system uppfyller sina specifikationer. Huvudmetoderna inkluderar model checking (automatisk utforskning av tillståndsutrymmet), theorem proving (interaktiva bevis med bevissassistenter), och abstakt interpretation (säker approximation av programbeteende). Verifieringen kan vara funktionell (korrekthet), säkerhetsrelaterad (safety/security properties), eller prestandarelaterad (timing, minnesbegränsningar). Formell verifiering används inom flygtrafik, medicinteknik, finansiella system och säkerhetskritisk hårdvara.

Grundläggande verifieringsmetoder

Formell verifiering syftar till att bevisa systemegenskaper matematiskt snarare än bara testa dem empiriskt.

Verifiering vs testning

Testning: kör systemet med utvalda indata, observera beteende

Täckning: begränsad till testfall som faktiskt körs

Formell verifiering: bevisa egenskaper för alla möjliga exekveringar

Täckning: komplett - alla möjliga scenarios täcks av beviset

Typer av egenskaper

Säkerhetsegenskaper (Safety):

'Något dåligt händer aldrig'

· Deadlock-frihet

· Minnessäkerhet (no buffer overflow)

· Typsäkerhet

Liveegenskaper (Liveness):

'Något bra händer så småningom'

· Terminering

· Progress (förfrågningar besvaras)

· Fairness

Model checking

Model checking utforskar systematiskt alla möjliga systemtillstånd för att verifiera temporala egenskaper.

Model checking-processen

1. Modellera systemet som finit tillståndsmaskin

2. Specificera egenskaper i temporal logik (LTL/CTL)

3. Kör model checking-algoritm

4. Om egenskap misslyckas: få motexempel-stig

5. Analysera motexempel och korrigera system

Exempel: Mutual exclusion

System: Två processer som delar kritisk sektion

Modell:

· Tillstånd: (process1_state, process2_state)

· process_state ∈ {idle, waiting, critical}

· Övergångar: idle→waiting→critical→idle

Egenskap: AG ¬(critical1 ∧ critical2)

'Aldrig båda processer i kritisk sektion samtidigt'

Model checker verifierar automatiskt denna egenskap.

Model checking-process med tillståndsutforskning

Theorem proving och bevissassistenter

Theorem proving använder interaktiva bevissassistenter för att konstruera formella bevis av systemegenskaper.

Populära bevissassistenter

Coq: baserad på Calculus of Constructions

Lean: modern, utvecklad av Microsoft Research

Isabelle/HOL: Higher-Order Logic

Agda: dependent types och konstruktiv matematik

Bevis av listsorterings-korrekthet

Specifikation:

· sorted(result) - resultatet är sorterat

· permutation(input, result) - samma element

Coq-bevis (förenklat):

Theorem sort_correct : ∀ l,

let result := sort l in

sorted result ∧ permutation l result.

Proof.

induction l.

(* basfall: tom lista *)

simpl. split; auto.

(* induktivt fall: a :: l *)

(* komplext induktivt argument *)

Interaktiv bevisprocess i bevissassistent

Program verification med Hoare-logik

Hoare-logik låter oss resonera om programkorrekthet genom pre- och post-villkor.

Hoare-tripler

{P} C {Q}

Tolkning: Om förvillkor P gäller innan kommando C exekveras, och C terminerar, så gäller eftervillkor Q.

Exempel:

{x ≥ 0} y := x + 1 {y > 0}

Detta säger att om x är icke-negativt innan tilldelningen, så är y positivt efteråt.

Hoare-regler för olika konstruktioner

Tilldelning: {P[x/E]} x := E {P}

Sekvens: {P} C1 {Q}, {Q} C2 {R} ⊢ {P} C1; C2 {R}

If-sats: {P ∧ B} C1 {Q}, {P ∧ ¬B} C2 {Q} ⊢ {P} if B then C1 else C2 {Q}

While-loop: {P ∧ B} C {P} ⊢ {P} while B do C {P ∧ ¬B}

Bevis av arraysortering

Bubble sort-verifiering:

Loop invariant: Efter i iterationer är de första i elementen korrekt placerade

{array.length = n}

for i := 0 to n-1 do

{första i element är sorterade}

for j := 0 to n-i-2 do

{bubble största element uppåt}

if array[j] > array[j+1] then swap(j, j+1)

{element i är på rätt plats}

{array är sorterat}

Abstrakt interpretation

Abstrakt interpretation approximerar programbeteende säkert för att bevisa egenskaper utan att utforska alla konkreta exekveringar.

Abstrakta domäner

Tecken-domän: {+, -, 0, ⊤} för talvärden

Intervall-domän: [a,b] för talintervall

Octagon-domän: ±xi ± xj ≤ c för relationella constraints

Form-domän: för heap-strukturer och pekare

Exempel: Buffertöverflödesanalys

Program:

char buffer[100];

for (int i = 0; i < n; i++) {

buffer[i] = data[i];

}

Abstrakt interpretation:

· Analysera möjliga värden för i: [0, n-1]

· Analysera möjliga värden för n: från kontext

· Om n > 100, rapportera möjligt buffertöverflöde

· Säker över-approximation: kan ge false positives men missar inga verkliga buggar

Abstrakt interpretation med säker approximation

Industriella tillämpningar

Formell verifiering används i kritiska system där fel kan ha katastrofala konsekvenser.

Flygindustrin

ARINC 653 - partitionerade operativsystem:

· Spatial isolation: applikationer kan inte komma åt varandras minne

· Temporal isolation: kritisk timing garanterad

· Formell verifiering av partitioneringsegenskap

DO-178C standard kräver formell verifiering för Level A software (flight-critical).

Medicinteknik

Pacemaker-verifiering: hjärtrytm aldrig för hög/låg

Insulinpumpar: dosering aldrig farlig överdos

Strålbehandling: exakt dosering, ingen felaktig exponering

FDA accepterar formell verifiering som bevis för säkerhet

Processorer och hårdvara

Intel Pentium FDIV-buggen 1994:

· Kostade Intel $475 miljoner

· Ledde till utökad användning av formell verifiering

Modern processorverifiering:

· Floating-point units formellt verifierade

· Cache-koherensprotokoll

· Out-of-order execution correctness

· Memory models och multicore-korrekthet

Vanliga misstag

❌ Felaktig abstraktionsnivå

Modellen kan vara för abstrakt (missar buggar) eller för konkret (tillståndsexplosion)

Exempel: Modellera timer som boolean istället för räknare kan missa timing-relaterade buggar

❌ Ofullständiga specifikationer

Verifiering bevisar bara att implementationen matchar specifikationen

Exempel: Om specifikationen inte kräver säkerhetskontroller kan systemet vara korrekt men osäkert

❌ Tillståndsexplosion

Model checking kan bli omöjligt för stora system

Exempel: System med n booleska variabler har 2ⁿ tillstånd - växer exponentiellt

Tillämpningar

Säkerhetskritiska system

System där fel kan äventyra liv eller säkerhet

Exempel: Flygtrafikkontroll, kärnkraftverk, medicinska enheter, autonoma fordon

Finansiella system

Transaktionssystem där fel kan kosta miljoner

Exempel: Högfrekvenshandel, betalningssystem, smart contracts på blockchain

Cybersäkerhet

Säkerhetsprotokoll och kryptografiska system

Exempel: TLS/SSL-protokoll, kryptografiska primitiver, säkra operativsystem

Kompilerare och verktyg

Verktyg som andra förlitar sig på måste vara korrekta

Exempel: CompCert (verifierad C-kompilator), seL4 (verifierat mikrokernel)

Övningar

1 Lätt

Skriv en Hoare-tripel för att verifiera att x := x + 1 ökar x med exakt 1

Tips

Använd en variabel för ursprungliga värdet av x

Visa facit

x₀ representerar ursprungliga värdet av x
Förvillkor: x = x₀ (x har värdet x₀)
Kommando: x := x + 1 (öka x med 1)
Eftervillkor: x = x₀ + 1 (x är nu 1 större än ursprungsvärdet)
Detta bevisar att tilldelningen ökar x med exakt 1

Svar: {x = x₀} x := x + 1 {x = x₀ + 1}

2 Medel

Formulera en temporal logik-egenskap som säger att en elevator så småningom besöker alla våningar

Tips

Använd LTL och tänk på att varje våning måste besökas infinit ofta

Visa facit

GF floor_i betyder 'globalt, så småningom floor_i'
Detta är ekvivalent med 'floor_i besöks oändligt ofta'
För alla våningar: ∧ᵢ₌₁ᴺ GF floor_i
Alternativt: G(request_i → F floor_i) - varje förfrågan besvaras
Detta säkerställer att hissen inte 'glömmer' någon våning

Svar: GF floor1 ∧ GF floor2 ∧ ... ∧ GF floorN

3 Svår

Designa en abstrakt domän för att upptäcka division med noll

Tips

Behöver skilja mellan värden som kan vara noll och värden som garanterat inte är noll

Visa facit

ZERO: värdet är definitivt 0
NON_ZERO: värdet är definitivt inte 0
MAYBE_ZERO: värdet kan vara 0 eller inte
⊤: ingen information (top element)
Abstrakta operationer:
• x + y: om båda är ZERO då ZERO, annars MAYBE_ZERO
• x * y: om någon är ZERO då ZERO
• x / y: om y är ZERO rapportera fel, om NON_ZERO så säkert

Svar: Domän: {ZERO, NON_ZERO, MAYBE_ZERO, ⊤}

Sammanfattning

Formell verifiering använder matematiska metoder för att bevisa att system uppfyller sina specifikationer. Huvudmetoderna är model checking (automatisk tillståndsutforskning), theorem proving (interaktiva bevis), och abstrakt interpretation (säker approximation). Hoare-logik möjliggör programverifiering genom pre/post-villkor. Formell verifiering är avgörande för säkerhetskritiska system inom flyg, medicin, finans och cybersäkerhet, där traditionell testning inte ger tillräckliga säkerhetsgarantier. Tekniken balanserar uttryckskraft mot automatisering och skalbarhet.