Statische Analyse kann nicht beweisen, dass Ihr Flugzeug nicht abstürzt. Sie kann etwas Nützlicheres beweisen.

Die Antwort lautet Nein. Die eigentliche Frage ist, was sie stattdessen beweisen kann.

Statische Analyse kann nicht beweisen, dass ein Flugzeug nicht abstürzt. Sie kann beweisen, dass die Regelschleife Ihres Höhenmessers niemals durch Null teilt, niemals außerhalb der Grenzen indiziert und niemals einen Festkomma-Akkumulator überläuft. Der Unterschied ist wichtig, denn die eine Aussage betrifft Physik, Aerodynamik und Aluminium unter Belastung, die andere eine Aussage über Code, die Sie verifizieren können, bevor das Flugzeug den Boden verlässt.

Das ist das Versprechen der abstrakten Interpretation. Nicht Allwissenheit. Sondern ein rigoroser Beweis, dass bestimmte Kategorien katastrophaler Softwarefehler in jeder möglichen Ausführung unmöglich sind.

Warum das Testen einer Million Szenarien Sie dennoch im Ungewissen lässt

Ein typisches Flugsteuerungssystem umfasst Hunderttausende Zeilen C. Der Eingaberaum ist das Kreuzprodukt aus Sensorwerten, Pilotenbefehlen, Umgebungsbedingungen und internen Zustandsvariablen. Sie könnten das System in einem Simulator bis zum Wärmetod des Universums laufen lassen und immer noch nicht jeden Pfad abdecken.

Tests finden Fehler. Sie beweisen jedoch nicht deren Abwesenheit. Jeder bestandene Test ist ein Datenpunkt. Er ist keine Garantie.

Die abstrakte Interpretation kehrt den Ansatz um. Statt das Programm mit konkreten Eingaben auszuführen, führt sie es auf abstrakten Domänen aus, die Mengen möglicher Werte repräsentieren. Wenn die abstrakte Analyse sagt, dass ein bestimmter Fehlerzustand unerreichbar ist, dann ist dieser Fehler für jede konkrete Eingabe unerreichbar. Der Beweis ist erschöpfend, weil er den gesamten Eingaberaum in einem einzigen Durchlauf abdeckt.

Konkrete Werte sind zu teuer. Verwenden Sie stattdessen Formen.

Betrachten Sie eine einfache Variable x. In einer konkreten Ausführung könnte x den Wert 42 haben. In einer abstrakten Interpretation könnte x „jede ganze Zahl zwischen 0 und 255“ sein. Das nennt man eine Intervallabstraktion.

Der Analyzer verfolgt diese Intervalle durch jede Operation. Wenn x [0, 100] und y [1, 10] ist, dann ist x / y gleich [0, 100]. Der Analyzer weiß, dass die Division sicher ist, weil das Divisorintervall Null nicht enthält.

Wäre y jedoch [-5, 5], würde der Analyzer eine potenzielle Division durch Null melden. Er weiß nicht, ob die konkrete Ausführung auf Null trifft. Er weiß, dass Null innerhalb des möglichen Bereichs liegt. Das reicht aus, um einen Alarm auszulösen.

Die zentrale Erkenntnis, die auf Patrick und Radhia Cousot im Jahr 1976 zurückgeht, ist, dass die abstrakte Domäne eine korrekte Überapproximation der konkreten Semantik sein muss. Jedes konkrete Verhalten muss in der Abstraktion darstellbar sein. Wenn die Abstraktion sicher ist, ist das konkrete Programm sicher. Wenn die Abstraktion warnt, könnte das konkrete Programm in Ordnung sein. Aber es könnte auch nicht.

Bauen Sie einen einfachen Intervall-Analysator in Python

Hier ist eine funktionierende Intervall-Abstraktionsdomäne. Sie ist naiv, zeigt aber die Mechanik.

from dataclasses import dataclass
from typing import Optional

