Introduzione all'analisi statica

In questo capitolo vengono introdotti i concetti basilari dell'analisi statica, e perché questa può essere utile per individuare problematiche di sicurezza. Viene fatta particolare attenzione al model checking, una tecnica di analisi statica molto usata nella pratica, e vengono proposti degli esempi di come utilizzare il software z3.

Che cos'è l'analisi statica

In questo modulo analizzeremo una delle modalità con cui è possibile analizzare staticamente i programmi, ovvero l'analisi formale. Come già detto in altri moduli, l'analisi statica di un programma viene effettuata semplicemente analizzando il codice sorgente, quindi senza eseguire il programma. In particolare l'analisi formale è una metodologia rigorosa utilizzata per verificare proprietà di sicurezza nei programmi attraverso l'uso di tecniche matematiche e logiche. Questo approccio si basa sulla costruzione di modelli astratti del codice sorgente e sull'applicazione di teoremi e regole di inferenza per dimostrare formalmente che il programma soddisfa certe proprietà. Alcune delle tecniche comuni che sono state studiate sono il model checking, l'abstract interpretation, l'esecuzione simbolica e i metodi basati sulla logica di Hoare.

Perché utilizzare l'analisi statica

La motivazione per l'utilizzo di queste metodologie è il fatto che il testing non può essere sufficiente a esaurire tutte le possibili esecuzioni del programma. Infatti ci può essere sempre qualche caso limite o qualche input non previsto, che può far invalidare una invariante oppure portare a un comportamento inaspettato. Queste tecniche permettono virtualmente di esaminare tutte le possibili esecuzioni di un programma, garantendo una copertura completa e sistematica. In altre parole, è possibile verificare formalmente delle proprietà sul programma.

In particolare, applicate all'ambito della sicurezza, queste tecniche ci possono permettere di dimostrare, ad esempio, che una certa proprietà di sicurezza viene rispettata per tutta l'esecuzione del programma. Un esempio di una proprietà interessante è il fatto che il programma non presenta bug di corruzione della memoria, ovvero per ogni possibile esecuzione ogni scrittura e ogni lettura in memoria viene eseguita correttamente in regioni valide. Un altro esempio potrebbe essere il fatto che in una applicazione web, gli utenti non privilegiati non possono mai accedere a dati riservati solo agli utenti privilegiati.

Alcune criticità

Nonostante la sua potenza, queste tecniche rimangono comunque non molto usate in pratica, o comunque relegate a porzioni di codice critiche per un sistema. Questo accade per varie ragioni.

  • Verificare proprietà arbitrarie per un programma in generale è un problema indecidibile, questo vuol dire che non esiste nessuna procedura meccanica che riesce a verificare una proprietà per un programma arbitrario. Questo fatto deriva direttamente dall'halting problem, ovvero non è possibile decidere se un programma terminerà oppure no dato un certo input, semplicemente analizzando il programma e l'input ricevuti.
  • A volte la formalizzazione di proprietà è molto complessa, in quanto devono essere espresse in un linguaggio matematico estremamente rigoroso. La verifica di proprietà complesse che coinvolgono oggetti di natura complessa può essere difficile da formalizzare, e da dimostrare.
  • Spesso gli strumenti a disposizione non sono molto intuitivi da utilizzare, e questo potrebbe scoraggiare qualche utente novizio nel loro utilizzo.

Questo modulo si propone anche l'obiettivo di semplificare l'approccio alle metodologie formali, per renderle accessibili anche a chi non si è mai interfacciato con questo ambito.

Diversi tipi di analisi statica

Come già detto, il problema di verificare una proprietà arbitraria per un programma è fondamentalmente indecidibile. Però, come per molti problemi indecidibili, è possibile comunque provare ad approssimare il problema, cercando di trovare soluzioni utili. In particolare le principali tecniche per approssimare sono le seguenti.

Interpretazione astratta

L'interpretazione astratta consiste nel fornire diverse astrazioni per un linguaggio di programmazione o di specifica. La semantica concreta rappresenta il comportamento in modo preciso del programma, descrivendo l'insieme delle tracce di esecuzione possibili. Queste però tipicamente portano a situazioni di non computabilità, quindi quello che viene fatto è derivare semantiche più astratte, come ad esempio l'insieme degli stati raggiungibili.

L'obiettivo dell'analisi statica è ottenere un'interpretazione semantica calcolabile, ad esempio rappresentando lo stato di un programma che manipola variabili intere solo tramite il loro segno (positivo o negativo). Questa astrazione può mantenere precisione per alcune operazioni, come la moltiplicazione, ma può perderla per altre, come la somma di numeri con segni opposti. Per questo si parla di sovra-approssimazione della semantica reale del programma. La perdita di precisione è talvolta necessaria per rendere la semantica decidibile, in quanto è necessario bilanciare accuratezza e costo computazionale. Le astrazioni utilizzate nella pratica sono adattate alle proprietà e ai programmi da analizzare, a seconda di cosa è interessante verificare.

Logica di Hoare

La logica di Hoare è un sistema formale che descrive un insieme di regole logiche per analizzare rigorosamente la correttezza di programmi. Si basa su una costruzione sintattica, detta tripla di Hoare, che è della forma

