Rust-Verifikation: Vom Borrow Checker zum Beweis

Der Borrow Checker ist Rusts bekannteste Sicherheitsgarantie — aber er ist nur der Anfang. Er verhindert Speicherfehler in sicherem Code, aber er beweist nicht, dass ein Programm funktional korrekt ist. Er prüft nicht, ob eine unsafe-Funktion ihre Verträge einhält. Er garantiert nicht, dass ein Algorithmus das richtige Ergebnis liefert. Die aktuelle Forschung geht daher einen Schritt weiter: formale Verifikation für Rust.

Kani: Ein Model Checker für Rust

Kani (2026) ist ein Open-Source-Model-Checker für Rust, der über das Bug-Finding hinausgeht und Korrektheitsgarantien liefert. Kani kompiliert Proof-Harnesses aus Rusts Mid-level Intermediate Representation (MIR) und nutzt bounded model checking, um Eigenschaften wie:

• Soundness von unsafe-Operationen (z. B. Raw-Pointer-Dereferenzierungen)
• Funktionale Korrektheit (liefert die Funktion das erwartete Ergebnis?)
• Abwesenheit von Runtime-Panics (kein unerwartetes panic!)

zu beweisen.

// Ein Kani-Proof-Harness
#[kani::proof]
fn verify_vec_push() {
    let mut v = vec![1, 2, 3];
    let old_len = v.len();
    v.push(42);
    // Kani beweist: die Länge erhöht sich um genau 1
    assert!(v.len() == old_len + 1);
    // Kani beweist: das letzte Element ist 42
    assert!(v[old_len] == 42);
}

Der Unterschied zum Borrow Checker: Kani prüft nicht Speichersicherheit, sondern funktionale Korrektheit. Der Borrow Checker sagt "das kompiliert ohne Speicherfehler". Kani sagt "das Programm tut, was es soll".

RustyDL: Ein Programmlogik für Rust

RustyDL (2026) ist eine Programmlogik für Rust — die Grundlage für ein deduktives Verifikationswerkzeug. Im Gegensatz zu anderen Tools, die Rust- Code in eine Zwischensprache übersetzen, arbeitet RustyDL direkt auf Quellcode-Ebene. Das ist entscheidend für eine Human-in-the-Loop- Verifikation: der Entwickler kann den Beweis auf derselben Ebene führen, auf der er den Code schreibt.

RustyDL reasoning über Rusts Ownership-Modell: es versteht Moves, Borrows, Lifetimes und Unsafe-Blöcke und erlaubt es, Eigenschaften über diese Konstrukte formal zu beweisen.

// RustyDL kann beweisen: diese Funktion verletzt keine Ownership-Regel
fn first_word(s: &str) -> &str {
    let bytes = s.as_bytes();
    for (i, &byte) in bytes.iter().enumerate() {
        if byte == b' ' {
            return &s[0..i];
        }
    }
    &s[..]
}
// RustyDL: der zurückgegebene Slice lebt genauso lang wie s.
// Kein Use-after-Free, kein Dangling Pointer — bewiesen, nicht nur geprüft.

Die größte Verifikationskampagne: Die Rust-Standardbibliothek

Verifying the Rust Standard Library (2026) ist, nach bestem Wissen der Autoren, die größte Verifikationskampagne, die bisher für eine Softwarebibliothek durchgeführt wurde. Die Rust-Standardbibliothek nutzt intensiv unsafe-Code — intern für Vec, String, HashMap und viele andere Typen. Die Korrektheit dieses unsafe-Codes wurde bisher durch Tests validiert, einschließlich dynamischer Prüfungen unter Miri, aber nicht durch statische Verifikation.

Die Studie ist ein offener, Crowdsourced-Ansatz, der komplementäre Verifikations-Tools in die Continuous Integration eines Verification-Repository integriert — ein Fork der Standardbibliothek, in dem Beweise kontinuierlich ausgeführt werden.

Die Implikation ist tiefgreifend: wenn die Standardbibliothek formal verifiziert ist, dann ist die Vertrauenskette vom Borrow Checker über die Standardbibliothek bis zum Anwendungscode lückenlos.

Unsafe Rust und Pointer-Aliasing

Towards verifying unsafe Rust programs against Rust's pointer-aliasing restrictions (2026) adressiert ein subtileres Problem: Rusts Pointer-Aliasing-Regeln. Der Compiler nutzt diese Regeln, um effizienteren Maschinencode zu generieren. Aber innerhalb von unsafe-Blöcken werden sie nicht vom Typsystem erzwungen — und ihre Verletzung führt zu Undefined Behavior, das schwer zu finden ist.

Diese Arbeit ist ein Schritt dahin, solche Verletzungen statisch zu beweisen — nicht nur zur Laufzeit zu finden.

// Pointer-Aliasing: in safe Rust vom Borrow Checker erzwungen
fn safe_example(s: &str) {
    let bytes = s.as_bytes();
    // bytes ist ein &[[u8]], lebt so lange wie s
    // Kein Aliasing möglich — der Borrow Checker verbietet es
}

// In unsafe: der Programmierer ist verantwortlich
unsafe fn unsafe_example(ptr: *mut u8) {
    *ptr = 42;
    // Hat jemand anderes einen Alias auf *ptr?
    // Der Borrow Checker kann es nicht prüfen. Verifikation kann es.
}

Was das für die Praxis bedeutet

Die Verifikationslandschaft für Rust reift schnell. In 2026 haben wir:

Tool	Ansatz	Beweist
Borrow Checker	Compile-Zeit	Speichersicherheit (safe code)
Miri	Laufzeit	UB-Erkennung (unsafe code)
Kani	Model Checking	Funktionale Korrektheit, Panic-Freiheit
RustyDL	Deduktiv	Source-Level-Eigenschaften
Verifying std	Crowdsourced	Korrektheit der Standardbibliothek

Für sicherheitskritischen Code (Kryptographie, Betriebssysteme, Embedded) ist das ein gamechanger: man kann nicht nur glauben, dass der Code sicher ist — man kann es beweisen.

Ins Thema einsteigen

• Modul 20: Unsafe Rust — unsafe-Code verstehen und sicher einsetzen
• Modul 9: Lifetimes — Lifetimes als Grundlage des Borrow Checkers
• Modul 15: Testing — Testen und Verifikation

Weiterführende Artikel:

• Rusts Sicherheitsmodell ist keine Meinung — es ist bewiesen — Wie neuro-symbolische Verifikation Rust-Code beweist
• KI schreibt Code — aber ist er richtig? — Was die Forschung über KI-generierten Code lehrt