Begriff
Frama-C
Warum wichtig?
Dieser Begriff ist ein Knoten im SengakujiWorks-Wissensnetz. Nutze Level 0 für die erste Einordnung, Level 1 für Praxis, Level 2 für technische Struktur und Level 3 für Grenzen, Fallstricke und Expertenkontext.
C ist die gefährlichste Sprache der Welt (Pointer, Buffer Overflows). Aber sie steuert unsere Welt (Linux Kernel, Airbag, Herzschrittmacher). Wir können C nicht abschaffen. Also müssen wir es sicher machen. Frama-C ist ein Analyse-Framework für C-Code. Es kann beweisen, dass in deinem C-Code niemals ein "Undefined Behavior" (z. B. Division durch Null, Array Access out of bounds) passiert. Es nutzt "ACSL" (eine Sprache für Kommentare), um Verträge zu definieren.
Merksatz: Eine Plattform zur statischen Analyse von C-Code, die verschiedene Techniken (Value Analysis, Proofs) kombiniert, um die Abwesenheit von Laufzeitfehlern mathematisch zu garantieren.
Du annotierst C-Code in Kommentaren:
/*@ requires n > 0; ensures \result == n * n; */
int square(int n) { ... }
Modul Eva (Evolved Value Analysis): Prüft vollautomatisch Wertebereiche. "Variable x ist hier immer zwischen -5 und 100".
Modul WP (Weakest Precondition): Beweist logische Eigenschaften (Hoare Logic).
1. Abstract Interpretation
Wie prüft Eva Millionen Codezeilen?
Es führt den Code nicht aus. Es rechnet mit "abstrakten Werten" (Intervallen).
Statt x = 5, rechnet es x = [0..10].
y = x + 2. -> y = [2..12].
Wenn array[y] Größe 10 hat, sagt Eva: "Alarm! y könnte 11 oder 12 sein. Index Out Of Bounds möglich!".
2. Soundness
Der wichtigste Begriff. Frama-C ist sound. Wenn Frama-C sagt "Code ist sicher", dann IST er sicher. (Keine False Negatives). Andere Tools (Lint, SonarQube) raten nur. Frama-C beweist.
1. Weakest Precondition (WP-Plugin)
Während das Eva-Modul über Wertebereiche "nachdenkt", nutzt das WP-Plugin die Hoare-Logik.
Es berechnet die "Weakest Precondition" (schwächste Vorbedingung).
Beispiel: Dein Code sagt x = y + 1; assert x > 5;.
WP rechnet rückwärts: Damit x > 5 gilt, muss nach der Zuweisung y + 1 > 5 (also y > 4) gelten.
Wenn dein Programm im Kommentar aber nur verspricht requires y > 0;, sagt WP: "Beweis fehlgeschlagen!". Dieser rückwärtsgerichtete Beweis ist der Goldstandard für die Verifikation von sicherheitskritischen Algorithmen.
2. Pointer-Modelle & Speicher-Trennung
Das größte Problem bei C ist der Speicher. Zeigen zwei Pointer p und q auf die gleiche Stelle (Aliasing)?
Frama-C nutzt verschiedene Memory Models (z. B. Typed oder Briand).
In ACSL kannst du angeben: /*@ requires \separated(p, q); */.
Das ist wie ein Vertrag: "Ich garantiere dem Compiler, dass diese zwei Pointer sich niemals in die Quere kommen." Frama-C nutzt diese Information, um den Code viel präziser zu beweisen, als es ein Standard-Compiler jemals könnte.
3. Kooperative Analyse (The Meta-Framework)
Frama-C ist nicht nur ein Tool, sondern ein "Orchester".
Ein Modul (Eva) findet heraus, welche Werte Variablen haben. Ein anderes Modul (Frama-Clang) erlaubt die Analyse von C++. Ein drittes Modul (RTE) fügt automatisch Assertions für alle potenziellen Fehlerstellen ein.
Der Clou: Die Plugins teilen sich eine zentrale Datenbank (den AST). Ein Beweis, den das WP-Plugin nicht schafft, kann vielleicht durch Informationen aus der Value-Analysis von Eva vervollständigt werden. Diese Synergie zwischen verschiedenen mathematischen Ansätzen macht Frama-C zu einem der mächtigsten Tools der Welt.
Quick-Check
Wer nutzt es?
Airbus, Atomkraftwerke. Überall, wo ein Bug Menschen töten kann.Warum nicht für Webseiten?
Zu viel Aufwand. Und Webseiten sind meist nicht in C.ACSL?
ANSI/ISO C Specification Language. Ein Standard für formale Kommentare in C.