$$ \{P\}\quad C \quad \{Q\} $$

dove \(P\) è una formula detta precondizione, \(Q\) è una formula detta postcondizione, e \(C\) è un comando (si può pensare come un programma). L'idea è che la tripla è valida se per ogni stato iniziale che soddisfa la precondizione, allora l'esecuzione del programma parta a uno stato finale che soddisfa la postcondizione. Un esempio di tripla valida è il seguente.

$$ \{x \geq 0\}\quad x = x + 1 \quad \{x \geq 1\} $$

Assumendo che \(x\) sia un intero, ogni stato che soddisfa \(x \geq 0\), dopo l'incremento di \(x\) soddisferà anche \(x \geq 1\). La logica di Hoare definisce assiomi e regole che possono essere usate per dimostrare la correttezza di triple arbitrarie, notando che questa logica per garantire la correttezza rimane comunque indecidibile.

Model checking

Nel model checking vengono considerati sistemi con un numero di stati finito (tipicamente rappresentati come sistemi di transizione), oppure che possono essere rappresentati con un numero di stati finito grazie a un apposita astrazione. Vengono poi applicate delle metodologie formali per dimostrare proprietà riguardo questo sistema. Queste proprietà nella pratica si trasformano in formule logiche, che possono essere risolte tramite alcuni risolutori SAT o SMT. Vedremo nel prossimo capitolo più nel dettaglio questa tecnica.

Introduzione al model checking

In generale, per model checking si intende un metodo per verificare che un sistema con stati finiti soddisfi una data proprietà o specifica. Tipicamente, questi modelli sono associati a sistemi hardware o software, dove le proprietà interessanti da verificare sono ad esempio proprietà di safety (il programma non va mai in crash) oppure di liveness (il programma non entra mai in un deadlock). Uno dei principali strumenti che viene usato per far sì che i model checker siano utili nella pratica è la categoria dei risolutori SMT.

Risolutori SMT

Tipicamente queste proprietà sui programmi vengono ridotte a espressioni in un linguaggio logico formale, e poi vengono usati risolutori logici per dimostrarle o falsificarle. In particolare, stanno diventando molto popolari i cosiddetti risolutori SAT e SMT, perché nella pratica funzionano particolarmente bene. Un risolutore SMT risolve il problema della Satisfiability Modulo Theories, ovvero determinare se una formula logica ammette un assegnamento che la rende vera. In particolare sono diventati molto popolari risolutori quali z3 oppure cvc5, che mirano a risolvere SMT su istanze che possono essere trovate nella pratica. Per questa ragione, sono diventati uno dei tasselli per moltissime applicazioni, dalla verifica formale alla dimostrazione automatica di teoremi.

Il risolutore SMT z3

Z3 è uno dei più famosi strumenti che permettono di risolvere il problema SMT. Prima di descrivere il suo funzionamento, consideriamo questa funzione scritta in c

int f(int x) {
    if (x < 0 || (x < 20 && x >= 0) || (x > 20)) {
        return 1;
    }
    return 0;
}

Analizzando il codice potremmo chiederci per quali input la funzione ritorna 0. Potremmo provare a capire e interpretare le condizioni, e in effetti in questo caso è molto semplice, ma in presenza di condizioni più complesse potrebbe non essere ovvio con quali input una condizione viene verificata. Possiamo utilizzare z3 esattamente per risolvere questo problema. In questo esempio, verrà utilizzato z3 con la sua interfaccia in Python, che può essere installato tramite il pacchetto pip z3-solver.

Per prima cosa definiamo un nuovo oggetto Solver

import z3

x = z3.Int('x')
s = z3.Solver()

A questo punto aggiungiamo al solver le condizioni che fanno ritornare 0 alla funzione, e stampiamo un modello

s.add(z3.Not(x < 0))
s.add(z3.Not(z3.And(x < 20, x >= 0)))
s.add(z3.Not(x > 20))
s.check()
print(s.model())

L'output del programma è

[x = 20]

Z3 è riuscito a trovare che 20 è un input valido alla funzione affinché ritorni 0. La cosa molto interessante è che se aggiungiamo al solver la condizione x != 20

s.add(x != 20)
print(s.check())

L'output del programma è

unsat

ovvero z3 ha determinato che nessun assegnamento di x soddisfa tutte le condizioni, ovvero il modello è non soddisfacibile, (unsatisfiable). Da questo si può dedurre quindi che x=20 era anche l'unico valore di input per cui la funzione sarebbe ritornata 0. Di seguito viene riportato lo script completo.

import z3

x = z3.Int('x')
s = z3.Solver()

s.add(z3.Not(x < 0))
s.add(z3.Not(z3.And(x < 20, x >= 0)))
s.add(z3.Not(x > 20))
s.check()
print(s.model())

s.add(x != 20)
print(s.check())

Si deve precisare, però, che l'astrazione utilizzata non è del tutto corretta, in quanto stiamo modellando x come un intero, mentre in c gli interi sono rappresentati su un numero fisso di bit, e sono soggetti a overflow e underflow. Per una rappresentazione più accurata in z3 di questi tipi di dati è possibile utilizzare il costrutto BitVec, che modella anche le operazioni aritmetiche di macchina. Inoltre, è possibile modellare altre strutture, come numeri a virgola mobile, liste, strutture dati, e molto altro. Per la documentazione completa si rimanda alla pagina del progetto.

