Introduzione a Kani

Kani è uno strumento di verifica formale per il linguaggio di programmazione Rust che sfrutta la rappresentazione intermedia MIR (Mid-level Intermediate Representation) per analizzare e garantire proprietà specifiche del codice. Kani può essere installato seguendo la documentazione ufficiale.

Kani permette di specificare proprietà formali del codice, come invarianti, pre-condizioni e post-condizioni. Utilizzando tecniche di model checking, questo strumento esplora tutte le possibili esecuzioni del programma per garantire che queste proprietà siano rispettate. Grazie a questo tipo di verifica possiamo assicurarci che il software si comporti correttamente in tutte le possibili circostanze.

Uno degli obiettivi principali di Kani è migliorare la sicurezza del codice Rust. Come già detto, l'analisi statica può identificare vulnerabilità di sicurezza, come buffer overflow, accessi non sicuri alla memoria e race condition. Questo è particolarmente utile per il codice unsafe, dove le garanzie di sicurezza del compilatore Rust sono disabilitate.

Kani, inoltre, è progettato per integrarsi facilmente con il flusso di lavoro di sviluppo Rust. Infatti, può essere eseguito come parte del processo di build e testing, permettendo agli sviluppatori di eseguire analisi formali con regolarità. Questo potrebbe facilitare la rilevazione rapida dei bug e migliorare la qualità complessiva del software.

Un primo esempio con Kani

Prendiamo la funzione analizzata nel primo capitolo e proviamo a riscriverla in Rust

#![allow(unused)]
fn main() {
fn f(x: i32) {
    if x < 0 || (x < 20 && x >= 0) || (x > 20) {
        return;
    }
    panic!("Is this code unreachable?");
}
}

Vogliamo identificare se esiste un input tale che la funzione f restituisce un errore. Possiamo farlo tramite un proof harness, ovvero del codice che chiama la funzione f con virtualmente "tutti gli input possibili". Questo è possibile tramite il seguente codice.

#![allow(unused)]
fn main() {
#[cfg(kani)]
#[kani::proof]
fn should_not_crash_f() {
    let x: i32 = kani::any();
    f(x);
}
}

Eseguendo il verificatore Kani otteniamo il seguente risultato

$ cargo kani
Kani Rust Verifier 0.52.0 (cargo plugin)
...
Check 2: f.assertion.2
	 - Status: FAILURE
	 - Description: "Is this code unreachable?"
	 - Location: src/main.rs:5:5 in function f

SUMMARY:
 ** 1 of 3 failed
Failed Checks: Is this code unreachable?
 File: "src/main.rs", line 5, in f

VERIFICATION:- FAILED
Verification Time: 0.12590145s

Summary:
Verification failed for - should_not_crash_f
Complete - 0 successfully verified harnesses, 1 failures, 1 total.

Questo ci dice che il Kani ha trovato un valore in cui la funzione va in crash. Per ottenere il valore concreto è necessario generare una traccia con il seguente comando.

$ cargo kani --visualize --enable-unstable

Questo comando genera una traccia in formato HTML che è possibile aprire in un browser. Se cerchiamo nella traccia, dovremmo vedere poco prima del check fallito il valore x = 20.

Step 837: Function MISSING, File MISSING, Line 0
<- kani::any::<i32>
Step 838: Function MISSING, File MISSING, Line 0
x = 20 (00000000 00000000 00000000 00010100)

In effetti, è possibile verificare con facilità che con il valore x = 20 la funzione f va in crash, grazie alla chiamata a panic.