Formale Verifikation für sicherheitskritische Verteidigungssoftware: Methoden, Werkzeuge und Nachweise

Von Corvus Intelligence Engineering Team · Über das Team →

25. Juni 2026 13 Min. Lesezeit

Jedes Software-Verifikationsprogramm stößt schließlich auf dasselbe strukturelle Problem: Testen ist begrenzt. Ein Testsuite, so umfangreich er auch sein mag, deckt eine endliche Teilmenge von Eingaben und Ausführungspfaden ab. Die verbleibenden, nicht getesteten Kombinationen stellen eine implizite Annahme dar, dass das nicht getestete Verhalten korrekt ist. Für die meisten kommerziellen Software-Anwendungen ist diese Annahme akzeptabel; die Kosten eines unentdeckten Fehlers sind behebbar. Für Software-Sicherheit in Verteidigungssystemen — Code, der Waffen, Flugsteuerungsflächen oder lebenswichtige Unterstützungsfunktionen steuert — kann ein einziger Fehler in einem nicht getesteten Pfad katastrophal sein. Die formale Verifikation schließt diese Lücke nicht durch das Ausführen weiterer Tests, sondern indem ausführungsbasierte Evidenz durch mathematischen Beweis ersetzt wird.

Formale Methoden umfassen eine Familie von Techniken — Model Checking, Theorem Proving und abstrakte Interpretation — die mathematisch über den vollständigen Raum möglicher Programmverhalten schlussfolgern. Jede bietet unterschiedliche Kompromisse zwischen Ausdrucksstärke, Automatisierung, Skalierbarkeit und der Stärke des erzeugten Nachweises. Dieser Artikel untersucht jede Technik im Kontext der Entwicklung von Verteidigungssoftware, erläutert, wie sie in die DO-178C DAL A-Zertifizierung und die MIL-STD-882-Sicherheitsanalyse integriert werden, und liefert eine realistische Einschätzung, wo formale Methoden sich auszahlen und wo nicht.

Warum Testen allein keine Sicherheitsgarantie bietet

Die Grenzen des Testens als alleinige Verifikationsstrategie sind nicht primär eine Frage der Testmenge; sie sind struktureller Natur. Drei Probleme kumulieren sich und machen eine reine testbasierte Zusicherung für sicherheitskritische Systeme unzureichend.

Die Abdeckungsgrenze. Strukturelle Abdeckungsmetriken — Anweisungsabdeckung, Zweigabdeckung, Modified Condition/Decision Coverage (MC/DC) — messen den Anteil der von einem Testsuite abgedeckten Codestrukturen. DO-178C schreibt MC/DC-Abdeckung für DAL A-Software vor, weil damit sichergestellt wird, dass jedes Entscheidungsergebnis und jede Bedingung innerhalb jeder Entscheidung nachweislich unabhängig das Ergebnis beeinflusst. Dennoch erschöpft selbst 100% MC/DC-Abdeckung den Eingaberaum nicht: Eine Funktion mit fünf 32-Bit-Integer-Parametern hat 2¹⁶⁰ mögliche Eingabekombinationen. Ein Testsuite, der 100% MC/DC-Abdeckung demonstriert, kann Dutzende oder Hunderte von Ausführungspfaden abdecken, aber nichts über die Korrektheit von Ausführungen aussagen, die bestimmte Eingabewerte auf nicht getestete Weise kombinieren. Die Abdeckungsgrenze ist kein Problem der Testqualität — sie ist eine mathematische Tatsache über das endliche Testen unendlicher Räume.

Kombinatorische Explosion in nebenläufigen Systemen. Sicherheitskritische Verteidigungssoftware ist fast immer nebenläufig: mehrere Tasks, die parallel ausgeführt werden, Speicher teilen, Nachrichten über Warteschlangen und Semaphore austauschen und Interrupts ausgesetzt sind, die die Ausführung an beliebigen Punkten unterbrechen können. Die Anzahl möglicher Verschachtelungen von N nebenläufigen Tasks mit je K Schritten wächst als O(K^N). Ein System mit drei Tasks à zehn Schritten hat über eine Milliarde möglicher Verschachtelungen. Tests decken eine Handvoll davon ab; Abdeckungsmetriken sagen nichts über die nicht getesteten Verschachtelungen aus. Race Conditions, Prioritätsinversionen und Deadlocks verbergen sich in den Verschachtelungen, die Tests zufällig nicht abdecken.

Die Rolle formaler Methoden. Formale Verifikation löst diese Probleme, indem Enumeration durch Beweis ersetzt wird. Statt zu fragen „Hat sich das System für diese Eingaben korrekt verhalten?" fragt sie: „Ist es mathematisch unmöglich, dass sich das System für eine beliebige Eingabe falsch verhält?" Die Frage ist schwerer und kostspieliger zu beantworten, aber die Antwort — wenn positiv — ist kategorisch stärker. Deshalb schreiben die Luftfahrtbranche, die Nuklearindustrie und der Verteidigungssektor formale Methoden für die höchsten Design-Assurance-Levels vor oder fördern sie: Testen schafft Vertrauen; formale Verifikation schafft Gewissheit innerhalb der Grenzen des formalen Modells und seiner Annahmen.

Die Begleitdisziplin der statischen Codeanalyse für Verteidigungssoftware liegt zwischen Testen und formaler Verifikation: Statische Analysetools untersuchen Quellcode ohne Ausführung und identifizieren Fehlerklassen, die Tests übersehen, typischerweise jedoch ohne die mathematischen Korrektheitsnachweise, die formale Methoden liefern.

Model Checking: erschöpfende Zustandsraumverifikation

Model Checking ist die am breitesten anwendbare formale Verifikationstechnik für Verteidigungssoftware, weil sie die am stärksten automatisierte ist. Ausgehend von einem formalen Modell eines Systems und einer in temporaler Logik ausgedrückten Eigenschaft durchsucht ein Model Checker erschöpfend alle erreichbaren Zustände und bestätigt, dass die Eigenschaft in jedem Zustand gilt — oder erzeugt ein Gegenbeispiel, das eine Verletzung demonstriert.