Analisi statica in Rust

Questo capitolo introduttivo fornisce una base solida per esplorare l'analisi statica in Rust, evidenziando l'importanza di questa pratica nel contesto del linguaggio e preparando il terreno per una discussione approfondita sugli strumenti e le tecniche disponibili.

L'importanza dell'analisi statica in Rust

Rust è rinomato per il suo potente sistema di controllo dei tipi, che fornisce una molte garanzie di sicurezza e correttezza del codice. Tuttavia, nonostante la potenza del type checker di Rust, ci sono diverse situazioni in cui l'analisi statica continua a giocare un ruolo cruciale. Vediamo un alcuni esempi.

Errori Logici

Anche avendo a disposizione un controllo dei tipi rigoroso, è possibile introdurre errori logici nel codice, ovvero errori derivanti dal fatto che l'implementazione non rispecchia il comportamento atteso. Questi errori non sono sempre catturati dal compilatore, poiché coinvolgono la logica dell'applicazione piuttosto che la correttezza sintattica o semantica del codice. L'analisi statica può aiutare a identificare diverse situazioni in cui si possono verificare degli errori logici, come l'uso scorretto delle API o delle librerie, oppure gli errori che possono portare a comportamenti indesiderati o bug di sicurezza.

Unsafe Rust

Rust permette l'uso di codice "unsafe" per situazioni in cui è necessario aggirare le garanzie di sicurezza del linguaggio per motivi di prestazioni o per interfacciarsi con librerie di basso livello. Tuttavia, come è stato visto nel modulo di introduzione a Rust, l'uso di unsafe introduce il rischio di corruzione della memoria, race condition e altri tipi comportamenti non definiti che il compilatore normalmente impedirebbe. L'analisi statica può aiutare a verificare formalmente delle invariati di sicurezza del programma, anche se scritto con codice unsafe.

Undefined Behaviour

I casi di undefined behaviour (comportamenti non definiti) sono uno dei grandi problemi di linguaggi a basso livello come c o c++. Si tratta di buchi nella specifica del linguaggio, e nel caso ci sia un undefined behaviour, non viene specificato come il compilatore dovrebbe intervenire. Esempi di undefined behaviour in c sono gli integer overflow su interi con segno, gli accessi out-of-bounds oppure la de-referenziazione di un puntatore NULL. La non specifica di comportamenti precisi in queste situazioni, possono portare i compilatori a generare codice inaspettato, anche a volte eliminando intere porzioni di codice. Anche se Rust cerca di minimizzare i casi di undefined behaviour, questi possono comunque verificarsi, soprattutto in codice unsafe o quando si ci si interfaccia con librerie esterne. Molti strumenti di analisi statica possono trovare istanze di undefined behaviour, segnalandole e permettendo agli sviluppatori di risolverle.

Introduzione a MIR

Nell'ambito della programmazione in Rust, uno degli elementi chiave per comprendere le capacità del linguaggio in termini di sicurezza e prestazioni è la sua rappresentazione intermedia a medio livello, conosciuta come MIR, ovvero Mid-level Intermediate Representation. MIR è una rappresentazione intermedia del codice Rust che si trova tra l'AST (Abstract Syntax Tree) generato dal parser e il codice macchina finale prodotto dal compilatore. Questa rappresentazione gioca un ruolo cruciale in vari aspetti del processo di compilazione, in particolare nell'ottimizzazione e nell'analisi statica del codice.

Il Ruolo di MIR

Nel processo di compilazione di Rust, MIR assume un ruolo fondamentale per diversi motivi. Per prima cosa, a questo livello è possibile effettuare Ottimizzazione del Codice. Infatti, una volta che il codice Rust è stato trasformato in MIR, il compilatore può applicare una serie di ottimizzazioni più aggressive e mirate, perché MIR è una rappresentazione più semplificata e normalizzata del codice, che elimina molte delle complessità e delle astrazioni presenti nel codice sorgente originale.

Uno degli aspetti più importanti di MIR è il fatto che a questo livello viene eseguito il Borrow Checker. MIR è infatti basato su un modello a grafo di control-flow, fondamentale per il funzionamento del borrow checker, permettendo al compilatore di verificare in modo più efficiente e accurato che il codice rispetti le regole di borrowing e lifetime. Dopo l'ottimizzazione e l'analisi, MIR viene ulteriormente trasformato in una rappresentazione ancora più bassa chiamata LLVM IR (Intermediate Representation), che viene poi utilizzata per generare il codice macchina finale da LLVM.

A livello di MIR operano anche moltissimi strumenti che eseguono analisi statica dei programmi, in quanto sono rimosse molte astrazioni ad alto livello, ma comunque nasconde molti dettagli dell'architettura e dell'hardware. Si tratta quindi di un buon compromesso tra basso livello e alto livello. Analizzatori e strumenti possono esaminare il MIR per individuare bug, potenziali problemi di sicurezza e opportunità di miglioramento delle prestazioni senza dover interpretare direttamente il codice sorgente Rust, che può essere più complesso e variegato.

