Date post: | 01-May-2015 |
Category: |
Documents |
Upload: | allegra-riccio |
View: | 213 times |
Download: | 1 times |
FoundationalProof-Carring Code
Andrew W.AppelPrinceton University
Relatore: Fabio Mortillaro 802657Anno accademico 2005-06
Corso di Analisi e Verifica Programmi
Fabio Mortillaro 802657 2
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 3
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 verification-
condition generator, negli assiomi logici, nelle typing rules o nel proof-checker
Fabio Mortillaro 802657 4
Esempi
Java System: byte-code verifier fornisce una garanzia di sicurezza solo se non ci sono bugs nel verifier stesso, nel compilatore JIT, nel garbage collector o in altre parti della JVM
TAL: compilatore produce TAL e si effettua il type-checking del linguaggio a basso livello che fornisce una garanzia di sicurezza solo se non ci sono bugs nel compilatore stesso, nel type-checker o nell’assembler che traduce TAL in ML Semplificato in TML
TAL (Typed Assembly Language)•Linguaggio assembly idealizzato su architetture RISC•Semantica operativa formale per una semplice macchina astratta•Sistema di tipi formali che cattura lo stato del registro del processore, lo stack e la memoria•Importante type-checker per quasi tutte le architetture Intel•Prototipo di compilatore per un linguaggio imperativo sicuro
TML (Typed Machine Language)•Linguaggio a più basso livello di TAL•Interfaccia tra il compilatore e il prover•Sposta il lavoro al type-checker
Fabio Mortillaro 802657 5
Soluzione
Il provider di un programma PCC deve fornire il codice eseguibile e la dimostrazione machine-checkable 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 6
Conventional PCC (Typed-Specialized)
Dimostrazioni scritte utilizzando una logica che 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
TYPE SYSTEMDescrive come un linguaggio di programmazione classifica i valori e le variabili in TIPI, come li può manipolare e come essi interagiscono tra di loro
Fabio Mortillaro 802657 7
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 8
Conventional PCC: VCGen
Programma grosso (es: Cedilla Systems è costituito da 23000 righe di codice C) Esamina le istruzioni macchina del programma 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
LOGICA di HOARESistema formale che fornisce un insieme di regole logiche al fine di motivare la correttezza di un programma con il rigore della logica matematica
TRIPLA di HOAREDescrive come l’esecuzione di un pezzo di codice cambi lo stato della computazione
{P} C {Q}P (precondizione), C(comando), Q (postcondizione)
Fabio Mortillaro 802657 9
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 10
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 11
Foundational PCC
1. Scelta della logica e del framework2. Specifica delle istruzioni macchina3. Definizione della sicurezza4. Dimostrazione della sicurezza
Typing rules Modelli semantici Modelli indicizzati per i tipi ricorsivi Mutable fields
5. Pruning del runtime system
Fabio Mortillaro 802657 12
1 - Logica e Framework
Logica di alto livello di Church con assiomi di aritmeticaRappresentata attraverso la metalogica LF
che produce in modo naturale delle dimostrazioni inviabili al consumer
Framework TWELF
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
TWELFVersione corrente di una serie di implementazioni del framework logico LF. Twelf è un software di ricerca
Fabio Mortillaro 802657 13
TWELF 1/2
tp : type %tipi della logicatm : tp -> type %tipo metalogico di tipo typeo: tp %proposizioni (primitive di tp)num: tp %numeri (primitive di tp)arrow %costruttori di tipi funzione
pf %data una formula A, la sua %dimostrazione appartiene a pf(A)
lam %costruttore di funzioni@ %applico una funzione ad un
argomentoimp %implicazione logicaforall %quantificatore universale
Fabio Mortillaro 802657 14
TWELF 2/2
Regole di introduzione e di eliminazione per i costruttori
beta_e beta_i imp_i imp_e
forall_i forall_e not_not_e
Lemmi e nuovi operatori
and and_i and_e1
Fabio Mortillaro 802657 15
2 – Istruzioni macchina
Machine state: coppia (r,m) costituita da: Register r Memory m
Relazione da interi (indirizzi) a interi (contenuti)
Fabio Mortillaro 802657 16
Istruzioni 1/2
Machine step = esecuzione di un’istruzione Esecuzione =
Descrive la relazione tra lo stato della macchina prima e dopo l’esecuzione
)','(),( mrmr
Fabio Mortillaro 802657 17
Istruzioni 2/2
Considero l’istruzioneDescritta da
Da cui è possibile definire add(i,j,k)
)3()2()1( rrr
mmxrxrxrrr
mrmr
'))()('.1()3()2()1('
)','(),(
),,( kjiadd)()()(''.,',, krjrirmrmr mmxrxrix '))()('.(
Fabio Mortillaro 802657 18
Instruction fetch e decoding 1/2
Supponiamo di codificare l’istruzione add in una word a 32 bit con opcode = 3
),( instrwdecodekji ,,(
555 202020 kji 0162126 22223 kjiw
),,( kjiaddinstr ...
Fabio Mortillaro 802657 19
Instruction fetch e decoding 2/2
Macchine reali non usano l’aritmetica degli interi ma quella modulare
Alcune macchine hanno PC multipli (Sparc) Alcune macchine hanno istruzioni di lunghezza variabile
(Pentium)
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)
SLED(Specification Language for Encoding and
Decoding)•Descrive le rappresentazioni di istruzioni macchina in linguaggio assembly•Usa fields e tokens (parti di istr), patterns (rappresentazioni binarie di istr o gruppi di istr), constructors (mapping tra livello astratto e binario)•Supporta implementazioni di elementi a livello macchina in modo indipendente dalla macchina
Fabio Mortillaro 802657 20
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
10000)( xxreadable
Fabio Mortillaro 802657 21
Esempio 1/3
L’istruzione
diviene
),,( cjiload))(()(''.,',, cjrmirmrmr mmxrxrix '))()('.(
),,( cjiload))(()(''.,',, cjrmirmrmr
))(( cjrreadable mmxrxrix '))()('.(
Fabio Mortillaro 802657 22
Esempio 2/3
Stato è sicuro se ogni stato raggiungibile nella sua chiusura di Kleene ha un successore
Un programma p è caricato in un punto start della memoria m se
),( mrstatesafe","','".,")',','.(,' mrmrmrmrmrmr
)()().(),,( ipistartmpdomistartmploaded
Fabio Mortillaro 802657 23
Esempio 3/3
Un programma p è sicuro se
OSS: non c’è VCGen e la sintassi e la semantica in esso implicite sono rese esplicite e più concise
)( psafe
startPCrstartmploadedstartmr )(),,(.,,),( mrstatesafe
Fabio Mortillaro 802657 24
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 25
Compilatori diversi
Fabio Mortillaro 802657 26
Typing rules
Approccio sintattico (definizione di |- )
Approccio semantico (lemma da dimostrare)
21
21
:)1(:)(|
:|
xmxmm
xm
21
21
:)1(:)(|
:|
mm
m
xmxm
x
Se x ha tipo nella memoria m allora il contenuto della locazione di memoria x ha tipo e quello della locazione di memoria x+1 ha tipo
21 12
Lemma semantico che deve essere dimostrato: dimostrazioni semantiche sono preferibili alle riduzioni sintattiche perché esse portano a dimostrazioni più corte e maneggevoli in Foundational Logic
Fabio Mortillaro 802657 27
Modelli semantici
Type: insieme di valuesLambda 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 strutturaPer le funzioni, x è l’entry address della f
Fabio Mortillaro 802657 28
Modelli semantici
Modello buono per strutture dati allocate staticamente
VALUE ((a,m),x)Coppia costituita da uno State (a,m) e da un root-pointer x
STATE (a,m)Coppia costituita da un allocset a e dal contenuto della memoria m
Fabio Mortillaro 802657 29
Modelli semantici - Limitazioni
Problemi:ricorsioneheap (mutable fields)
Soluzioni:Modello indicizzatoMutable fields
Fabio Mortillaro 802657 30
Modello indicizzato
Value: coppia dove k è un indice di approssimazione e v è un valore significa che v
approssimativamente ha tipo e tutti i programmi che eseguono per meno di k istruzioni non notano diversità
Tipo: insieme di coppie dove k è un intero non negativo, v è un valore e è tale che se e allora
vk,
vk,
vk,
vk, kj 0 vj,
Fabio Mortillaro 802657 31
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:
Problema: ricorsione Soluzione: sostituire il tipo nell’allocset col suo numero di Godel
typenumallocset finnummemoryallocsetvalue
ovaluenumtype
Fabio Mortillaro 802657 32
Livelli di astrazione di un’istruzione 1/21. Intero (codice opcode 3 per l’add)2. Implementa una relazione sugli stati3. Istruzione add (es di Sparc) implementa una add
indipendente dalla macchina4. Add manipola non solo i registri ma delle variabili locali5. Add è una delle numerose istruzioni tipate che
lavorano sui tipi6. Add tipata viene specializzata per un particolare
contesto dove appaiono alcune sue istanze
)','(),( mrmr
int)int(int
Livello di astrazione usato in modo implicito dal Conventional Proof-Carrying Code
Fabio Mortillaro 802657 33
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 34
5 - Pruning del Runtime System
Problemi: bugs del garbage collector, debugger, mashaller/unmarshaller,…
Soluzione: portare le componenti dal runtime system al codice utente type-checkableBugs individuati dal type-checkingType-safe Bugs che portano a
comportamento non corretto ma sicuro
Fabio Mortillaro 802657 35
Garbage collector
Problemi:Alloca e dealloca aree di memoria con oggetti
di tipo diversoAttraversa oggetti di tipo sconosciuto in modo
arbitrario Soluzioni:
Region calculus di Tofte e Talpin Intesional type analysis
Region calculus di Tofte e TalpinLambda calcolo tipato in modo polimorfico con annotazioni che rendono esplicita l’allocazione e la deallocazione della memoria. Possono essere liberati solo oggetti che probabilmente sono morti
Intensional Type AnalysisUtilizzo di linguaggi che consentono il polimorfismo ad hoc, l’analisi dei tipi a runtime e la definizione di operatori che determinino la struttura di un abstract type
Fabio Mortillaro 802657 36
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