@dataclass(frozen=True)
class Interval:
    lo: int
    hi: int

    def __post_init__(self):
        if self.lo > self.hi:
            raise ValueError("Empty interval")

    def add(self, other: "Interval") -> "Interval":
        return Interval(self.lo + other.lo, self.hi + other.hi)

    def div(self, other: "Interval") -> Optional["Interval"]:
        if other.lo <= 0 <= other.hi:
            return None  # Potential division by zero
        # Simplified: assumes positive divisor for demo
        return Interval(self.lo // other.hi, self.hi // other.lo)

    def intersect(self, other: "Interval") -> Optional["Interval"]:
        lo = max(self.lo, other.lo)
        hi = min(self.hi, other.hi)
        if lo > hi:
            return None
        return Interval(lo, hi)

    def __repr__(self):
        return f"[{self.lo}, {self.hi}]"


def analyze_division(a: Interval, b: Interval) -> None:
    result = a.div(b)
    if result is None:
        print(f"ALERT: {a} / {b} may divide by zero")
    else:
        print(f"SAFE: {a} / {b} = {result}")

Ein paar Fälle ausführen:

analyze_division(Interval(10, 20), Interval(2, 5))   # SAFE
analyze_division(Interval(10, 20), Interval(-1, 1))  # ALERT
analyze_division(Interval(10, 20), Interval(0, 5))   # ALERT

Der erste Fall ist sicher, weil jeder Divisor positiv ist. Der zweite wird gemeldet, weil Null innerhalb von [-1, 1] liegt. Der dritte wird gemeldet, weil Null innerhalb von [0, 5] liegt.

Beachten Sie, was im dritten Fall passiert ist. Das konkrete Programm könnte b = 0 niemals tatsächlich ausführen. Das weiß der Analyzer nicht. Er ist von Natur aus konservativ. Das ist der fundamentale Kompromiss.

Die Steuer für falsch-positive Meldungen

Ein korrekter statischer Analyzer übersieht niemals einen Fehler. Wenn ein Absturz möglich ist, meldet er ihn. Aber er meldet auch Abstürze, die unmöglich sind. Diese falsch-positiven Meldungen sind der Preis der Korrektheit.

In der Praxis ist dieser Preis hoch. Eine naive Intervallanalyse einer Schleife wie for (i = 0; i < n; i++) wird oft zu dem Schluss kommen, dass i [0, +∞] ist, auch wenn n begrenzt ist. Der Analyzer verliert an Präzision an Zusammenführungspunkten, an denen sich zwei Kontrollflusspfade treffen und ihre abstrakten Zustände kombiniert werden müssen.

Echte Werkzeuge verwenden ausgefeiltere Domänen. Polyeder, Oktagonen und Prädikatenabstraktionen verfolgen Beziehungen zwischen Variablen. x < y ist für Intervalle unsichtbar, aber eine polyedrische Domäne behält es im Gedächtnis. Diese Domänen sind präziser. Sie sind auch teurer. Die polyedrische Domäne hat im schlimmsten Fall exponentielle Komplexität. Für ein Flugsteuerungssystem mit 300.000 Zeilen C würde eine naive Implementierung nicht vor der Ausmusterung des Flugzeugs terminieren.

Was Astrée tatsächlich beim A380 bewiesen hat

Astrée ist der statische Analyzer, der die abstrakte Interpretation in der Luftfahrt berühmt gemacht hat. Im Jahr 2003 wurde Astrée gegen die primäre Flugsteuerungssoftware des Airbus A380 ausgeführt. Er bewies die Abwesenheit jeglicher Laufzeitfehler. Keine Division durch Null. Kein Zugriff außerhalb der Array-Grenzen. Kein arithmetischer Überlauf. Kein unerreichbarer Code in kritischen Pfaden.

Er bewies nicht, dass das Flugzeug nicht abstürzt. Er bewies nicht, dass die Regelgesetze korrekt sind. Er bewies nicht, dass die Anstellwinkelberechnung mit der Physik des Flugzeugs übereinstimmt. Das sind andere Probleme, die mit anderen Werkzeugen gelöst werden.

Astrée bewies, dass die Software sich nicht selbst zerstören würde. Das ist eine engere Aussage, als sie klingt, und eine wertvollere, als die meisten Menschen realisieren. Die Selbstzerstörung von Software ist eine häufige Ursache von Flugzeugunfällen. Den Beweis, dass sie nicht passieren kann, ist den Aufwand wert.

Das Werkzeug erreichte dies, indem es mehrere domänenspezifische Tricks kombinierte. Es verwendet eine nicht-relationale Domäne für Geschwindigkeit und eine relationale Domäne für Präzision. Es behandelt Gleitkommaarithmetik mit einem Modell, das Rundungsfehler berücksichtigt. Es versteht die spezifische C-Teilmenge, die in der Avionik verwendet wird, und behandelt undefiniertes Verhalten als Fehler. Es dauerte Jahre der Feinabstimmung, um die Rate falsch-positiver Meldungen so niedrig zu bekommen, dass Ingenieure der Ausgabe vertrauen würden.

Korrektheit ist eine Wahl, keine Voreinstellung

Nicht jeder statische Analyzer zielt auf Korrektheit ab. Werkzeuge wie Coverity, CodeQL und Infer priorisieren das Finden echter Fehler gegenüber dem Beweis der Abwesenheit. Sie unterapproximieren den Zustandsraum. Sie könnten eine Division durch Null übersehen, aber die, die sie finden, sind in der Regel real.

Das ist eine legitime ingenieurtechnische Entscheidung. Für eine Webanwendung schlägt ein zu 90 % genauer Fehlerfinder, der in Minuten läuft, einen korrekten Analyzer, der Sie mit falsch-positiven Meldungen überschwemmt. Für ein Flugsteuerungssystem gilt das Gegenteil. Sie wollen den Beweis, auch wenn Sie Rauschen herausfiltern müssen.

Die abstrakte Interpretation ist die Technologie, die den Beweis möglich macht. Sie ist nicht die einzige formale Methode. Modelchecker wie SPIN und TLA+ verifizieren Zustandsautomaten. Theorembeweiser wie Coq und Isabelle verifizieren funktionale Korrektheit. Die abstrakte Interpretation besetzt einen Sweet Spot: Sie ist vollständig automatisch, sie skaliert auf große codebases, und sie liefert mathematische Garantien über das Laufzeitverhalten.

Wo die abstrakte Interpretation an ihre Grenzen stößt

Die Methode hat harte Grenzen. Sie kann nicht über Speicher schlussfolgern, der durch komplexe Zeigerarithmetik alloziert wurde. Sie kann nicht verifizieren, dass Ihr Algorithmus den richtigen Wert berechnet, nur dass er nicht abstürzt, während er ihn berechnet. Sie hat Schwierigkeiten mit Nebenläufigkeit, dynamischem Dispatch und Code, der von Natur aus auf undefiniertem Verhalten beruht.

Sie erfordert außerdem, dass der Code in einem verifizierbaren Stil geschrieben ist. Die A380-Flugsoftware vermeidet Rekursion, begrenzt die dynamische Speicherallokation und hält den Kontrollfluss einfach. Diese Einschränkungen sind keine Grenzen des Analyzers. Sie sind Voraussetzungen für den Beweis. Sie können keine Eigenschaften von Code beweisen, der zu chaotisch ist, um ihn zu modellieren.

Beginnen Sie mit Intervallen an einer echten Funktion

Sie brauchen Astrée nicht, um diese Ideen anzuwenden. Wählen Sie eine einzelne reine Funktion in Ihrer Codebasis. Identifizieren Sie eine Variable, die innerhalb von Grenzen bleiben muss. Schreiben Sie ein einfaches Intervallpropagationsskript. Verfolgen Sie die Variable durch jeden Zweig und jede Operation.

Wenn das Intervall am Verwendungsort innerhalb des sicheren Bereichs liegt, haben Sie einen manuellen Sicherheitsbeweis für diese Variable. Wenn nicht, haben Sie entweder einen Fehler identifiziert oder eine Stelle, an der Ihre Schlussfolgerung unvollständig war. Auf jeden Fall haben Sie etwas gelernt, das ein Unit-Test möglicherweise nicht entdeckt hätte.

Die abstrakte Interpretation wird nicht beweisen, dass Ihr Flugzeug nicht abstürzt. Nichts kann das. Aber sie kann beweisen, dass Ihre Software nicht der Grund dafür sein wird.

FAQ

Was ist abstrakte Interpretation?

Abstrakte Interpretation ist eine formale Methode zur statischen Programmanalyse, bei der konkrete Programmwerte durch abstrakte Darstellungen wie Intervalle oder Formen ersetzt werden. Der Analyzer simuliert die Programmausführung auf diesen abstrakten Werten. Wenn ein Fehler in der abstrakten Domäne unerreichbar ist, ist er im konkreten Programm für alle möglichen Eingaben unerreichbar.

Kann abstrakte Interpretation alle Fehler finden?

Nein. Abstrakte Interpretation beweist die Abwesenheit spezifischer Laufzeitfehler wie Division durch Null, Pufferüberläufe und arithmetische Überläufe. Sie kann nicht verifizieren, dass ein Algorithmus das korrekte Ergebnis liefert, nur dass er nicht abstürzt. Sie kann auch nicht über Eigenschaften außerhalb des Codes schlussfolgern, wie Hardwarefehler oder das Verhalten physikalischer Systeme.

Was ist der Unterschied zwischen korrekter und nicht-korrekter statischer Analyse?

Ein korrekter Analyzer überapproximiert die Menge möglicher Programmverhalten. Er wird niemals einen Fehler der Art übersehen, für die er konzipiert ist, aber er kann falsch-positive Meldungen erzeugen. Ein nicht-korrekter Analyzer unterapproximiert. Er kann Fehler übersehen, aber die, die er meldet, sind mit höherer Wahrscheinlichkeit real. Korrektheit ist für sicherheitskritische Systeme unverzichtbar. Nicht-korrekte Analyse wird oft für schnelleres Feedback in der allgemeinen Softwareentwicklung bevorzugt.

Ist abstrakte Interpretation nur für sicherheitskritische Software?

Nein, auch wenn sie dort am intensivsten eingesetzt wird. Die Ideen hinter der abstrakten Interpretation tauchen in vielen Compilern und Optimierern auf. Die Bereichsanalyse von LLVM zum Beispiel verwendet Intervallabstraktionen, um redundante Grenzprüfungen zu eliminieren. Sie können dieselbe Intervallschlussfolgerung auf jeden Code anwenden, bei dem der Beweis von Grenzen wichtig ist, von eingebetteter Firmware bis hin zu numerischen Hochleistungskernels.