Esempio di MIR

Prendiamo questo codice Rust

fn main() {
    let mut vec = Vec::new();
    vec.push(1);
}

Possiamo visualizzare il codice MIR generato nel playground ufficiale di Rust. Per il codice sopra dovremmo ottenere un output di questo tipo

// WARNING: This output format is intended for human consumers only
// and is subject to change without notice. Knock yourself out.
fn main() -> () {
    let mut _0: ();
    let mut _1: std::vec::Vec<i32>;
    let _2: ();
    let mut _3: &mut std::vec::Vec<i32>;
    scope 1 {
        debug vec => _1;
    }

    bb0: {
        _1 = Vec::<i32>::new() -> [return: bb1, unwind continue];
    }

    bb1: {
        _3 = &mut _1;
        _2 = Vec::<i32>::push(move _3, const 1_i32) -> [return: bb2, unwind: bb4];
    }

    bb2: {
        drop(_1) -> [return: bb3, unwind continue];
    }

    bb3: {
        return;
    }

    bb4 (cleanup): {
        drop(_1) -> [return: bb5, unwind terminate(cleanup)];
    }

    bb5 (cleanup): {
        resume;
    }
}

L'output è costituito da molti basic blocks, e le variabili e i rispettivi drop sono esplicitamente indicati. Inoltre ogni variabile è esplicitamente accompagnata dal suo tipo. Il controllo del flusso è indicato come relazioni tra i basic-blocks. Non è importante capire nel dettaglio questa rappresentazione, ma solo il fatto che stiamo operando a un livello di astrazione intermedio, né troppo basso né troppo alto.

Strumenti di analisi statica su MIR

Rust ha un ecosistema ricco di strumenti per l'analisi statica che sfruttano la rappresentazione intermedia MIR per migliorare la qualità, la sicurezza e le prestazioni del codice. Come abbiamo detto, questi strumenti permettono di analizzare il codice a un livello più astratto rispetto al codice macchina, mantenendo comunque un dettaglio sufficiente per individuare potenziali problemi. Di seguito, viene presentata una panoramica di alcuni dei più usati strumenti di analisi statica basati su MIR.

MIRAI

MIRAI è un analizzatore statico avanzato per Rust, sviluppato da Facebook. MIRAI utilizza MIR per eseguire verifiche dettagliate sul codice Rust, identificando potenziali bug e vulnerabilità prima della fase di esecuzione. Tra le sue funzionalità principali:

  • Verifica del flusso di dati: MIRAI traccia il flusso di dati attraverso il programma, identificando possibili vulnerabilità come overflow, accessi a memoria non valida e condizioni di race.
  • Analisi delle invarianti: Può verificare invarianti e precondizioni, garantendo che le funzioni rispettino i contratti definiti.
  • Analisi dei contratti di funzione: Consente agli sviluppatori di specificare pre e post-condizioni per le funzioni, migliorando la verificabilità del codice.

Miri

Miri è un interprete per il sottoinsieme di Rust che include la rappresentazione MIR. Miri esegue il codice Rust in un ambiente controllato, permettendo di individuare errori di corruzione della memoria e di comportamento indefinito che potrebbero sfuggire al compilatore. Le principali caratteristiche di Miri includono:

  • Esecuzione interpretata: Miri esegue il codice Rust interpretando MIR, il che consente di rilevare problemi come l'accesso a memoria non inizializzata e overflow aritmetici.
  • Supporto per unsafe: È particolarmente utile per il debugging di codice unsafe, permettendo di eseguire codice che interagisce direttamente con la memoria in modo sicuro e controllato.
  • Compatibilità con test: Può essere utilizzato insieme ai test Rust per identificare problemi che si manifestano solo in specifiche condizioni di esecuzione.

Rust Analyzer

Rust Analyzer è un moderno analizzatore di codice per Rust che si integra con vari editor di testo e IDE. Sebbene non sia specificamente focalizzato su MIR, Rust Analyzer sfrutta MIR per fornire funzionalità avanzate di completamento del codice, analisi di tipo e refactoring. Le sue funzionalità includono:

  • Completamento intelligente del codice: Suggerisce completamenti basati sul contesto del codice, migliorando la produttività degli sviluppatori.
  • Navigazione del codice: Permette di navigare facilmente tra definizioni, dichiarazioni e usi delle variabili e delle funzioni.
  • Refactoring: Fornisce strumenti per ristrutturare il codice in modo sicuro, mantenendo la correttezza del programma.

Clippy

Clippy è un linter per Rust che aiuta a scrivere codice idiomatico e a evitare pattern di programmazione comuni che possono portare a bug. Utilizza MIR per alcune delle sue analisi più avanzate, offrendo suggerimenti su come migliorare il codice. Le sue caratteristiche includono:

  • Suggerimenti idiomatici: Consiglia modifiche per rendere il codice più idiomatico e leggibile secondo le convenzioni di Rust.
  • Identificazione di pattern rischiosi: Segnala l'uso di pattern di programmazione che possono essere fonte di bug o problemi di prestazioni.
  • Configurabilità: Gli sviluppatori possono configurare Clippy per ignorare specifici avvertimenti o applicare regole personalizzate.

