Kani: Rust için model checker doğrulama aracı

Kani, Rust kodları için açık kaynaklı bir sınırlı model checker aracıdır ve klasik derleyici garantilerinin ötesine geçerek unsafe işlemlerin (örneğin ham pointer dereferansları) doğruluğunu, fonksiyonel korrektliği ve runtime panic'lerin yokluğunu kanıtlamayı hedefler. Araç, Rust'ın Mid-level Intermediate Representation (MIR) çıktısından proof harness'ları derleyip bunları CBMC'nin bit-precise doğrulama motoruna aktararak kullanıcı ek açıklaması gerektirmeden kapsamlı bir güvenlik özellikleri seti üzerinde otomatik kontrol yapar.

Sınırlı model checking'i sınırsız doğrulamaya taşımak için Kani; fonksiyon kontratları, döngü kontratları, kuantörler ve fonksiyon stub'lama içeren bir spesifikasyon dili sunuyor. Endüstriyel Rust projeleri üzerinde yapılan vaka çalışmalarında bu kontratlar, doğrulama seviyesini panic-freedom'dan fonksiyonel doğruluğa yükseltmiş ve daha önce bilinmeyen altı hatayı ortaya çıkarmıştır.

Kani, üretim CI ortamlarında ölçeklenebilir şekilde çalışıyor; Rust standart kütüphanesi doğrulama kampanyasında her kod değişikliğinde 16.000'den fazla harness doğrulanıyor. Bu, statik doğrulama araçlarının gerçek dünya, büyük ölçekli sistem yazılımlarına entegre edilebileceğini gösteren somut bir örnek teşkil ediyor ve Rust ekosisteminde güvenlik garantilerini derleyici seviyesinin ötesine taşıyor.