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.