Kani

Kani è uno strumento di verifica formale per Rust che utilizza MIR per analizzare e verificare proprietà formali del codice. Kani sfrutta tecniche di model checking per garantire che il codice rispetti determinati invarianti e comportamenti attesi. Le sue caratteristiche principali includono:

  • Verifica delle proprietà formali: Kani permette di specificare proprietà formali del codice (come invarianti e post-condizioni) che devono essere verificate durante l'analisi. Utilizza tecniche di model checking per esplorare tutte le possibili esecuzioni del programma e garantire che queste proprietà siano rispettate.
  • Analisi di sicurezza: Può identificare vulnerabilità di sicurezza come buffer overflow, accessi non sicuri alla memoria e condizioni di race. Questa analisi è particolarmente utile per il codice unsafe, dove le garanzie di sicurezza del compilatore Rust sono disabilitate.
  • Integrazione con il flusso di lavoro di sviluppo: Kani si integra facilmente con il flusso di lavoro di sviluppo Rust, permettendo agli sviluppatori di eseguire analisi formali come parte del processo di build e testing.
  • Supporto per l'annotazione del codice: Gli sviluppatori possono annotare il codice Rust con specifiche formali che Kani utilizzerà per la verifica. Questo rende il processo di verifica formale trasparente e parte integrante dello sviluppo del software.

Analizzare i programmi Rust con Kani

Questo capitolo introduttivo fornisce una panoramica su come Kani può essere utilizzato per analizzare e migliorare i programmi Rust, offrendo una guida dettagliata su come sfruttare le capacità avanzate di questo strumento per migliorare la sicurezza e la correttezza del codice.

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.

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.

Loop unwinding

I cicli sono trattati in modo particolare da Kani. Prendiamo questo esempio che inizializza un vettore a zero.

#![allow(unused)]
fn main() {
fn initialize_prefix(buffer: &mut [u8], up_to: usize) {
    if up_to > buffer.len() {
        return;
    }

    for i in 0..=up_to {
        buffer[i] = 0;
    }
}
}

Questo codice presenta un errore di tipo off-by-one, possiamo scrivere un proof harness per questa funzione.

#![allow(unused)]
fn main() {
#[cfg(kani)]
#[kani::proof]
fn loop_unwinding() {
    let up_to: usize = kani::any();
    let array = [1; 16];
    initialize_prefix(&mut array, up_to);
}
}

Se proviamo a eseguire così il verificatore non terminerà mai. Questo perché Kani ha l'approccio ai loop chiamato loop unwinding, ovvero mette in sequenza le istruzioni del corpo del ciclo, e verifica ogni possibile caso. Possiamo istruire su quanti cicli espandere tramite la macro kani::unwind.

#![allow(unused)]
fn main() {
#[cfg(kani)]
#[kani::proof]
#[kani::unwind(20)]
fn loop_unwinding() {
    let up_to: usize = kani::any();
    let array = [1; 16];
    initialize_prefix(&mut array, up_to);
}
}

Adesso Kani riesce a eseguire tutto il loop in tempo finito, e trova l'errore.

 ** 1 of 74 failed
Failed Checks: index out of bounds: the length is less than or equal to the given index
 File: "src/main.rs", line 53, in initialize_prefix

VERIFICATION:- FAILED
Verification Time: 0.70454884s

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

Risoluzione del problema

Proviamo adesso a risolvere il bug di tipo off-by-one, modificando la condizione all'interno dell'if.

#![allow(unused)]
fn main() {
fn initialize_prefix(buffer: &mut [u8], up_to: usize) {
    if up_to >= buffer.len() {
        return;
    }

    for i in 0..=up_to {
        buffer[i] = 0;
    }
}
}

Eseguendo Kani, la verifica andrà adesso a buon fine, e questo ci garantisce che la funzione non presenterà problemi.

SUMMARY:
 ** 0 of 74 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 0.6491398s

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

Variabili non deterministiche

Nel contesto della verifica formale, le variabili non deterministiche giocano un ruolo cruciale, specialmente quando si tratta di esplorare tutte le possibili esecuzioni di un programma. Abbiamo già visto l'uso di variabili non deterministiche, e adesso ne faremo altri esempi

Come abbiamo visto, le variabili non deterministiche sono variabili il cui valore non è fissato durante l'esecuzione dell'analisi. Invece di avere un valore predeterminato, queste variabili possono assumere qualsiasi valore all'interno di un insieme specificato. Questo approccio è utile per simulare una varietà di scenari e per garantire che il programma gestisca correttamente tutti i possibili casi.

Variabili non deterministiche intere

Supponiamo di voler verificare che una funzione che calcola il quadrato di un numero intero non produca un overflow. Utilizziamo una variabile non deterministica per rappresentare l'input della funzione.

#![allow(unused)]
fn main() {
fn square(x: i32) -> i32 {
    x * x
}

#[kani::proof]
fn check_square() {
    let x: i32 = kani::any();
    // Verifica che il risultato sia non negativo e che non ci sia overflow
    let result = square(x);
    assert!(result >= 0, "Result should be non-negative");
}
}

