Analisi e Verifica di Programmi
Laboratorio di AVP
Corso di Laurea in Informatica
AA 2009-’10
Tino Cortesi
Analisi e Verifica
Cosa
Individuare proprietà interessanti dei nostri programmi:
Valori prodotti, dipendenze, uso, terminazione
Perché:
Verifica, Debugging
Type checking
Verifica di asserzioni
Ottimizzazioni:
Compile time garbage collection
Ottimizzazioni source-to-source
Come
Le proprietà non banali dei programmi sono indecidibili o
computazionalmente molto costose (NP)
Approssimazioni o condizioni sufficienti
Tino Cortesi
Analisi e Verifica di Programmi
2
L’impatto degli errori run-time
Il 50% degli attacchi alla sicurezza dei sistemi
avviene tramite buffer overruns (Microsoft Security
Bulletins MS02-065, MS04-111 etc.
La maggior parte dei crash in sistemi embedded è
dovuta a overflow di vario tipo.
Tino Cortesi
Analisi e Verifica di Programmi
3
Guyana francese, 4 giugno 1996
Lancio di ARIANE 5
$600 miliardi di dollari bruciati per
un errore del software:
un dato a 64 bit in virgola mobile
venne convertito in un intero a
16 bit con segno, questa operazione
causò una trap del processore:il
numero in virgola mobile era troppo
grande per poter essere rappresentato
con un intero a 16 bit.
(autodistruzione a 39 secondi dal lancio
Tino Cortesi
Analisi e Verifica di Programmi
4
Marte, Mars Polar Lander si spegne il 3 dicembre 1999
per una variabile non inizializzata.
Tino Cortesi
Analisi e Verifica di Programmi
5
Sillabo del corso
Elementi di Teoria dei Reticoli
Interpretazione Astratta
Correttezza dell’analisi - Connessioni di Galois - Widening
Applicazioni a problemi di sicurezza
Applicazioni nell’ambito delle basi di dati
Dataflow Analysis
Liveness Analysis
Reaching Definitions - Constant Folding - Available
Expressions
Basic Blocks - Value Numbering - Alias Analysis
Loop Optimizations
Model Checking
Seminari di ricerca su temi di Analisi e Verifica di Programmi
Progetto: realizzazione guidata di codice per un’analizzatore
statico
Tino Cortesi
Analisi e Verifica di Programmi
6
Bibliografia
F.Nielson, H.R.Nielson, C. Hankin Principles of Static Analysis
Springer Verlag, 2004
B. Berard et al. Systems and Software Verification
Springer Verlag, 1999
B,A,Davey, H,A, Priestly; Introduction to Lattices and Orders,
Cambridge, 2006
Altri testi utili:
A. W. Appel, Modern Compiler Implementation in Java
Cambridge Univ. Press, 1998
Steven Mucknick, Compiler Design Implementation
Morgan Kaufmann Publ., 1997
Articoli su journals o proceedings di conferenze
Tino Cortesi
Analisi e Verifica di Programmi
7
Introduzione
Analisi
Metodo conoscitivo che procede dall’individuazione e
dallo studio dei particolari
Scomposizione di un tutto organico nelle sue parti
Tino Cortesi
Analisi e Verifica di Programmi
9
Analisi Statica di Programmi
Tecniche automatiche per inferire a tempo di
compilazione informazione approssimata sul
comportamento run-time dei programmi
Applicazioni:
Ottimizzazione di compilatori
Verifica automatica dei programmi
Certificazione - validazione del software
Sicurezza
Tino Cortesi
Analisi e Verifica di Programmi
10
Esempio
Cosa voglio verificare: assenza di un certo tipo di
errori run-time (es. overflow)
Come posso astrarre i valori numerici: Intervalli Poliedri (disuguaglianze lineari)
Quale teoria posso usare: Interpretazione astratta
Tino Cortesi
Analisi e Verifica di Programmi
11
Etichettatura
input n;
m:=2;
while n>1 do
m:= m * n;
n:= n-1;
output m;
Tino Cortesi
(1) input n;
(2) m:=2;
while (3) n>1 do
(4) m:= m * n;
(5) n:= n-1;
(6) output m;
Analisi e Verifica di Programmi
12
Grafo di flusso
1
input n
(1) input n;
(2) m:=2;
while (3) n>1 do
(4) m:= m * n;
(5) n:= n-1;
(6) output m;
2
m:= 2
3
n>1
4
m:= m*n
5
n:= n-1
Tino Cortesi
Analisi e Verifica di Programmi
6
output m
13
Possiamo inferire mediante analisi statica
che al punto (6) il valore della variabile m
sarà pari per qualsiasi valore di input n.
1
input n
2
Per fare questo l’analisi dovrà propagare
“parity information”
m:= 2
3
Possiamo assegnare ad ogni variabile uno
dei tre “valori”:
Pari
il valore è
sicuramente pari
Dispari
il valore è
sicuramente dispari
Non_So
il valore può essere
pari oppure dispari
Tino Cortesi
Analisi e Verifica di Programmi
n>1
4
m:= m*n
5
n:= n-1
6
output m
14
(1) n Non_So
(1) input n;
(2)
(2) m:= 2;
while (3) n>1 do
(3)
(4) m:= m * n;
(4)
(5) n:= n - 1;
(5)
(6) output m;
(6)
Tino Cortesi
Analisi e Verifica di Programmi
m
n
m
n
m
n
m
n
m
n
m
Non_So
Non_So
Non_So
Non_So
Pari
Non_So
Pari
Non_So
Pari
Non_So
Pari
15
Questo programma, dato un
intero positivo n, calcola il
doppio del fattoriale: 2 * (n!)
(1) input n;
(2) m:= 2;
while (3) n>1 do
(4) m:= m * n;
n=1
n=2
n=3
n=4
(5) n:= n - 1;
(6) output m;
…
…
…
…
l’output
l’output
l’output
l’output
è
è
è
è
2
4
12
48
pari!
Tino Cortesi
Analisi e Verifica di Programmi
16
(1) input n;
(2) m:= 1;
while (3) n>1 do
(4) m:= m * n;
(5) n:= n - 1;
(6) output m;
Tino Cortesi
Questo programma, dato un
intero positivo n, calcola il
fattoriale: n!
In questo caso l’analisi
precedente non restituisce
nessuna informazione utile sulla
parità di m.
Questo è corretto (per n=1…)
Ma nemmeno se restringiamo
l’input a n pari e n>1 l’analisi è
precisa: in (3) sia n che m sono
Non_So.
Analisi e Verifica di Programmi
17
Precisione e Correttezza
Questa perdita di precisione è una caratteristica comune delle
tecniche di analisi statica
La maggior parte delle proprietà sui programmi che si vogliono
inferire sono indecidibili (o NP-complete), quindi non possiamo
pensare di inferirle con precisione (ed in tempi ragionevoli)
Dobbiamo assicurarci che il risultato dell’analisi sia in ogni caso
corretto:
Se l’analisi dice SI allora sicuramente la proprietà è verificata
Se l’analisi dice NO allora può darsi che la proprietà non sia
verificata
Tino Cortesi
Analisi e Verifica di Programmi
18
Esempio
Sappiamo che il problema della terminazione è
indecidibile (halting problem)
programmi
programmi che
terminano
Tino Cortesi
Analisi e Verifica di Programmi
19
programmi che
potrebbero terminare
programmi che
sicuramente terminano
programmi
programmi che
terminano
Tino Cortesi
Analisi e Verifica di Programmi
20
Precisione e Correttezza
Un’analisi di terminazione può essere quindi di due
tipi:
“Definite”
SI
il programma sicuramente termina
NO
il programma potrebbe non terminare
“Possible”
SI
il programma può terminare
NO
il programma sicuramente non termina
Tino Cortesi
Analisi e Verifica di Programmi
21
Precisione e Correttezza
Le tecniche di analisi che introdurremo si dicono
“semantics-based”.
Questo significa che l’informazione ottenuta
dall’analisi può essere dimostrata corretta rispetto
alla semantica del linguaggio di programmazione
Tino Cortesi
Analisi e Verifica di Programmi
22
Compilatori ottimizzanti
Un compilatore ottimizzante trasforma un programma
per migliorare la sua efficienza senza modificarne
l’output.
Trasformazioni che migliorano l’efficienza:
Allocazione dei registri
Eliminazione delle sotto-espressioni comuni: se una
espressione viene calcolata più di una volta, elimina le
ripetizioni
Eliminazione di “dead-code”: cancella una computazione il
cui risultato non viene mai usato
“Constant folding”: se gli operandi di un’espressione sono
costanti, il calcolo può essere fatto a tempo di compilazione.
Tino Cortesi
Analisi e Verifica di Programmi
23
Escape Analysis
Consideriamo queste due procedure in C:
typedef int A[10000];
typedef A* B;
void esegui1(){
int i;
B b;
b = (A*) malloc(sizeof(A));
for (i=0; i<100; i++)
(*b)[i]=0;
free(b);
}
Tino Cortesi
Analisi e Verifica di Programmi
void esegui2(){
int i;
A a;
for (i=0; i<100; i++)
a[i]=0;
}
24
ambiente
typedef int A[10000];
typedef A* B;
void esegui1(){
int i;
B b;
b = (A*) malloc(sizeof(A));
for (i=0; i<100; i++)
(*b)[i]=0;
free(b);
}
int
i
B
b
memoria
stack
heap
0
L’array viene allocato nello heap e poi eliminato...
Tino Cortesi
Analisi e Verifica di Programmi
25
ambiente
typedef int A[10000];
int
i
A
a
memoria
stack
heap
0
void esegui2(){
int i;
A a;
for (i=0; i<100; i++)
a[i]=0;
}
L’array viene allocato nello stack e poi eliminato...
Tino Cortesi
Analisi e Verifica di Programmi
26
allocare nello heap costa...
for (i=0; i<1000000; i++)
esegui1();
// circa 90 sec
for (i=0; i<1000000; i++)
esegui2();
// circa 35 sec
I programmi “sembrano” uguali, ma l’allocazione nello heap fa sì che il
primo sia tre volte più lento del secondo...
Se riesco a “predire” che una variabile dinamica “non esce” dalla
procedura dov’è introdotta, posso sostituirla con una variabile locale.
Tino Cortesi
Analisi e Verifica di Programmi
27
Esiste il compilatore ottimo?
Definiamo “fully optimizing compiler” un compilatore che
trasforma un programma P nel programma Opt(P) che è il più
piccolo programma con lo stesso output di P.
Dato un programma Q che non produce nessun output e non
termina, Opt(Q) è facile da trovare: è il programma L1: goto L1;
Supponiamo di avere un fully optimizing compiler. Potremmo
usarlo per risolvere il problema della terminazione:
per vedere se esiste un input per il quale P termina, basta
vedere se Opt(P) è il programma L1: goto L1;
Ma sappiamo che il problema della terminazione è indecidibile,
ovvero che non esiste nessun algoritmo che lo risolve. Quindi
non può esistere nemmeno un fully optimizing compiler.
Tino Cortesi
Analisi e Verifica di Programmi
28
Ottimizzazione del codice
Idea: anziché chiedere al programmatore di preoccuparsi
dell’efficienza del programma, si può demandare a un
compilatore ottimizzanti la trasformazione di un codice
inefficiente in uno (equivalente) con performances migliori
Control-Flow
Analysis
Tino Cortesi
Analisi
Analisi e Verifica di Programmi
Trasformazioni
29
Trasformazioni ottimizzanti
Le trasformazioni che un compilatore ottimizzante può operare
seguono principalmente la seguente metodologia:
Analisi: attraversa il grafo di flusso del programma e
raccogli informazioni su cosa può succedere a tempo si
esecuzione
Trasformazioni: modifica il programma per renderlo in
qualche modo più veloce. L’informazione ottenuta dall’analisi
garantisce che il risultato del nuovo programma è uguale a
quello del programma originario
Tino Cortesi
Analisi e Verifica di Programmi
30
Tecniche di Analisi Statica
Per definire un’analisi statica dobbiamo preoccuparci
di:
Come specificarla
Come implementarla efficientemente
Come provarne la correttezza
Tino Cortesi
Analisi e Verifica di Programmi
31
Principali tecniche
Abstract Interpretation
Valutazione Parziale
Dataflow Analysis
Control Flow Analysis
Model Checking
Type Systems
Tino Cortesi
Analisi e Verifica di Programmi
32