Temporallogische Eigenschaften für Verteidigungssysteme. Linear Temporal Logic (LTL) und Computation Tree Logic (CTL) sind die zwei primären Eigenschaftssprachen im Model Checking. LTL-Eigenschaften drücken Einschränkungen für einzelne Ausführungspfade aus. Eine typische Sicherheitseigenschaft in der Verteidigung: Global gilt: Wann immer das System den Scharf-Zustand einnimmt, müssen im nächsten Zustand sowohl die Sicherheitsverriegelung freigegeben als auch die Bedienerbestätigung vorhanden sein. CTL-Eigenschaften schlussfolgern über verzweigte Berechnungsbäume — und drücken z. B. aus, dass von jedem erreichbaren Zustand immer ein Wiederherstellungspfad existiert. Verteidigungsanwendungen umfassen die Verifikation, dass Kommunikationsprotokoll-Zustandsmaschinen niemals undefinierte Zustände annehmen, dass die Planungslogik unter jeder gültigen Task-Reihenfolge stets Fristen einhält, und dass Sicherheitsverriegelungssequenzen durch keine Kombination gültiger Eingaben umgangen werden können.

Werkzeuge: SPIN und NuSMV. SPIN ist ein expliziter Zustandsmodell-Checker, der primär zur Verifikation nebenläufiger Software und Kommunikationsprotokolle eingesetzt wird. Seine Eingabesprache, Promela, modelliert nebenläufige Prozesse, die über Nachrichtenkanäle kommunizieren; Eigenschaften werden in LTL ausgedrückt. SPIN verifiziert durch Tiefensuche mit hash-basierter Zustandsspeicherung und erzeugt Gegenbeispielverfolgungen, die in einem Simulator wiedergegeben werden können. NuSMV ist ein symbolischer Model Checker, der Binary Decision Diagrams (BDDs) und begrenztes Model Checking mit SAT-Solvern verwendet, um Zustandsmengen symbolisch darzustellen und zu erkunden — was ihn für Systeme mit großen Zustandsräumen effektiv macht, wo explizite Enumeration nicht durchführbar ist. Für Verteidigungssoftwareprotokolle und Zustandsmaschinen ist SPIN typischerweise besser geeignet; für eingebettete Steuerungslogik, die auf Register-Transfer-Ebene modelliert wird, ist NuSMVs symbolischer Ansatz oft praktischer.

Das Zustandsexplosionsproblem und CEGAR. Der erreichbare Zustandsraum wächst exponentiell mit der Systemgröße. Counterexample-Guided Abstraction Refinement (CEGAR) ist die wichtigste praktische Technik zur Handhabung dieses Problems. Der Arbeitsablauf beginnt mit einem groben abstrakten Modell, das klein genug zur Verifikation ist, aber möglicherweise spuriöse Verhaltensweisen einführt, die im konkreten System nicht vorhanden sind. Wenn die Eigenschaft auf dem abstrakten Modell gilt, gilt sie aufgrund der Korrektheit der Abstraktion auch auf dem konkreten System. Wird ein Gegenbeispiel gefunden, wird es gegen das konkrete Modell geprüft: Weist das konkrete Modell das Gegenbeispiel ebenfalls auf, handelt es sich um einen echten Fehler; wenn nicht, wird die Abstraktion verfeinert, indem im Bereich des spuriösen Gegenbeispiels mehr Detail hinzugefügt wird. CEGAR ist iterativ und kann zu einem Verifikationsergebnis konvergieren, ohne den vollständigen Zustandsraum explizit darzustellen.

/* SPIN Promela-Fragment: Waffenfreigabe-Verriegelung */
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-Eigenschaft: Freigabe nur wenn beide Vorbedingungen erfüllt */
ltl p1 { [] (release_state == RELEASED ->
              (safety_state == ARMED && confirm_state == RELEASED)) }

Wenn ein Model Checker eine Eigenschaftsverletzung findet, erzeugt er eine Gegenbeispielverfolgung — eine vollständige Abfolge von Systemzuständen vom Anfangszustand bis zum verletzenden Zustand. Diese Verfolgung ist direkt verwertbar: Sie gibt genau an, welche Ereignissequenz zum unsicheren Zustand führt, sodass Entwickler den Fehler deterministisch reproduzieren und eine Lösung entwickeln können. Gegenbeispiele aus der dokumentierten Verifikation von C2-Protokollen in der Verteidigung haben Authentifizierungs-Umgehungen aufgedeckt, die nur unter bestimmten Kombinationen von Nachrichtenverzögerung und Neuübertragung möglich waren — Szenarien, die monatelang in Integrationstests nie aufgetreten waren.

Theorem Proving: maschinell geprüfte mathematische Beweise

Während Model Checking einen begrenzten Zustandsraum automatisch erschöpft, konstruiert Theorem Proving einen mathematischen Beweis einer Eigenschaft, die über einen unbegrenzten oder parametrisierten Bereich gilt — was es zur Technik der Wahl macht, wenn die zu verifizierende Eigenschaft reelle Arithmetik, unbegrenzte Datenstrukturen oder parametrisierte Algorithmen umfasst, die kein endlicher Zustandsraum darstellen kann.

Coq, Isabelle/HOL und PVS in der Verteidigung. Coq ist ein Beweisassistent, der auf abhängiger Typentheorie aufbaut; sein Extraktionsmechanismus kann verifizierten ausführbaren Code direkt aus einer bewiesenen Spezifikation erzeugen und schafft so eine Kette vom Beweis zum laufenden Binärprogramm. Er wurde zur Verifikation kryptografischer Algorithmen und Compilertransformationen eingesetzt. Isabelle/HOL bietet eine Logik höherer Ordnung mit leistungsstarken Taktiken für die Automatisierung; der seL4-Microkernel — der am gründlichsten verifizierte Betriebssystem-Kernel, der je existiert hat — wurde in Isabelle/HOL korrekt bewiesen und demonstriert damit, dass das binäre Programm seine formale Spezifikation korrekt implementiert. PVS, entwickelt am SRI International, wurde speziell für die Software-Spezifikation entworfen und wurde auf NASA-Flugsoftware und Sicherheitssystemlogik für Nuklearanlagen angewendet. Alle drei wurden in Verteidigungskontexten eingesetzt: Coq für Protokoll- und Algorithmusbeweise, Isabelle für Betriebssystem- und Plattformsoftware, PVS für Spezifikationsebenen-Überlegungen in der Avionik und bei Raumsystemen.