In questo esempio, kani::any() crea una variabile non deterministica x che può assumere qualsiasi valore i32. Kani esplora tutti i valori possibili per x, verificando che la funzione square non produca risultati negativi e non causi overflow. Il codice presenta possibilità di integer overflow, quindi l'analisi fallisce.

SUMMARY:
 ** 1 of 4 failed
Failed Checks: attempt to multiply with overflow
 File: "src/main.rs", line 58, in square

VERIFICATION:- FAILED

Variabili non deterministiche booleane

Consideriamo una funzione che esegue operazioni diverse in base al valore di un flag booleano. Utilizziamo una variabile non deterministica per rappresentare questo flag.

#![allow(unused)]
fn main() {
fn toggle(value: i32, flag: bool) -> i32 {
    if flag {
        value + 1
    } else {
        value - 1
    }
}

#[kani::proof]
fn check_toggle() {
    let value: i32 = kani::any();
    let flag: bool = kani::any();
    let result = toggle(value, flag);
    // Verifica che il risultato sia sempre un valore intero valido
    assert!(result >= i32::MIN && result <= i32::MAX);
}
}

In questo esempio, kani::any() è utilizzato per creare una variabile non deterministica flag di tipo booleano. L'esecuzione di Kani verifica che, indipendentemente dal valore di flag, la funzione toggle produca sempre un valore intero valido. Infatti, questa funzione può dare sia overflow che underflow, a seconda del valore di flag. Il risultato dell'analisi riporta due controlli falliti.

 ** 2 of 3 failed
Failed Checks: attempt to add with overflow
 File: "src/main.rs", line 72, in toggle
Failed Checks: attempt to subtract with overflow
 File: "src/main.rs", line 74, in toggle

VERIFICATION:- FAILED

Variabili non deterministiche di tipo array

Come abbiamo già visto, è possibile creare variabili non deterministiche di tipo array e anche Vec, anche con dimensione anch'essa non deterministica.

#![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];
    // ...
}
}

Questo proof harness controllerà l'esecuzione per tutti i vettori di dimensione minore di 4096.

Oltre l'analisi statica

Nel panorama dello sviluppo software moderno, garantire la robustezza e la sicurezza del codice è una priorità fondamentale. L'analisi statica svolge un ruolo cruciale nell'individuare errori di sintassi, problemi di tipo e vulnerabilità potenziali già durante la fase di compilazione. Tuttavia, non è l'unica strategia disponibile per garantire la qualità del software. In questo capitolo, esploreremo due approcci complementari che ampliano le capacità di testing e verifiche: il fuzzing e il proptest.

Il fuzzing rappresenta una tecnica dinamica di testing che mira a esplorare input casuali o non validi nel software al fine di individuare bug, crash o vulnerabilità di sicurezza. Questa metodologia si distingue per la sua capacità di scoprire scenari d'uso inattesi che potrebbero sfuggire all'analisi statica tradizionale.

D'altra parte, proptest è una libreria per la generazione automatica di input.

Esploreremo come l'uso combinato di fuzzing e proptest non solo estenda le capacità di testing del codice Rust, ma anche migliorare la sicurezza, la robustezza e l'affidabilità delle applicazioni, integrandosi efficacemente con le pratiche esistenti di analisi statica.

Fuzzing di programmi Rust

Il fuzzing è una tecnica di testing dinamica che consiste nel fornire input casuali o non validi a un programma al fine di individuare bug, crash o vulnerabilità di sicurezza. In Rust, possiamo sfruttare lo strumento cargo-fuzz per eseguire il fuzzing dei nostri programmi in modo efficace e automatizzato.

Configurazione di cargo-fuzz

Per utilizzare cargo-fuzz, è necessario aggiungere cargo-fuzz come dipendenza nel file Cargo.toml del progetto:

[dependencies]
fuzz_targets = "0.2"

[dev-dependencies]
cargo-fuzz = "0.11"

Creiamo quindi una cartella fuzz nella radice del progetto e all'interno un file fuzz/Cargo.toml:

[package]
name = "fuzz"
version = "0.1.0"
edition = "2021"

[dependencies]
fuzz_targets = "0.2"

Definizione di un target di fuzzing

Successivamente, definiamo un target di fuzzing nel file fuzz/fuzz_targets/parse.rs, in questo esempio stiamo cercando di capire se il parsing di un i32 da una stringa può dare problemi.

#![allow(unused)]
#![no_main]
fn main() {
use libfuzzer_sys::fuzz_target;

// Questa funzione è il nostro target di fuzzing
fuzz_target!(|data: &[u8]| {
    // Convertiamo l'input in una stringa UTF-8
    if let Ok(s) = std::str::from_utf8(data) {
        // Eseguiamo il parsing della stringa
        let _ = s.parse::<i32>();
    }
});
}

Esecuzione del Fuzzing

Per eseguire il fuzzing, possiamo utilizzare il comando cargo fuzz run parse:

$ cargo fuzz run parse

