Foundational
Proof-Carring Code
Andrew W.Appel
Princeton University
Relatore: Fabio Mortillaro 802657
Anno accademico 2005-06
Corso di Analisi e Verifica Programmi
Proof-Carrying code: PCC

Framework per la verifica automatica delle proprietà di
sicurezza dei programmi scritti in linguaggio macchina

Tipologie di PCC



Conventional PCC
Foundational PCC
Problema: “quis custodiet ipso custodes?”
Fabio Mortillaro 802657
2
Scopo e modalità di PCC

Eseguire solo software sicuro



Software: piccole applicazioni, plugin per browser, applet,
estensioni del kernel di OS
Sicuro: accede solo alle zone di memoria ad esso dedicate,
rispetta le variabili private delle API a cui è linkato, non accede a
risorse senza autorizzazione, non sovrascrive i valori delle
variabili, non legge dati privati
Costruire e testare dimostrazioni matematiche sul
programma scritto in LM

Garantisce sicurezza solo se non ci sono bugs nel verificationcondition generator, negli assiomi logici, nelle typing rules o nel
proof-checker
Fabio Mortillaro 802657
3
Esempi
TAL (Typed Assembly Language)
•Linguaggio assembly idealizzato su
architetture RISC
•Semantica operativa formale per una
semplice macchina astratta
 Java System:•Sistema
byte-code
fornisce
garanzia
di
di tipiverifier
formali che
catturauna
lo stato
del
lo nel
stackverifier
e la memoria
sicurezza soloregistro
se nondelciprocessore,
sono bugs
stesso,
•Importante
type-checker
per quasiotutte
le
nel compilatore
JIT, nel garbage
collector
in altre
parti
architetture Intel
della JVM
•Prototipo di compilatore per un linguaggio
imperativo sicuro

TAL: compilatore produce TAL e si effettua il typeTML (Typed Machine Language)
checking del linguaggio
a basso livello che fornisce una
•Linguaggio a più basso livello di TAL
garanzia di sicurezza
solo se
ci sono ebugs
nel
•Interfaccia
tra non
il compilatore
il prover
compilatore stesso,
nel type-checker
o nell’assembler
•Sposta
il lavoro al type-checker
che traduce TAL in ML

Semplificato in TML
Fabio Mortillaro 802657
4
Soluzione

Il provider di un programma PCC deve fornire il
codice eseguibile e la dimostrazione machinecheckable che il codice non violi la politica di
sicurezza della macchina su cui gira

Il computer non lancia il programma finché non
ha verificato che il codice sia sicuro (la
dimostrazione è valida)
Fabio Mortillaro 802657
5
TYPE SYSTEM
Conventional
PCC
Descrive come un linguaggio di
(Typed-Specialized)
programmazione classifica i valori e le



variabili in TIPI, come li può manipolare
e come
essi interagiscono
tra di loro
scritte
utilizzando
una logica
che
Dimostrazioni
ha incorporata la comprensione di un particolare
type-system
Type constructor appaiono come primitive delle
logica stessa e alcuni lemmi sono costruiti
all’interno del sistema di verifica
Semantica dei costruttori e validità dei lemmi
sono dimostrati rigorosamente dagli autori del
PCC ma non in modo meccanico
Fabio Mortillaro 802657
6
Conventional PCC: VCGen

VCGen (Verification Condition Generator): ricava
per ogni programma una verification condition
(formula logica che se vera garantisce la
sicurezza del programma)
 VCGen
usato dal provider e dal consumer per trovare
la giusta formula per il programma considerato
 VC fornita dal provider e controllata dal consumer
Fabio Mortillaro 802657
7
LOGICA di HOARE
Sistema formale che fornisce un insieme di regole
logiche al fine di motivare la correttezza di un
programma con il rigore della logica matematica
Conventional PCC: VCGen
TRIPLA di HOARE
 Programma
grosso
CedilladiSystems
Descrive
come(es:
l’esecuzione
un pezzo di è
codice
lo stato righe
della computazione
costituitocambi
da 23000
di codice C)
{P} C {Q}
 Esamina
le istruzioni macchina
del programma
P (precondizione),
C(comando),
Q (postcondizione)
 Espande le sostituzioni del codice macchina secondo
la logica di Hoare
 Esamina i parametri formali per trovare le