Erzeugung von Beweispflichten. Moderne formale Methoden-Workflows erzeugen Beweispflichten automatisch aus annotiertem Quellcode und reduzieren so den Aufwand für das Schreiben von Spezifikationen von Grund auf. Tools wie Frama-C mit seinem WP-Plugin (Weakest Precondition) analysieren mit ACSL (ANSI/ISO C Specification Language) annotierte C-Quellcode-Verträge und erzeugen Beweispflichten, die durch automatisierte Beweiser (Alt-Ergo, CVC4, Z3) oder durch interaktive Theorem Prover abgeleitet werden können, wenn die Automatisierung versagt. Die Sprache SPARK für Ada bietet einen ähnlichen integrierten Workflow: SPARK-Code wird mit Vor-/Nachbedingungsverträgen geschrieben, und GNATprove erzeugt und versucht automatisch, Beweispflichten abzuleiten, und greift nur für Pflichten auf interaktiven Beweis zurück, die die Automatisierung nicht bewältigen kann. Dieser hybride Ansatz — Maximierung der Automatisierung bei gleichzeitiger Reservierung menschengeführter Beweise für die schwierigen Fälle — ist das praktische Modell für Verteidigungsprogramme, die kein Team von Beweistheoretikern beschäftigen können.

Der Kompromiss der Lernkurve. Die Lücke zwischen dem Wert, den Theorem Proving liefern kann, und dem erforderlichen organisatorischen Investment ist die zentrale Herausforderung bei der Einführung der Technik. Das Schreiben von Spezifikationen in Coq oder Isabelle erfordert Kenntnisse in Logik höherer Ordnung und Typentheorie, die eine standardmäßige Software-Engineering-Ausbildung nicht vermittelt. Die Beweiserstellung wird für nicht-triviale Komponenten in Ingenieur-Monaten gemessen. Programme, die dieses Investment unterschätzen, überschreiten konsequent den Zeitplan. Der realistische Weg besteht darin, spezialisierte Theorem-Proving-Arbeit von Organisationen zu erwerben, die bereits über die Fähigkeit verfügen, und ihren Umfang auf die Komponenten zu beschränken, bei denen keine andere Technik ausreichend ist — typischerweise die Algorithmen, auf denen der Sicherheitsnachweis aufgebaut ist.

Abstrakte Interpretation und korrekte statische Analyse

Abstrakte Interpretation nimmt eine praktische Mittelstellung zwischen konventioneller statischer Analyse (die typischerweise nicht korrekte Ergebnisse liefert — sie kann Fehler übersehen) und Theorem Proving (das korrekt, aber manuellen Aufwand erfordert) ein. Ein abstraktes Interpretationswerkzeug berechnet eine korrekte Überapproximation: Wenn es keinen Fehler meldet, ist das konkrete Programm garantiert frei von Fehlern dieser Klasse. Wenn es einen potenziellen Fehler meldet, kann das Programm den Fehler haben oder auch nicht — der Bericht ist ein konservativer Alarm, der untersucht werden muss.

Astrée. Astrée (entwickelt an der ENS Paris/INRIA und kommerzialisiert von AbsInt) ist das prominenteste abstrakte Interpretationswerkzeug in Verteidigungs- und Luftfahrtkontexten. Es analysiert C-Quellcode auf folgende Laufzeitfehlerklassen: Integer-Überlauf und -Unterlauf (vorzeichenbehaftet und vorzeichenlos), Division durch null, Null-Zeiger-Dereferenzierung, Out-of-bounds-Array-Zugriff, ungültige Bit-Shift-Anzahlen und Lesezugriffe auf nicht initialisierte Variablen. Es wurde verwendet, um das Fehlen von Laufzeitfehlern in der primären Flugsoftware des Airbus A380 nachzuweisen — etwa 132.000 Zeilen C ohne ungelöste Alarme nach der Analyse. Für eingebettete Verteidigungssoftware wird Astrée auf Modulebene angewendet; jedes Modul muss null echte Alarme erreichen, bevor es als formal verifiziert hinsichtlich der Abwesenheit von Laufzeitfehlern gilt.

Polyspace von MathWorks. Polyspace Bug Finder und Polyspace Code Prover bieten ähnliche abstrakte Interpretationsfähigkeiten mit engerer Integration in die MathWorks-Toolchain (MATLAB/Simulink modellbasierte Entwicklung), die in eingebetteten Verteidigungssystemen verbreitet ist. Code Prover verwendet intervallbasierte abstrakte Interpretation, um das Fehlen bestimmter Fehlerklassen zu beweisen — nicht nur zu erkennen — und klassifiziert jeden Check als Bewiesen (kein Fehler möglich), Unbewiesen (nicht bestimmbar) oder Fehler (Defekt bestätigt). Sowohl Astrée als auch Polyspace liefern DO-330-Werkzeugqualifizierungskits und reduzieren damit den Programmaufwand für regulatorische Anerkennung.

Fehlerklasse	Astrée	Polyspace Code Prover	Korrektheit
Integer-Überlauf / -Unterlauf	Ja	Ja	Korrekt (kein Übersehen)
Null-Zeiger-Dereferenzierung	Ja	Ja	Korrekt (kein Übersehen)
Division durch null	Ja	Ja	Korrekt (kein Übersehen)
Out-of-bounds-Array-Zugriff	Ja	Ja	Korrekt (kein Übersehen)
Lesezugriffe auf nicht initialisierte Variablen	Ja	Ja	Korrekt (kein Übersehen)