Durante l'esecuzione, cargo-fuzz genera automaticamente input casuali per testare la funzione di parsing. Ogni volta che viene trovato un input che provoca un fallimento, cargo-fuzz conserva quel caso di test per ulteriori analisi. cargo-fuzz produce inoltre report dettagliati che mostrano gli input che hanno causato crash o errori nel programma sotto test. Questi report sono essenziali per comprendere e risolvere le vulnerabilità o i bug identificati durante il fuzzing.

Tramite il fuzzing in Rust è possibile:

  • Identificare precocemente di Bug: il fuzzing permette di individuare bug e vulnerabilità di sicurezza che potrebbero non essere stati previsti durante lo sviluppo.
  • Automatizzare il Testing: cargo-fuzz automatizza il processo di generazione e test di input casuali, riducendo l'onere manuale sullo sviluppatore.
  • Migliorare la Sicurezza: migliorando la copertura dei test, il fuzzing contribuisce a garantire che il software sia robusto e sicuro anche in presenza di input non previsti.

Test Property-Based con proptest-rs

I test property-based sono una metodologia di testing che si basa sulla generazione automatica di input per verificare le proprietà del software in condizioni diverse e estreme. In Rust, proptest-rs è una libreria potente e flessibile che facilita la creazione di test property-based, garantendo una copertura più completa e una maggiore affidabilità del codice.

Introduzione a proptest-rs

proptest-rs permette di definire proprietà del software e genera automaticamente input che le violano, consentendo di scoprire edge case e comportamenti inaspettati. Questo approccio si distingue dai test tradizionali, dove gli input sono staticamente definiti, e permette di esplorare in modo più completo lo spazio delle possibilità del software. Per iniziare, aggiungiamo proptest come dipendenza nel nostro file Cargo.toml:

[dev-dependencies]
proptest = "1.0"

Successivamente, definiamo un test property-based nel file di test Rust:

#![allow(unused)]
fn main() {
use proptest::prelude::*;

#[test]
fn test_reverse() {
    // Definiamo la proprietà: invertire una lista due volte torna alla lista originale
    fn reverse_twice_prop(input: Vec<i32>) -> bool {
        let reversed = input.iter().rev().cloned().collect::<Vec<_>>();
        let twice_reversed = reversed.iter().rev().cloned().collect::<Vec<_>>();
        input == twice_reversed
    }

    // Configuriamo proptest per generare input
    proptest!(|(input in prop::collection::vec(-100..100, 1..1000))| {
        // Verifichiamo la proprietà per ogni input generato
        assert!(reverse_twice_prop(input));
    });
}
}

In questo esempio si può trovare

  1. Definizione della Proprietà reverse_twice_prop: questa funzione verifica che invertire una lista due volte torni alla lista originale.

  2. Utilizzo di proptest! Macro: la macro proptest! genera input casuali basati sulle specifiche fornite. Nel nostro caso, genera liste di numeri interi nel range da -100 a 100, con dimensioni variabili da 1 a 999 elementi.

  3. Verifica della Proprietà: per ogni input generato, la proprietà reverse_twice_prop viene verificata utilizzando l'asserzione assert!, assicurando che la proprietà sia soddisfatta per ogni caso generato.

Esempio di Prevenzione di IDOR in Rust con actix-web

Per prevenire IDOR (Insecure Direct Object Reference) in una API web scritta in Rust con actix-web, possiamo implementare controlli di autorizzazione adeguati e utilizzare test property-based con proptest-rs per verificare che l'accesso agli oggetti sia correttamente limitato agli utenti autorizzati.

Supponiamo di avere un sistema di gestione di risorse dove gli utenti possono accedere solo alle risorse a cui sono autorizzati. Utilizzeremo JSON Web Token (JWT) per l'autenticazione e l'autorizzazione degli utenti.

use actix_web::{web, App, HttpResponse, HttpServer, Responder};
use jsonwebtoken::{decode, DecodingKey, Validation};
use serde::{Deserialize, Serialize};
use std::collections::HashMap;

// Struttura per rappresentare una risorsa
#[derive(Debug, Serialize, Deserialize)]
struct Resource {
    id: u64,
    name: String,
    owner_id: u64,
}

// Dati per simulare un database di risorse
lazy_static::lazy_static! {
    static ref RESOURCES: HashMap<u64, Resource> = {
        let mut map = HashMap::new();
        map.insert(1, Resource { id: 1, name: "Resource 1".to_string(), owner_id: 1 });
        map.insert(2, Resource { id: 2, name: "Resource 2".to_string(), owner_id: 2 });
        map.insert(3, Resource { id: 3, name: "Resource 3".to_string(), owner_id: 1 });
        map
    };
}

// Dati per simulare utenti autorizzati (id e JWT)
lazy_static::lazy_static! {
    static ref USERS: HashMap<u64, String> = {
        let mut map = HashMap::new();
        map.insert(1, generate_jwt_token(1));
        map.insert(2, generate_jwt_token(2));
        map
    };
}

// Funzione per generare un JWT token per un utente con un dato id
fn generate_jwt_token(user_id: u64) -> String {
    let claims = serde_json::json!({ "sub": user_id });
    jsonwebtoken::encode(&jsonwebtoken::Header::default(), &claims, &DecodingKey::from_secret("secret".as_ref())).unwrap()
}