precondizioni e i risultati per le postcondizioni

Bug in VCGen consente a formule errate di
essere approvate
Fabio Mortillaro 802657
8
Foundational PCC




Sistema per la specifica, la dimostrazione automatica e il
controllo della sicurezza dei programmi in LM
Evita di specializzarsi per un type-system
Evita di usare un VCGen
Semantiche operazionali delle istruzioni macchina e
politiche di sicurezza definite in una logica
sufficientemente espressiva da servire da fondamento
alla matematica

Logica di alto livello con pochi assiomi dell’aritmetica, da cui è
possibile costruire la maggior parte della matematica moderna
Fabio Mortillaro 802657
9
Foundational PCC

Provider deve fornire il codice e una dimostrazione in
foundational logic che il codice soddisfi la politica di
sicurezza del consumer



Dimostrazione deve definire in modo esplicito, con i fondamenti
di matematica, tutti i concetti richiesti e provare in modo esplicito
tutte le loro proprietà
Dimostrazione della correttezza rispetto ai tipi inserita nella
dimostrazione della sicurezza del codice
Vantaggi rispetto Conventional PCC:


Flessibilità: provider può inserire un nuovo type-system o una
nuova politica di sicurezza
Sicurezza: base da verificare è minore (sistema è più piccolo
con logica di alto livello, definizione delle semantiche delle
istruzioni macchina e politica di sicurezza)
Fabio Mortillaro 802657
10
Foundational PCC
1.
2.
3.
4.
Scelta della logica e del framework
Specifica delle istruzioni macchina
Definizione della sicurezza
Dimostrazione della sicurezza




5.
Typing rules
Modelli semantici
Modelli indicizzati per i tipi ricorsivi
Mutable fields
Pruning del runtime system
Fabio Mortillaro 802657
11
1 - Logica e Framework
LF (Logical Framework)
Metalinguaggio per la specifica di sistemi deduttivi
rappresentati attraverso la dichiarazioni di costanti. È
una teoria dei tipi definita su tre livelli: oggetti, tipi e
generi di alto livello di Church con assiomi
 Logica
di aritmetica
TWELF
Versione
corrente di una attraverso
serie di implementazioni
 Rappresentata
la metalogica
del framework logico LF. Twelf è un software di
che produce in modo naturale delle
ricerca
LF
dimostrazioni inviabili al consumer

Framework TWELF
Fabio Mortillaro 802657
12
TWELF
1/2
tp : type
tm : tp -> type
o: tp
num: tp
arrow
%tipi della logica
%tipo metalogico di tipo type
%proposizioni (primitive di tp)
%numeri (primitive di tp)
%costruttori di tipi funzione
pf
%data una formula A, la sua
%dimostrazione appartiene a pf(A)
lam
@
imp
forall
%costruttore di funzioni
%applico una funzione ad un argomento
%implicazione logica
%quantificatore universale
Fabio Mortillaro 802657
13
TWELF
2/2
Regole di introduzione e di eliminazione per
i costruttori
beta_e
forall_i
beta_i
forall_e
imp_i
not_not_e
imp_e
Lemmi e nuovi operatori
and
and_i
and_e1
Fabio Mortillaro 802657
14
2 – Istruzioni macchina

Machine state: coppia
(r,m) costituita da:
 Register
r
 Memory m

Relazione da interi
(indirizzi) a interi
(contenuti)
Fabio Mortillaro 802657
15
Istruzioni


1/2
Machine step = esecuzione di un’istruzione
Esecuzione = (r , m)  (r ' , m' )
 Descrive
la relazione tra lo stato della macchina
prima e dopo l’esecuzione
Fabio Mortillaro 802657
16
Istruzioni

2/2
Considero l’istruzione r (1)  r (2)  r (3)
 Descritta
da
( r , m)  ( r ' , m' ) 
r ' (1)  r (2)  r (3)  (x  1.r ' ( x)  r ( x))  m'  m
 Da