Verwaltung falsch positiver Ergebnisse. Korrekte Werkzeuge melden konservativ: Bei Unsicherheit schlagen sie Alarm. In großen C-Codebasen mit komplexer Zeigerarithmetik, Umgebungs-Stubs für nicht modellierte Hardware-Schnittstellen oder plattformspezifischen Compiler-Erweiterungen können falsch positive Raten hoch sein — 30–70% bei einem ersten Durchlauf ist nicht ungewöhnlich. Die Disziplin besteht darin, jeden falsch positiven Alarm mit einer maschinenlesbaren Begründung zu annotieren, die das Werkzeug als Unterdrückung akzeptiert, sodass der unterdrückte Alarm bei nachfolgenden Durchläufen nicht erneut erscheint. Jede Unterdrückung ist eine Behauptung — „Dieser Alarm kann zur Laufzeit nicht eintreten, weil [Grund]" — und Behauptungen müssen bei Codeüberprüfungen als Teil des Sicherheitsnachweises geprüft werden. Das Unterdrückungsprotokoll ist selbst ein Sicherheitsartefakt; ein Modul mit vielen Unterdrückungen verdient zusätzliche Prüfung.

Anwendung formaler Methoden auf DO-178C DAL A-Software

DO-178C, der primäre Zertifizierungsstandard für Avionik-Software und der Standard, der am häufigsten analog auf andere sicherheitskritische Verteidigungsplattformen angewendet wird, enthält ein Ergänzungswerk für formale Methoden — DO-333 (Formal Methods Supplement to DO-178C and DO-278A) — das definiert, wie formale Analyseaktivitäten DO-178C-Verifikationsziele erfüllen können.

Ergänzung versus Ersatz des Testens. Ein verbreitetes Missverständnis ist, dass formale Verifikation den Testbedarf unter DO-178C eliminiert. DO-333 unterstützt dies nicht. Formale Methoden sind eine Ergänzung: Sie können Anerkennung für spezifische Verifikationsziele liefern, die andernfalls durch Testen erfüllt würden, und so den Testumfang reduzieren, ersetzen aber nicht die gesamte Testanforderung. Die typische Anwendung besteht darin, formale Analyse zur Erfüllung von Strukturabdeckungszielen zu nutzen — ein korrekter abstrakter Interpretationsbeweis, dass in einem Modul kein Laufzeitfehler erreichbar ist, bietet äquivalente Sicherheit zur Ausführung jedes Zweiges dieses Moduls und kann als Abdeckungsgutschrift beansprucht werden — während konventionelles Testen weiterhin anforderungsbasierte Testziele erfüllt. Das Nettoergebnis ist ein reduzierter Testumfang für DAL A-Module bei erhöhter Nachweistiefe für die Eigenschaften, auf die formale Analyse abzielt.

PSAC- und SAS-Dokumentation. Der Plan for Software Aspects of Certification (PSAC) muss den Ansatz für formale Methoden bei Programmbeginn beschreiben: welche formalen Methoden verwendet werden, welche DO-178C-Ziele sie adressieren, welche Werkzeuge verwendet werden und wie die Werkzeuge qualifiziert werden. Dieses Planungsartefakt wird von der Zertifizierungsbehörde vor Beginn der formalen Verifikationsarbeit geprüft — dem Zertifizierer einen formalen Methodennachweis erst nach Abschluss zu präsentieren ist ein Prozessfehler, der die Anerkennung ungültig machen kann. Das Software Accomplishment Summary (SAS) dokumentiert die formalen Verifikationsaktivitäten als abgeschlossen und liefert eine Rückverfolgbarkeit von jedem formalen Ergebnis zum DO-178C-Ziel, das es erfüllt. Die formale Verifikationsevidenz — Werkzeugausgaben, Eigenschaftsdateien, Modelldateien, Alarmdispositionsprotokolle — wird im Konfigurationsmanagementsystem als Teil der Zertifizierungslebenszyklus-Daten aufbewahrt.

Werkzeugqualifizierung. DO-330 definiert die Qualifizierungsanforderungen für Software-Werkzeuge, die in der Entwicklung von Avionik-Software verwendet werden. Werkzeuge, deren Ausgabe ohne unabhängige Verifikation im Compliance-Nachweis verwendet wird, erfordern eine Qualifizierung, die dem DAL und der Rolle des Werkzeugs entspricht. Abstrakte Interpretationswerkzeuge, die zur Erfüllung von DAL A-Verifikationszielen eingesetzt werden, erfordern TQL-1-Qualifizierung — das strengste Niveau. Kommerzielle Werkzeuge wie Astrée und Polyspace bieten Qualifizierungs-Support-Kits, die Werkzeugbetriebsanforderungen, Qualifizierungstestverfahren und Qualifizierungstestergebnisse enthalten. Die Verantwortung des Programms besteht darin, festzustellen, dass das Kit auf den spezifischen Verwendungskontext anwendbar ist: den spezifischen Compiler, das Betriebssystem und die verwendete Sprachuntermenge. Open-Source-Werkzeuge ohne vorhandene Qualifizierungskits erfordern, dass das Programm alle Qualifizierungsartefakte von Grund auf erstellt — ein erheblicher Programmaufwand, der ab dem ersten Tag im Projektplan berücksichtigt werden muss.

DO-178C / DO-333 Grundprinzip: Formale Methodenanerkennung im Compliance-Nachweis wird durch die Qualität des Rückverfolgbarkeitsarguments verdient — es muss nachgewiesen werden, dass die formal verifizierte Eigenschaft genau der Sicherheitsanforderung entspricht, deren Erfüllung sie beansprucht. Eine formal verifizierte Eigenschaft, die die Anforderung nur annähernd erfasst, bietet keine regulatorische Anerkennung und kann den Sicherheitsnachweis eher schwächen als stärken.

MIL-STD-882-Gefahrenelimination und formale Verifikation