// Funzione per verificare e ottenere l'id dell'utente dal token JWT
fn get_user_id_from_token(token: &str) -> Option<u64> {
    let decoding_key = DecodingKey::from_secret("secret".as_ref());
    let validation = Validation::default();

    match decode::<HashMap<String, serde_json::Value>>(token, &decoding_key, &validation) {
        Ok(token_data) => {
            if let Some(user_id) = token_data.claims.get("sub") {
                if let Some(user_id) = user_id.as_u64() {
                    return Some(user_id);
                }
            }
            None
        },
        Err(_) => None,
    }
}

// Handler per ottenere una risorsa
async fn get_resource(info: web::Path<u64>, auth_header: web::HeaderMap) -> impl Responder {
    // Estraiamo il JWT token dall'header Authorization
    let token = auth_header.get("Authorization")
        .and_then(|v| v.to_str().ok())
        .and_then(|s| s.strip_prefix("Bearer "))
        .unwrap_or("");

    // Verifichiamo il token JWT e otteniamo l'id dell'utente
    let user_id = match get_user_id_from_token(token) {
        Some(user_id) => user_id,
        None => return HttpResponse::Unauthorized().body("Unauthorized"),
    };

    // Cerchiamo la risorsa nel database
    if let Some(resource) = RESOURCES.get(&info.into_inner()) {
        // Verifichiamo che l'utente sia autorizzato ad accedere alla risorsa
        if resource.owner_id == user_id {
            HttpResponse::Ok().json(resource)
        } else {
            HttpResponse::Forbidden().body("Accesso negato")
        }
    } else {
        HttpResponse::NotFound().body("Risorsa non trovata")
    }
}

#[actix_web::main]
async fn main() -> std::io::Result<()> {
    HttpServer::new(|| {
        App::new()
            .route("/resources/{id}", web::get().to(get_resource))
    })
    .bind("127.0.0.1:8080")?
    .run()
    .await
}

In questo esempio si trovano le seguenti parti:

  • Implementazione dell'API:

    • Resource rappresenta una struttura dati per le risorse, con un id univoco, un name e owner_id che identifica il proprietario della risorsa.
    • RESOURCES è una mappa simulata che contiene le risorse nel sistema.
    • USERS è una mappa che associa gli id degli utenti ai loro token JWT simulati.

  • Verifica dell'Accesso: nel handler get_resource, estraiamo e verifichiamo il token JWT dall'header Authorization. Inoltre la funzione get_user_id_from_token decodifica e verifica il token JWT, estraendo l'id dell'utente.

  • Controllo di Autorizzazione: dopo aver ottenuto l'id dell'utente dal token JWT, verifichiamo se l'utente è il proprietario della risorsa richiesta. Se non è il proprietario, restituiamo una risposta Forbidden.

  • Gestione delle Risposte: il server gestisce le richieste GET all'endpoint /resources/{id}. Restituisce la risorsa se trovata, altrimenti restituisce un messaggio di errore appropriato.

Test Property-Based per Prevenire IDOR

Possiamo utilizzare proptest-rs per verificare che solo gli utenti autorizzati possano accedere alle loro risorse. Definiamo un test che generi input casuali di id risorsa e token JWT, verificando che solo gli utenti autorizzati possano accedere alle risorse corrette:

#![allow(unused)]
fn main() {
#[cfg(test)]
mod tests {
    use super::*;
    use actix_web::test;

    #[test]
    fn test_get_resource_authorization() {
        proptest!(|(resource_id in 1..=3u64, user_id in 1..=2u64)| {
            // Simuliamo il token JWT per l'utente corrente
            let token = USERS.get(&user_id).unwrap().clone();

            // Costruiamo una richiesta HTTP simulata con il token JWT
            let mut app = test::init_service(
                App::new().route("/resources/{id}", web::get().to(get_resource))
            ).unwrap();
            let req = test::TestRequest::get()
                .uri(&format!("/resources/{}", resource_id))
                .header("Authorization", format!("Bearer {}", token))
                .to_request();

            // Eseguiamo la richiesta
            let resp = test::call_service(&mut app, req);
            
            // Verifichiamo l'autorizzazione
            if let Some(resource) = RESOURCES.get(&resource_id) {
                if resource.owner_id == user_id {
                    assert_eq!(resp.status(), http::StatusCode::OK);
                } else {
                    assert_eq!(resp.status(), http::StatusCode::FORBIDDEN);
                }
            } else {
                assert_eq!(resp.status(), http::StatusCode::NOT_FOUND);
            }
        });
    }
}
}

In questo test property-based andiamo a definire le seguenti parti:

  • Definizione del Test: utilizziamo proptest! per generare input casuali di resource_id e user_id, verificando che la risposta della richiesta HTTP sia coerente con le regole di autorizzazione definite nell'API.
  • Simulazione del Token JWT: utilizziamo i token JWT simulati da USERS per simulare l'autenticazione degli utenti nelle richieste di test.
  • Verifica dell'Autorizzazione: verifichiamo che solo gli utenti autorizzati possano accedere alle risorse corrispondenti, con una corretta gestione delle risposte HTTP in base alle regole di autorizzazione.