cui è possibile definire add(i,j,k)
add (i, j , k ) 
r , m, r ' , m'.r ' (i )  r ( j )  r (k )
 (x  i.r ' ( x)  r ( x))  m'  m
Fabio Mortillaro 802657
17
Instruction fetch e decoding

1/2
Supponiamo di codificare l’istruzione add in una
word a 32 bit con opcode = 3
decode( w, instr ) 
(i, j , k
0  i  25  0  j  25  0  k  2 5 
w  3  226  i  221  j  216  k  20 
instr  add (i, j , k )
 ...
Fabio Mortillaro 802657
18
Instruction fetch e decoding
2/2
SLED
(Specification Language for Encoding and Decoding)
•Descrive
le rappresentazioni
di istruzioni
macchina
 Macchine
reali non usano
l’aritmetica
degli interi ma
in linguaggio
assembly
quella modulare
•Usa
fields emacchine
tokens (parti
di istr),
 Alcune
hanno
PCpatterns
multipli (Sparc)
(rappresentazioni binarie di istr o gruppi di istr),
 Alcune macchine hanno istruzioni di lunghezza variabile
constructors (mapping tra livello astratto e binario)
(Pentium)
•Supporta implementazioni di elementi a livello
macchina in modo indipendente dalla macchina

Tutte le istruzioni non definite vengono trattate come
illegali in base alla politica di sicurezza

Parte sintattica: relazione decode


1035 (600) linee di logica Twelf (da 151 linee di specifiche SLED)
Parte semantica: definizione di add,..

600 linee di logica (compresa definizione di logica modulare)
Fabio Mortillaro 802657
19
3 – Definizione della sicurezza
Situazione: alcuni stati non hanno
successore e r(PC) punta a istruzioni
illegali (violano politica di sicurezza)
 Esempio: “solo gli indirizzi readable
saranno caricati”

 Definisco
il predicato readable
readable ( x)  0  x  1000
Fabio Mortillaro 802657
20
Esempio

1/3
L’istruzione load (i, j, c) 
r , m, r ' , m'.r ' (i )  m(r ( j )  c)
 (x  i.r ' ( x)  r ( x))  m'  m
diviene load (i, j, c) 
r , m, r ' , m'.r ' (i )  m(r ( j )  c)
 readable (r ( j )  c)
 (x  i.r ' ( x)  r ( x))  m'  m
Fabio Mortillaro 802657
21
Esempio

2/3
Stato è sicuro se ogni stato raggiungibile nella
sua chiusura di Kleene ha un successore
safe  state(r , m) 
r ' , m'.(r , m  r ' , m' )  r" , m". r ' , m'  r" , m"

Un programma p è caricato in un punto start
della memoria m se
loaded ( p, m, start )  i  dom( p).m( start  i )  p(i )
Fabio Mortillaro 802657
22
Esempio

3/3
Un programma p è sicuro se
safe( p) 
r , m, start.loaded ( p, m, start )  r ( PC )  start 
safe  state(r , m)

OSS: non c’è VCGen e la sintassi e la
semantica in esso implicite sono rese esplicite e
più concise
Fabio Mortillaro 802657
23
4 – Dimostrazione della
sicurezza

Per produrre dimostrazioni in modo automatico
servono:
 Typed Intermediate Languages
 Typed Assembly Language

Dimostrazioni per induzione strutturale in ogni
punto del programma per dimostrare che è
sicuro
 CPCC: dimostrazioni fatte dai fornitori
 FPCC: dimostrazione della correttezza
dei tipi inserita
nella dimostrazione spedita al consumer
Fabio Mortillaro 802657
24
Compilatori diversi
Fabio Mortillaro 802657
25
Typing rules

Approccio sintattico (definizione di |- )
m |  x :  1  2
Lemma
m | msemantico
( x) :  1 che
m(deve
x  1essere
) :  2 dimostrato:
dimostrazioni semantiche sono preferibili alle
riduzioni sintattiche perché esse portano a
 Approccio
(lemma
1semantico
nella
Se x ha tipodimostrazioni
memoria
allora il da
contenuto
2
più cortem
e maneggevoli
in

della locazione
di memoria
x ha tipo
1
Foundational
Logic
dimostrare)
e quello della locazione di memoria x+1 ha tipo  2
| x :m  1  2
| m( x) :m  1  m( x  1) :m  2
Fabio Mortillaro 802657
26
Modelli semantici

Type: insieme di values
 Lambda

calcolo: costrutto sintattico
Value: coppia (m,x) dove m è la memoria
e x un intero (indirizzo)
 Per
puntatori a strutture dati, x è il root-pointer
della struttura
 Per le funzioni, x è l’entry address della f
Fabio Mortillaro 802657
27
VALUE ((a,m),x)
Coppia costituita da uno State (a,m) e da un
root-pointer x
Modelli semantici
STATE (a,m)
Coppia costituita da un allocset a e dal
contenuto della memoria m
Modello buono per strutture dati allocate staticamente
Fabio Mortillaro 802657
28
Modelli semantici - Limitazioni

Problemi:
 ricorsione
 heap

(mutable fields)
Soluzioni:
 Modello
indicizzato
 Mutable fields
Fabio Mortillaro 802657
29
Modello indicizzato

Value: coppia k, v dove k è un indice di
approssimazione e v è un valore
 k, v  significa che v approssimativamente
ha tipo  e tutti i programmi che eseguono
per meno di k istruzioni non notano diversità

Tipo: insieme di coppie k, v dove k è un
intero non negativo, v è un valore e  è
tale che se k, v  e 0  j  k allora j, v 
Fabio Mortillaro 802657
30
Mutable fields

Immutable fields


State: coppia (a,m) dove m è la memoria e a è un insieme di indirizzi allocati
Mutable fields


State: coppia (a,m) dove m è la memoria e a è una mappa da indirizzi a tipi
Definizione metalogica di tipo:
allocset  num  type
value  allocset  memory  num
fin
type  num  value  o
Problema: ricorsione
 Soluzione: sostituire il tipo nell’allocset col suo numero di Godel
Fabio Mortillaro 802657
31
Livelli di astrazione di
un’istruzione
1.
2.
3.
4.
5.
6.
1/2
Intero (codice opcode 3 per l’add)
Implementa una relazione sugli stati ( r , m)  ( r ' , m' )
Livello di astrazione usato in modo
Istruzione
add (es
Sparc) implementa
implicito
daldiConventional
Proof- una add
indipendente
dalla
macchina
Carrying
Code
Add manipola non solo i registri ma delle variabili locali
Add è una delle numerose istruzioni tipate che
lavorano sui tipi (int  int  int)
Add tipata viene specializzata per un particolare
contesto dove appaiono alcune sue istanze
Fabio Mortillaro 802657
32
Livelli di astrazione di
un’istruzione
2/2
FPCC ricerca e tenta di trovare modelli
semantici per ciascuno dei livelli di
astrazione in modo da poter dimostrare
lemmi che consentano il passaggio da un
livello all’altro
 Livelli di astrazione definiti per
modularizzare le dimostrazioni in modo da
semplificare il lavoro del prover

Fabio Mortillaro 802657
33
5 - Pruning del Runtime System
Problemi: bugs del garbage collector,
debugger, mashaller/unmarshaller,…
 Soluzione: portare le componenti dal
runtime system al codice utente typecheckable

 Bugs
individuati dal type-checking
 Type-safe Bugs che portano a
comportamento non corretto ma sicuro
Fabio Mortillaro 802657
34
Garbage collector

Problemi:
 Alloca
e dealloca
di memoria
con oggetti
Regionaree
calculus
di Tofte e Talpin
Lambda
calcolo tipato in modo polimorfico con
di tipo
diverso
Intensional
Type Analysis
annotazioni che
rendono esplicita
l’allocazione e la
 Attraversa
tipo
sconosciuto
in liberati
modo
Utilizzo
dioggetti
linguaggi
che
consentono
il polimorfismo
deallocazione
delladi
memoria.
Possono
essere
ad
hoc,
l’analisi
tipi a runtime
e la morti
definizione di
arbitrario
solo
oggetti
che dei
probabilmente
sono
operatori che determinino la struttura di un abstract
 Soluzioni:
type
 Region
calculus di Tofte e Talpin
 Intesional type analysis
Fabio Mortillaro 802657
35
Conclusioni

Sfrutta il lavoro di molti





Logical framework (teoria e implementazione)
Prover automatici
Type theory e type system
Verifica partendo dall’insieme di assiomi più piccolo
possibile, usando il più piccolo e semplice verifier e
runtime system
Riduzione della costo di computazione dei sistemi
che fanno girare codice macchina da risorse non
sicure
Fabio Mortillaro 802657
36