MIL-STD-882E (System Safety) definiert die bevorzugte Hierarchie von Gefahrenkontrollen in abnehmender Wirksamkeit: Gefahr eliminieren, Eintrittswahrscheinlichkeit reduzieren, Erkennung oder Warnung hinzufügen, und Restrisiko mit dokumentierter Begründung akzeptieren. Formale Verifikation trägt direkt zu den ersten beiden Ebenen bei und liefert das am besten vertretbare Sicherheitsargument, wenn sie dies tut.

Gefahrenelimination durch Unmöglichkeitsbeweis. Wenn ein Model-Checking-Beweis demonstriert, dass eine temporale Eigenschaft für alle erreichbaren Zustände gilt — zum Beispiel, dass der Zündenergiekreis niemals aktiviert werden kann, wenn das Sicherheitsverriegelungs-Flag gesetzt ist — stellt dies eine Behauptung der Gefahrenelimination für den softwarekausalen Pfad dieser Gefahr dar. Der Gefahrenprotokolleintrag für die entsprechende Gefahr kann aktualisiert werden, um zu zeigen, dass der softwarekausale Pfad durch formalen Beweis eliminiert wurde, und die Restrisikobewertung spiegelt nur die verbleibenden hardwarekausalen Pfade wider. Dies ist kategorisch stärker als das Risikominderungsargument aus dem Testen, das nur belegen kann, dass die Gefahr während der Testläufe nicht ausgelöst wurde.

Wahrscheinlichkeitsreduktiongutschrift durch korrekte Analyse. Wo Elimination nicht erreichbar ist — weil die Gefahr von Bedingungen außerhalb der Softwarekontrolle abhängt — liefert formale Analyse eine Schranke für den Beitrag der Software zur Ausfallwahrscheinlichkeit. Ein abstrakter Interpretationsbeweis, dass Integer-Überlauf im Navigationsalgorithmus nicht auftreten kann, begrenzt die Rate stiller Datenkorrumpierung auf null für diese Fehlerklasse und reduziert direkt den Softwareausfallratenterm in der probabilistischen Risikoanalyse. Diese Schranke ist vertretbarer als eine testbasierte Ausfallratenschätzung, weil die formale Schranke innerhalb der Modellannahmen exakt ist, während die testbasierte Schätzung ein Konfidenzintervall über eine endliche Stichprobe ist.

Rückverfolgung formaler Beweise zu Gefahrenursachen. Das Sicherheitsargument ist vollständig, nur wenn jedes formale Ergebnis explizit zur Gefahrenursache, die es adressiert, zurückverfolgt wird. Die Rückverfolgbarkeitskette lautet: formale Eigenschaft → Softwareanforderung → Softwaregefahrenursache → System-Hazard-Analysis-Eintrag. Diese Kette muss im Software Safety Analysis-Dokument dokumentiert und im formalen Verifikationsevidenzpaket querverwiesen werden. Ein formaler Beweis, der ohne diese Rückverfolgbarkeit existiert, ist ein Qualitätssicherungsasset, aber kein Sicherheitsargument — er demonstriert Verifikationsaktivität, ohne Sicherheitsauswirkung zu demonstrieren.

Die Verbindung formaler Verifikationsergebnisse mit der breiteren Disziplin der DevSecOps für Verteidigungspipelines bedeutet, dass formale Analyseläufe in die kontinuierliche Integrationspipeline als automatisierte Tore integriert werden können — die die Integration jedes Moduls blockieren, das neue ungelöste Alarme einführt — anstatt nur als späte Zertifizierungsaktivitäten ausgeführt zu werden.

Praktische Integration in ein Verteidigungssoftwareprojekt

Die zentrale Herausforderung bei der Einführung formaler Verifikation in ein Verteidigungssoftwareprojekt ist nicht technischer Natur — die Werkzeuge existieren und die Techniken sind ausgereift. Es ist die Ressourcenallokation: Formale Methoden erfordern Investitionen, die gegen konkurrierende Programmprioritas gerechtfertigt werden müssen, und die Investition ist frontgeladen, während die Vorteile spät realisiert werden.

Wo zu investieren: kritische Algorithmen versus Wrapper. Die Rendite aus formalen Verifikationsinvestitionen ist am höchsten, wo die Komponente mathematisch präzise, klein genug für eine handhabbare Modellierung und mit einer hohen Schweregrad-Gefahr verbunden ist. Regelkreisalgorithmen, Planungslogik, Sicherheitsverriegelungssequenzierung und kryptografische Primitive-Implementierungen sind die kanonischen Ziele. Umgekehrt haben große Integrationsschicht-Komponenten, Benutzeroberflächencode, Daten-Marshalling-Schichten und Konfigurationsmanagement-Logik komplexe Schnittstellen und geringe mathematische Präzision — der Spezifikationsschreibaufwand nähert sich dem Implementierungsaufwand, und das formale Modell muss parallel zum Code gepflegt werden. Eine vertretbare Daumenregel: Formale Methoden anwenden, wo das Verhalten der Komponente in weniger Seiten spezifiziert als implementiert werden kann, und wo die spezifizierte Eigenschaft direkt einer Gefahrenursache in der System Hazard Analysis entspricht.

Team-Skill-Anforderungen. Abstrakte Interpretationswerkzeuge sind der Einstiegspunkt mit der niedrigsten Einstiegshürde und sollten zuerst eingeführt werden. Ingenieure mit C/C++-Embedded-Hintergrund können Astrée oder Polyspace nach einigen Tagen Training produktiv einsetzen; die primäre Fähigkeit ist Alarm-Triage — echte Fehler von falsch positiven Ergebnissen zu unterscheiden. Model Checking erfordert Ingenieure, die Promela- oder SMV-Modelle schreiben und Eigenschaften in LTL/CTL ausdrücken können; diese Fähigkeit braucht Wochen bis Monate zur Entwicklung, wird nicht breit gelehrt und sollte ab Programmbeginn in Einstellungs- oder Ausbildungspläne einbezogen werden. Theorem Proving erfordert Expertise in formaler Logik und Beweistheorie, die die meisten Programme eher von Spezialisierungsorganisationen beauftragen als intern entwickeln werden. Die Planung der formalen Methoden-Personalbesetzung als Nachgedanke — „Wir werden herausfinden, wer die formale Verifikation macht, wenn wir sie brauchen" — ist die häufigste Einzelursache dafür, dass formale Methodenpläne nicht ausgeführt werden.

