Kani: Ein Modellprüfer für Rust, der über Bug-Finding hinausgeht

Kani: A Model Checker for Rust

Kani ist ein Open-Source-Modellprüfer für Rust, der über die Grenzen der Typprüfung hinausgeht und Korrektheitsgarantien für Eigenschaften wie die Sicherheit von unsafe-Operationen, funktionale Korrektheit und die Abwesenheit von Laufzeit-Panics bietet. Er kompiliert Proof-Harnesses aus Rusts Mid-level Intermediate Representation (MIR) in die bit-präzise Verifikations-Engine von CBMC und prüft automatisch eine umfassende Menge von Sicherheitseigenschaften ohne Benutzerannotationen. Eine Spezifikationssprache mit Funktionsverträgen, Schleifenverträgen, Quantoren und Funktions-Stubbing erweitert die Verifikation von beschränkt auf unbeschränkt. In Fallstudien mit industriellen Rust-Projekten deckte Kani sechs bisher unbekannte Bugs auf und hob die Verifikation von Panik-Freiheit auf funktionale Korrektheit. In der Produktion wird Kani in der CI eingesetzt, wo über 16.000 Harnesses pro Codeänderung in der Rust-Standardbibliothek verifiziert werden.