Die Arbeit präsentiert C*, eine beweisintegrierte Sprache für C, die Programmentwicklung und formale Verifikation in einer gemeinsamen Umgebung vereint. Angetrieben durch eine symbolische Ausführungs-Engine und einen LCF-artigen Beweiskern ermöglicht C* die Einbettung von Beweiscode direkt neben dem Implementierungscode für interaktive Echtzeit-Verifikationen. Entwickler nutzen C als einheitliche Sprache zur Erstellung wiederverwendbarer logischer Bibliotheken, Theoreme und programmierbarer Beweisautomatisierung. Die Evaluierung anhand kleinerer C-Benchmarks sowie der komplexen attach-Funktion des pKVM-Buddy-Allocators zeigt, dass C* gängige C-Programmiermuster und anspruchsvolle Verifikationsaufgaben in realen Szenarien effektiv unterstützt.
Wichtigste Punkte
Vereinheitlichter Sprachansatz: C* eliminiert die Hürde getrennter Paradigmen zwischen Programmierung und Verifikation, indem C als gemeinsame Sprache für Quellcode und logische Beweise dient.
Beweisarchitektur: Das System kombiniert eine symbolische Ausführungs-Engine (Symbolic Execution Engine) mit einem LCF-artigen Beweiskern (LCF-style Proof Kernel), um formal korrekte Beweise zu garantieren.
Echtzeit-Verifikation: Programmierer können Beweisblöcke direkt in den C-Code einbetten, was eine unmittelbare, interaktive Rückmeldung und Aktualisierung des Beweiszustands während der Entwicklung erlaubt.
Erweiterbare Beweisbibliothek: C* bietet Werkzeuge zur Definition wiederverwendbarer mathematischer Begriffe, Theoreme und benutzerdefinierter Beweisautomatisierung.
Evaluierung an Kernel-Komponenten: Die Praxistauglichkeit wurde erfolgreich an kleinen C-Programmen sowie an einer kritischen Systemkomponente demonstriert: der attach-Funktion des Buddy-Allocators aus pKVM (Protected Kernel-based Virtual Machine).
Diskussions-Highlights
Namenskonflikte und Historie: Mehrere Kommentatoren wiesen darauf hin, dass der Name „C*“ historisch bereits mehrfach belegt ist – unter anderem durch eine parallele C-Variante von Thinking Machines aus den 1990er-Jahren sowie eine bekannte Abhandlung über das Ausnutzen von undefiniertem Verhalten (Undefined Behavior) in C-Compilern.
Syntax und Ergonomie: Die Syntax von C* stieß auf Kritik. Die Nutzung von C++20-ähnlichen Attributen ([[require/ensure/invariant/proof]]) und Backticks für logische Zusicherungen wurde teilweise als unübersichtlich („Frankengrammar“) empfunden, während Befürworter die Abstimmung auf moderne C/C++-Standards verteidigten.
Formale Verifikation vs. Laufzeitanalyse: Es wurde diskutiert, dass Werkzeuge wie Valgrind und spezifische Compiler-Flags (GCC/LLVM) zwar Speicherfehler finden, aber keine funktionale Korrektheit beweisen können. Formale Verifikation erfordert zwar ein tieferes mathematisches Verständnis, bietet jedoch Garantien („Correct by Construction“), die reine Testläufe nicht liefern können.
KI- und LLM-Integration: Entwickler hoben hervor, dass C* Schnittstellen und Tutorials für das Model Context Protocol (MCP) bereitstellt. Dies ermöglicht es Sprachmodellen (LLMs), interaktiv beim Schreiben und Überprüfen von Verifikationsbeweisen zu helfen.
Vergleich zu bestehenden Werkzeugen: C* wurde mit der etablierten verifikationsorientierten Sprache F* verglichen, wobei betont wurde, dass F* der ML-Sprachfamilie angehört, während C* direkt auf der C-Syntax aufbaut.
Theoretische Fundamente: In den Beiträgen wurde auf Edsger Dijkstras Ansatz der Programmentwicklung („Correctness-by-Construction“), seine Guarded Command Language (GCL), den wp-calculus (weakest precondition) sowie Carroll Morgans Refinement Calculus verwiesen.
Verhältnis von C zu C++: Eine Seitendebatte entstand über die Beziehung zwischen C und C++. Während einige betonten, dass viele C-Entwickler C++ ablehnen (z. B. im Linux-Kernel-Umfeld), verteidigten andere C++ als mächtige Sprache für Abstraktionen mit Zero-Cost-Overhead.
Glossar
LCF-style Proof Kernel (LCF-Beweiskern): Eine Architektur für Theorembeweiser (benannt nach Logic for Computable Functions), bei der logische Beweise nur durch einen kleinen, strikt überprüften Satz von Kernregeln erzeugt werden können, um Fehlschlüsse zu vermeiden.
Symbolic Execution (Symbolische Ausführung): Eine Programmanalysemethode, die ein Programm mit symbolischen Variablen anstelle konkreter Eingabewerte evaluiert, um mathematische Bedingungen über alle möglichen Ausführungspfade zu berechnen.
pKVM (Protected Kernel-based Virtual Machine): Eine sicherheitsgehärtete Version der Linux-KVM-Virtualisierungstechnologie, die streng geschützte Speicherbereiche für Hypervisor und Gast-VMs garantiert.
Buddy Allocator: Ein klassischer Speicherverwaltungs-Algorithmus, der den Arbeitsspeicher kontinuierlich in halbierte Blöcke („Buddies“) aufteilt und wieder zusammenfügt, um Speicherfragmentierung zu verhindern.
Design by Contract (Entwurf durch Kontrakte): Ein Entwurfsmuster für Software, bei dem Funktionen durch explizite Vorbedingungen (requirements), Nachbedingungen (ensures) und Invarianten mathematisch spezifiziert werden.
Valgrind: Ein Programmierwerkzeug zur dynamischen Ausführungsanalyse, das primär zur Erkennung von Speicherlecks und unzulässigen Speicherzugriffen in C/C++-Programmen verwendet wird.
wp-calculus (Weakest Precondition Calculus): Ein von Edsger Dijkstra entwickeltes mechnisches Verfahren zur Berechnung der schwächsten Vorbedingung, unter der ein Programm garantiert korrekt terminiert und ein gewünschtes Resultat liefert.
Refinement Calculus (Verfeinerungskalkül): Ein mathematisches System zur schrittweisen, beweisbar korrekten Transformation einer abstrakten Spezifikation in ausführbaren Quellcode.
F:* Eine funktionale, verifikationsorientierte Programmiersprache aus der ML-Familie, die ein abhängiges Typensystem für formale Softwarebeweise nutzt.
Model Context Protocol (MCP): Ein offener Schnittstellenstandard, der es Künstlicher Intelligenz (z. B. LLMs) ermöglicht, strukturiert mit Entwicklungsumgebungen und Werkzeugen zu interagieren.