Realistische Kosten-Nutzen-Erwartungen. Eine realistische Erwartung für ein Programm, das abstrakte Interpretation in DAL A-Module einführt, ist eine 15–30%ige Reduzierung der erforderlichen Testfälle für strukturelle Abdeckung, ausgeglichen gegen etwa 5–10% zusätzlichen Ingenieuraufwand für Alarm-Triage und Unterdrückungsdokumentation im ersten Programmzyklus. Im zweiten Zyklus reduziert die Vertrautheit mit den Alarmmustern des Werkzeugs für die spezifische Codebasis den Triageaufwand, und der Nettonutzen verbessert sich. Model Checking für Zustandsmaschinen fügt 10–20% Kosten zur Entwurfsphase der spezifisch anvisierten Komponenten hinzu, eliminiert aber eine ganze Fehlerklasse — Zustandsmaschinenverletzungen, Protokollfehler — die andernfalls im Integrationstest oder im Feld gefunden würde. Theorem Proving ist die kostspieligste und wertvollste Technik und sollte auf einer Komponentenbasis mit expliziter Kosten-Nutzen-Dokumentation vor der Verpflichtung bewertet werden.

Abstrakte Interpretation (Astrée, Polyspace): niedrigste Einstiegshürde, ausgereifte Werkzeuge, DO-330-Kits verfügbar — auf alle DAL A C/C++-Module anwenden
Model Checking (SPIN, NuSMV): auf Zustandsmaschinen, Protokolle und Moduswechsel-Logik anwenden, wo der Zustandsraum handhabbar ist
Theorem Proving (Coq, Isabelle/HOL, PVS, SPARK/GNATprove): für Algorithmen reservieren, wo mathematische Korrektheit ein primäres Sicherheitsargument ist und keine andere Technik ausreicht
Werkzeugqualifizierung: DO-330 TQL im PSAC planen; kommerzielle Qualifizierungskits verwenden wo verfügbar; Open-Source-Werkzeugqualifizierung explizit budgetieren
MIL-STD-882-Rückverfolgbarkeit: jedes formale Ergebnis zu einer Gefahrenursache zurückverfolgen, bevor Sicherheitsgutschrift beansprucht wird — nicht rückverfolgbare Verifikation ist kein Sicherheitsargument

Programme, die formale Verifikation erfolgreich integrieren, behandeln sie als erstklassige Ingenieurdisziplin mit dediziertem Personal, geplanter Werkzeugqualifizierung, expliziter Anforderungsrückverfolgbarkeit und einem realistischen Umfang, der auf die Komponenten beschränkt ist, bei denen formale Methoden die Sicherheitsklassifizierung einer Gefahr ändern. Programme, die formale Verifikation als Compliance-Kontrollkästchen behandeln, das am Ende der Entwicklung hinzugefügt wird, stellen konsequent fest, dass die formale Analyse die Compliance-Behauptung nicht unterstützt, weil der Code nicht mit formaler Analyse im Sinn entworfen wurde. Entwurf und formales Modell müssen gemeinsam entwickelt werden — die Spezifikationsdisziplin, die formale Methoden erfordern, ist genauso wertvoll wie der Beweis selbst.

Formale Verifikation in Ihr Verteidigungssoftwareprogramm integrieren

Corvus Intelligence wendet formale Methoden — abstrakte Interpretation, Model Checking und Theorem Proving — auf sicherheitskritische Verteidigungssoftwareprogramme an, die unter DO-178C und MIL-STD-882 betrieben werden. Wenn Ihr Programm DAL A-Sicherheit erfordert oder einen Software-Sicherheitsnachweis stärken muss, stehen wir zur Verfügung, um Ihre Verifikationsanforderungen zu besprechen.

Verteidigungssoftware-Entwicklung → Briefing buchen

Diese Analyse wurde von Corvus Intelligence-Ingenieuren erstellt, die sicherheitskritische Software für Verteidigungs- und Regierungsorganisationen entwickeln und verifizieren. Erfahren Sie mehr über unser Team →

Häufig gestellte Fragen

Was ist formale Verifikation und worin unterscheidet sie sich vom Software-Testen?

Formale Verifikation verwendet mathematische Beweistechniken, um nachzuweisen, dass ein Softwaresystem eine präzise formulierte Spezifikation erfüllt, während Testen das Programm gegen eine endliche Menge von Eingaben ausführt und Ausgaben beobachtet. Der grundlegende Unterschied ist die Vollständigkeit: Testen kann das Vorhandensein von Fehlern zeigen, aber nicht ihre Abwesenheit beweisen, weil kein endlicher Testsuite alle möglichen Eingaben und Zustände abdeckt. Formale Verifikation schlussfolgert über den vollständigen Raum möglicher Verhaltensweisen — wenn sie erfolgreich ist, liefert sie eine Garantie, die für jede Ausführung gilt, nicht nur für die getesteten. In der Praxis ergänzen formale Methoden das Testen, anstatt es zu ersetzen: Sie werden auf die kritischsten Eigenschaften angewendet, wo die Kosten unentdeckter Fehler am höchsten sind und wo Testabdeckung strukturell nicht erreichbar ist. Für sicherheitskritische Verteidigungssoftware kann selbst ein einziger nicht getesteter Pfad mit einem Fehlermodus ein inakzeptables Sicherheitsrisiko darstellen — genau diese Lücke adressieren formale Methoden.

Was ist Model Checking und welche Arten von Eigenschaften kann es verifizieren?

