Bound checking

Tramite Kani è possibile verificare formalmente che una funzione rispetta i limiti della memoria ad esempio si un array. Prendiamo come esempio una funzione che ritorna l'elemento di un array a un certo indice.

#![allow(unused)]
fn main() {
fn get_mod(i: usize, a: &[u32]) -> u32 {
    if a.len() == 0 {
        return 0;
    }
    return a[i % (a.len() + 1)];
}
}

Questa funzione presenta un bug, infatti la riduzione in modulo dovrebbe essere fatta con a.len() e non con a.len() + 1. Esiste quindi un particolare input che farà andare in crash il programma. Possiamo scrivere un proof harness di Kani per verificarlo.

#![allow(unused)]
fn main() {
#[cfg(kani)]
#[kani::proof]
fn bound_check() {
    let size: usize = kani::any();
    kani::assume(size < 4096);
    let index: usize = kani::any();
    let array: Vec<u32> = vec![0; size];
    get_mod(index, &array);
}
}

Il costrutto kani::assume() serve per istruire il model checker ad assumere una certa proposizione come vera. In questo caso, assumiamo che il nostro vettore abbia lunghezza minore di 4096. Entrambe le variabili size e index sono simboliche, e sono state create con kani::any().

Se proviamo a eseguire Kani, ci verrà restituito un caso in cui la funzione va in crash, proprio perché si è verificato un accesso fuori dai bounds.

SUMMARY:
 ** 1 of 364 failed (8 unreachable)
Failed Checks: index out of bounds: the length is less than or equal to the given index
 File: "src/main.rs", line 35, in get_mod

VERIFICATION:- FAILED

Se proviamo a correggere la funzione e togliere il bug

#![allow(unused)]
fn main() {
fn get_mod(i: usize, a: &[u32]) -> u32 {
    if a.len() == 0 {
        return 0;
    }
    return a[i % a.len()];
}
}

Otteniamo che tutti i test hanno successo, quindi la funzione non può presentare problemi.

SUMMARY:
 ** 0 of 363 failed (8 unreachable)

VERIFICATION:- SUCCESSFUL
Verification Time: 0.903892s

Complete - 1 successfully verified harnesses, 0 failures, 1 total.

Altri check di Kani

Eseguendo il test precedente, possiamo notare come Kani abbia controllato molte più cose di quanto ci aspettassimo. Questi sono alcuni esempi

Check 73: std::intrinsics::write_bytes::<u8>.arithmetic_overflow.1
	 - Status: SUCCESS
	 - Description: "write_bytes: attempt to compute number in bytes which would overflow"

Check 350: get_mod.division-by-zero.1
	 - Status: SUCCESS
	 - Description: "division by zero"

Check 358: alloc::raw_vec::RawVec::<u32>::ptr.pointer_dereference.2
	 - Status: SUCCESS
	 - Description: "dereference failure: pointer invalid"

Check 364: <alloc::raw_vec::RawVec<u32> as std::ops::Drop>::drop.pointer_dereference.1
	 - Status: SUCCESS
	 - Description: "dereference failure: dead object"

Kani sta verificando anche l'esecuzione della libreria standard (in particolare delle funzioni che riguardano Vec) per molti potenziali problemi che potrebbero far andare in crash il programma. Alcuni esempi mostrati sono

• integer overflow,
• divisione per zero, e
• de-referenziazione di oggetti.

Quando un test ha successo, vuol dire che Kani ha in qualche modo dimostrato che non è possibile che si verifichi quella particolare istanza del problema. Ad esempio se un test di una divisione per zero ha successo, non può mai succedere (nelle condizioni del proof harness) che il denominatore sia zero.