Model Checking ist eine formale Verifikationstechnik, die erschöpfend alle erreichbaren Zustände eines endlichen Zustandsmodells eines Systems durchsucht und in jedem Zustand prüft, ob eine in temporaler Logik ausgedrückte Eigenschaft gilt. LTL-Eigenschaften drücken Anforderungen über Zustandssequenzen aus — zum Beispiel: „Wann immer das Waffenscharfschalte-Flag gesetzt ist, muss die Sicherheitsverriegelung im vorherigen Zustand freigegeben worden sein". CTL-Eigenschaften schlussfolgern über verzweigte Zukünfte — „Von jedem erreichbaren Zustand aus ist es immer möglich, einen sicheren Zustand zu erreichen". Typische Verteidigungsanwendungen umfassen die Verifikation von Kommunikationsprotokoll-Zustandsmaschinen, die Prüfung, dass alle Pfade durch einen Kontrollflussgraphen eine gegebene Sicherheitsinvariante erfüllen, und die Bestätigung, dass keine Sequenz gültiger Eingaben das System in eine verbotene Konfiguration treiben kann. Model Checker wie SPIN und NuSMV geben eine Gegenbeispielverfolgung aus, wenn eine Eigenschaft verletzt wird, was CEGAR zu einem praktischen iterativen Workflow macht.

Was ist das Zustandsexplosionsproblem beim Model Checking?

Das Zustandsexplosionsproblem ist das exponentielle Wachstum des Zustandsraums, der erkundet werden muss, wenn die Anzahl der nebenläufigen Komponenten oder Datenvariablen zunimmt. Ein System mit N booleschen Variablen hat 2^N mögliche Zustände; ein System mit N nebenläufigen Threads, jeder mit K Zuständen, hat K^N kombinierte Zustände. In der Praxis können selbst kleine eingebettete Systeme Zustandsräume mit Milliarden erreichbarer Zustände erzeugen, die den verfügbaren Speicher erschöpfen, bevor die Erkundung abgeschlossen ist. Moderne Model Checker begegnen dem durch Binary Decision Diagrams (BDDs), CEGAR, partielle Ordnungsreduktion und begrenztes Model Checking mit SAT-Solvern. Für Verteidigungssoftware hält die Begrenzung des Model-Checking-Umfangs auf spezifische kritische Subsysteme den Zustandsraum handhabbar, während der Verifikationsaufwand dort konzentriert wird, wo er am wichtigsten ist.

Was sind Theorem Prover und welche werden in der Verifikation von Verteidigungssoftware eingesetzt?

Theorem Prover sind Werkzeuge, die Ingenieure beim Konstruieren maschinell geprüfter mathematischer Beweise von Softwareeigenschaften unterstützen. Im Gegensatz zu Model Checkern sind Theorem Prover nicht durch die Zustandsraumgröße begrenzt und können über unendliche Bereiche schlussfolgern — einschließlich reeller Zahlen, unbegrenzter Ganzzahlen und parametrisierter Algorithmen. Die drei Beweiser, die am häufigsten in der formalen Verifikation von Verteidigungs- und Raumfahrtsoftware anzutreffen sind, sind Coq, Isabelle/HOL und PVS. Coqs Extraktionsmechanismus kann zertifizierten ausführbaren Code direkt aus verifizierten Spezifikationen erzeugen. Isabelle/HOL hat bedeutende industrielle Verwendung gefunden, insbesondere im seL4-Microkernel-Beweis. PVS wurde speziell für die Software-Spezifikation entworfen und wurde auf NASA-Flugsoftware und Sicherheitssystemlogik für Nuklearanlagen angewendet. Alle drei erfordern erhebliche Spezialistenexpertise und signifikante Vorabinvestitionen in das Schreiben von Spezifikationen, weshalb Programme sie typischerweise für die kritischsten Algorithmen reservieren, wo keine andere Technik ausreichende Sicherheit bietet.

Was ist abstrakte Interpretation und wie verwendet Astrée sie?

Abstrakte Interpretation ist ein mathematisches Framework zur Berechnung korrekter Überapproximationen der Programmsemantik. Anstatt exakte Werte zu verfolgen, die eine Variable halten könnte, verfolgt ein abstrakter Interpreter eine Abstraktion — wie das Intervall, in dem die Variable garantiert liegt. Wenn die abstrakte Berechnung abgeschlossen wird, ohne in einem abstrakten Zustand einen Fehler zu erkennen, garantiert das Werkzeug, dass das konkrete Programm ebenfalls frei von dieser Fehlerklasse ist. Astrée wendet abstrakte Interpretation an, um die Abwesenheit von Laufzeitfehlern in C-Programmen zu beweisen — Integer-Überlauf, Division durch null, Null-Zeiger-Dereferenzierungen, Out-of-bounds-Array-Zugriffe und nicht initialisierte Lesezugriffe. Es wurde verwendet, um die primäre Flugsoftware des Airbus A380 mit null ungelösten Alarmen zu verifizieren. Für eingebettete Verteidigungssoftware werden Astrée und MathWorks Polyspace Code Prover angewendet, um zu beweisen, dass sicherheitskritische Module unter keiner Eingabe eine Laufzeitausnahme auslösen werden, und erfüllen so wichtige Anforderungen für DO-178C DAL A und MIL-STD-882-Softwaregefahrenelimination.

Wie berücksichtigt DO-178C formale Methoden?

DO-178C enthält ein Ergänzungswerk für formale Methoden — DO-333 (Formal Methods Supplement to DO-178C and DO-278A) — das definiert, wie formale Analyseaktivitäten DO-178C-Verifikationsziele erfüllen können. Unter DO-333 kann eine formale Methode Anerkennung für Strukturabdeckungsanforderungen liefern: Ein Beweis, dass eine Eigenschaft über alle erreichbaren Zustände gilt, bietet äquivalente Sicherheit zur MC/DC-Abdeckung der entsprechenden Codepfade, solange die formale Methode korrekt ist und die Eigenschaft nachweislich die Sicherheitsanforderung impliziert. Das Ergänzungswerk erfordert, dass das formale Modell die Implementierung genau darstellt, alle Annahmen explizit angegeben und gerechtfertigt sind, und die verwendeten Werkzeuge gemäß DO-330 qualifiziert sind. Formale Methoden ergänzen das Testen unter DO-178C, anstatt es zu ersetzen — der PSAC muss den Ansatz für formale Methoden bei Programmbeginn beschreiben.

Wie verbindet MIL-STD-882 formale Verifikation mit Gefahrenreduktionsgutschrift?

MIL-STD-882E definiert eine Risikomatrix basierend auf Gefahrenschwere und Eintrittswahrscheinlichkeit mit einer bevorzugten Minderungshierarchie: Gefahr eliminieren, Wahrscheinlichkeit reduzieren, Erkennung und Warnung hinzufügen, dann Restrisiko akzeptieren. Formale Verifikation trägt zu den ersten beiden Ebenen bei. Ein Model-Checking-Beweis, dass die Waffenfreigabelogik niemals ohne sowohl die Sicherheitsverriegelungsfreigabe als auch die Bedienerbestätigung in der richtigen Reihenfolge ausgelöst werden kann, stellt Gefahrenelimination für den softwarekausalen Pfad dieser Gefahr dar. Wo Elimination nicht erreichbar ist, liefert ein korrekter abstrakter Interpretationsbeweis, der die Rate softwareinduzierter Ausfälle begrenzt, Evidenz für die Wahrscheinlichkeitsreduktiongutschrift in der Gefahrenanalyse. Der Schlüsseldokumentationsschritt ist die Rückverfolgung jedes formalen Ergebnisses zu einer spezifischen Gefahrenursache in der System Hazard Analysis.

Was ist der realistische Kosten-Nutzen-Kompromiss der formalen Verifikation in einem Verteidigungsprogramm?

Formale Verifikation trägt erhebliche Vorabkosten: Aufbau formaler Modelle, Schreiben von Spezifikationen, Ausbildung von Ingenieuren und Qualifizierung von Werkzeugen für regulatorische Anerkennung. Die Vorteile sind hoch, aber ungleich verteilt: Formale Methoden liefern starken Wert für kleine, mathematisch präzise Komponenten — Planungsalgorithmen, Zustandsmaschinen, Sicherheitsverriegelungslogik — und geringen Wert für große Integrationscode, wo die Spezifikation so komplex wie die Implementierung wäre. Realistische Erwartungen: Abstrakte Interpretation fügt 5–10% Ingenieuraufwand hinzu, ausgeglichen gegen 15–30% Reduzierung der erforderlichen Testfälle; Model Checking fügt 10–20% Entwurfsphasekosten für gezielte Zustandsmaschinen hinzu, eliminiert aber eine ganze Fehlerklasse; Theorem Proving trägt die höchsten Kosten und sollte pro Komponente mit expliziter Rechtfertigung bewertet werden. Programme, die formale Methoden selektiv auf die richtigen Komponenten anwenden, erholen ihre Investition; Programme, die sie wahllos anwenden, überschreiten Zeitplan und Budget.

Welche Werkzeugqualifizierung ist erforderlich, wenn formale Analysewerkzeuge für DO-178C-Anerkennung verwendet werden?

DO-178C §12.2 schreibt vor, dass Software-Werkzeuge qualifiziert werden müssen, wenn ihre Ausgabe ohne unabhängige Verifikation verwendet wird. DO-330 definiert Werkzeugqualifizierungsniveaus (TQL-1 bis TQL-5) basierend auf der Rolle des Werkzeugs und dem Entwicklungssicherheitsniveau. Ein formales Analysewerkzeug, das zur Erfüllung eines DO-178C DAL A-Verifikationsziels verwendet wird, fällt auf TQL-1 oder TQL-2 und erfordert die strengsten Qualifizierungsartefakte: Werkzeugbetriebsanforderungen, Werkzeugqualifizierungsplan, Werkzeugerfüllungszusammenfassung und Evidenz korrekter Ergebnisse für den relevanten Anwendungsfall. Kommerzielle Werkzeuge wie Astrée und Polyspace liefern vorhandene Qualifizierungskits, die den Programmaufwand auf den Nachweis reduzieren, dass das Kit auf den spezifischen Verwendungskontext und die Compilerkonfiguration anwendbar ist. Open-Source-Werkzeuge erfordern typischerweise vollständige Qualifizierung von Grund auf — ein erheblicher Programmaufwand, der von Anfang an im Projektplan berücksichtigt werden muss.

Welche Team-Skills sind erforderlich, um formale Verifikation in ein Verteidigungssoftware-Team einzuführen?

Abstrakte Interpretationswerkzeuge wie Astrée und Polyspace sind der Einstiegspunkt mit der niedrigsten Einstiegshürde und können von Ingenieuren mit C/C++-Hintergrund nach einigen Tagen Training bedient werden — die primäre Fähigkeit ist Alarm-Triage: echte Fehler von falsch positiven Ergebnissen aufgrund von Abstraktionsungenauigkeit zu unterscheiden. Model Checking mit SPIN oder NuSMV erfordert Ingenieure, die Spezifikationen in Promela oder SMV schreiben und Eigenschaften in LTL/CTL ausdrücken können — eine Fähigkeit, die Wochen bis Monate zur Entwicklung braucht und in Standardlehrplänen nicht gelehrt wird. Theorem Proving mit Coq, Isabelle/HOL oder PVS erfordert tiefe Expertise in formaler Logik und Beweistheorie — Fähigkeiten, für die die meisten Programme eher einstellen oder von Spezialisierungsorganisationen beauftragen müssen. Der praktischste Personalbesetzungspfad ist, zuerst abstrakte Interpretation einzuführen, Ingenieure speziell für Model Checking zur Zustandsmaschinen-Verifikation zu schulen, und Theorem Proving für beauftragte Spezialarbeit an den höchstkritischen Komponenten zu reservieren.