Checking Security of Java Bytecode by Abstract Interpretation R. Barbuti - C. Bernardeschi - N. De...

Checking Security of Java Bytecode by Abstract Interpretation

R. Barbuti - C. Bernardeschi - N. De Francesco

Corso di Analisi e Verifica dei Programmi

Carnielli Efrem 804207 Terenzoni Alessandro 804545

Sommario

• Introduzione

• Il linguaggio JVML (ossia JVML0)

• La semantica operazionale di JVML

• Il modello per definire “sicuro” di JVML

• La semantica concreta di JVML

• La semantica astratta di JVML

• Considerazioni finali e sviluppi innerenti

Introduzione

• Si presenta un metodo per certificare come sicuro un sottoinsieme di comandi di Java Bytecode.

• Un metodo basato sulla interpretazione astratta della semantica operazionale del linguaggio.

Perché è importante che sia sicuro Java Bytecode?(1)

Java Virtual Machine Bytecode Language (JVML) può essere scaricato da internet ed eseguito da un browser Java-compatibile.

L’esecuzione del codice scaricato:

- può richiedere l’accesso ai dati privati dell’utente;

- può aver bisogno di informazioni in Internet che compromettono la riservatezza dei dati privati dell’utente.

Perché è importante che sia sicuro Java Bytecode? (2)

Quindi bisogna garantire la sicurezza dei dati privati dell’utente in ogni forma di possibile utilizzo.

Perché è importante che sia sicuro Java Bytecode? (3)

Alternativa possibile:

l’utente potrebbe fare la scelta di vietare che del codice possa accedere ai suoi dati personali, ma ciò comporterebbe la possibilità che il codice non verrebbe più eseguito correttamente.

Informazione sicura

• In base alla proprietà che riguarda il flusso sicuro di informazione (secure information flow property)

si ha

che l’informazione con un dato livello di sicurezza (security level) non può essere utilizzata a un livello di sicurezza più basso.

Flusso sicuro

Dato un programma in linguaggio ad alto livello nel quale ogni variabile è considerata sicura (security level) si ha un flusso sicuro (secure flow) dell’informazione se, alla terminazione del programma, il valore di ogni variabile al livello più basso non dipende dal valore della variabile con livello di sicurezza più alto.

Esempio

Supponiamo che la variabile y ha un livello di sicurezza più alto della variabile x se scrivo:

x:= y oppure if y=0 then x:=1 else x:=0

Si nota come alla fine dell’esecuzione del codice il valore di x “rivela” il valore della variabile y, variabile con un livello di sicurezza più alto di x.

Falla nella sicurezza

Possibile falla nella sicurezza (security leakage) che potrebbe accadere nei linguaggi ad alto livello si ha quando l’informazione sicura (security level) viene rivelato il suo valore con il comportamento del programma eseguito.

Esempio

while (y>0) do skip

Se programma non termina per loop-infinito si capisce che la variabile y definita con alto livello di sicurezza, è maggiore di zero.

JVML

• Il linguaggio assembly utilizza uno stack.

• L’articolo considera un sottoinsieme del linguaggio.

• Definiremo una semantica estesa a piccoli passi del linguaggio considerando principalmente l’influenza che ha il flusso di informazione sullo stack.

Flusso di informazione

Considerando il flusso di informazioni anche in un codice assembly bisogna tener conto del:

- flusso di informazione esplicito

- flusso di informazione implicito

Flusso di informazione esplicito

Nel linguaggio ad alto livello si ha quando viene fatto un assegnamento. Esempio x:=y

Il livello di sicurezza può essere definito dall’espressione nella parte destra dell’assegnamento.

Nel codice assembly essendo il valore messo come push nello stack, una istruzione di pop non mostra la sorgente del valore.

Flusso di informazione implicito

Nel linguaggio ad alto livello l’ambiente (scope) del flusso di informazione implicito può essere visto su comandi condizionali o comandi iterativi coincidente con l’ambiente del comando stesso.

Esempio if y=0 the x:=1 else x:=0 Il linguaggio assembly non è strutturato. Lo stack

può essere influenzato da un flusso implicito perché lo stack può essere manipolato in modi diversi attraverso i rami di una istruzione condizionale oppure può eseguire un diverso numero di operazioni push e pop in ordine differente.

Stato della macchina

In JVML si deve parlare anche di stato della macchina.

Il linguaggio assembly definisce una macchina astratta nel quale il programma eseguito può modificare lo stato della macchina che a sua volta può causare una modifica nel livello di sicurezza dell’informazione: ad esempio il contenuto del program counter quando il programma termina.

Il linguaggio JVML0

cima.in elementol’ è 1 non vuotostack uno è se

che econvenzion lacon sequenze comestack lo oIndicherem

se cioè di

elemento esimo-il’ indichiamo con },#,,1{ Se

1

]w[w

w, w[i] w www

w[i]wi

in

Il linguaggio JVML0

In JVML0 si ha un operand stack, una memoria contenente:

le variabili locali,

istruzioni aritmetiche semplici,

salti condizionali e non condizionali

Insieme di istruzioni JVML0

• op dove op {add, sub, …}

Estrae due operandi dallo stack, esegue

l’ operazione e mette il risultato nello stack• pop estrae il valore in cima allo stack• push k mette una costante k sullo stack• load x mette il valore della variabile x nello stack• store x estrae dallo stack e mette il valore nella

variabile x


• if j estrae il valore dalla cima dallo stack e salta a j se non-zero

• goto j salta a j• jsr j all’indirizzo p, salta all’indirizzo j e ritorna

all’indirizzo p+1 messo nell’operand stack• ret x salta all’indirizzo della variabile x• halt istruzione di terminazione del programma


• Un programma è una sequenza c di istruzioni, numerate partendo dall’indirizzo 1.

• Per ogni i {1,…,#c}, c[i] è l’istruzione all’indirizzo i

• Noi assumiamo che il programma rispetti i seguenti vincoli statici, generalmente verificabili da un verificatore di codice: non si presenta nessun stack overflow o underflow, l’esecuzione non salta ad un indirizzo indefinito.


• Data una sequenza di istruzioni c, denoteremo con Var(c) il nome delle variabili che occorrono in c.

Semantica operazionale di JVML0

• La semantica operazionale descrive il significato di un linguaggio di programmazione specificando come il programma viene eseguito su una macchina astratta.


• La semantica sarà data in termini di sistema di transizioni, dove il

- cammino rappresenta la traccia di esecuzione e dove

- i nodi mostrano che il programma cambia stato


. che taleesistenessun sse

) da (denotato ne transiziodi sistema del finale stato uno è che Diremo

. di a transitive riflessiva chiusura la con Denoteremo

. scriveremo solito di , ),( sse ' a da ne transiziouna èc’ che Diremo

ne. transiziodi relazione la è di mesottoinsie è e iniziale stato lo è

stati, di insiemeun è dove , ),,( triplauna è ni transiziodi sistemaUn

*

0

0

sss

Ss

ssssss

SSs

SsST


La semantica standard del linguaggio definisce un insieme di regole …

sxkmisi,m,k

xic

skmii,m,s

kxmxic

skmii,m,s

kic

smisi,m,k

ic

skopkmiski,m,k

ic

e

e

e

e

e

],/[,1

store][ store

,,1

)( load][ load

,,1

push ][push

,,1

pop][ pop

)(,,1

op][ op

2121



smxmi,m,s

xic

simji,m,s

jic

smji,m,s

jic

smjsi,m,k

jic

smisi,m,

jic

e

e

e

e

e

,),(

ret ][ret

)1(,,

jsr ][jsr

,,

goto][ goto

,,0

if][ if

,,10

if][ if

true

false


.in ememorizzat variabilile cioè , di dominio il

var,di mesottoinsie )D(con denoteremo noi , memoria una data , seguito Nel

,, stack, dello )(su sequenze (finite )( dominioUn

,,, valori,a variabile

di toriidentifica da ionememorizzaz di var : funzioni di dominioUn

,, indirizzi, che dati sia

includono che , , , , costanti valoridi dominioun usa semantica La

1*

1

21

mm

mm

,sssVVS

mmm

VM

ji

kkkV

eee

ee

e


stack. operand dell’

stato corrente il è ed locali variabilidelle stato corrente il

arappresent che memoria la è counter, program nel indirizzol’

è dove ),,( upla,- una esegue programma del stati a modello Il

s

m

ismit


. quale nella per che tranne variabilile per tutte

ad uguale è quale la memoria la indicare ad serve notazione La

. di mesottoinsie relazione una definisce standard semantica della regole Le

stati. degli dominio il con Denoteremo

o.stack vuot operandcon e

1 istruzionedall’ partendo eseguito sempre è programma il che Assumeremo

e

k(x)mx

mmm[k/x]

CC

C

]c[

ee

e


o.stack vuot operandun e memoria data una , istruzione prima della

indirizzodell' consiste iniziale stato lo dove ,,1,,( come

definito ni transiziodi sistema è programmaun di standard semantica la

, a teappartenen memoria una e programmaun Dato

e ),m(C

Mmc

e

e

programma. del one terminazialla

vuotosiastack operandl’ che richiesto Non viene . e qualcheper

halt,con ,, forma la ha e unico è esiste se finale, stato Lo

cammino. infinito, possibile un, solo ha itransazion

di sistema entecorrispond il tico,determinis è programma il che Dato

ms

c[i]smi

Grafo del flusso di controllo (1)

Dato un programma c composto di n istruzioni (#c=n), grafo di flusso di controllo di un programma è un grafo diretto (V,E) dove V={1,…,n+1} è un insieme di nodi e E sottoinsieme VV contiene gli archi (i,j) sse l’istruzione all’indirizzo j può essere immediatamente eseguita dopo quella all’indirizzo i, in più contiene l’arco (i,n+1) per ogni indirizzo i tale che c[i]=halt.

Grafo del flusso di controllo (2) Siano i e j nodi di grafo di flusso di controllo di un

programma con n istruzioni. Diremo che il nodo j prevale su (postdominates) i,

denotato da j pd i, se ji e j è in ogni cammino che parte da i.

Diremo che il nodo j prevale immediatamente (immediate postdominates) i, denotato da j ipd i, se j pd i e non c’è nessun nodo r tale

che j pd r pd i. Useremo la notazione j=ipd(i). Per ogni nodo i n+1 tale che ipd(i) non esiste,

scriveremo ipd(i)=n+1.

Esempio

3 load y

5 pop

6 store x

7 halt

4 if 6

2 push 01 push 1

j=ipd(i)

1 push 1

2 push 0

3 load y

4 if 6

5 pop

6 store x

7 halt

i

Il modello per definire “sicuro” JVML0(1)

• Assumiamo un reticolo finito (L,) dove L è un insieme di livelli di sicurezza, σ,τ … secondo un ordinamento parziale .

• Dati σ,τ L, στ indica il least upper bound di σ e di τ.

• στ significa che σ τ e σ τ.

Il modello per definire “sicuro” JVML0(2)

• Nel modello di sicurezza di JVML0 noi considereremo di annotare il programma dove ad ogni variabile verrà associato un livello di sicurezza.

• Un programma è una coppia (c,Λ) dove c è una sequenza di istruzioni e Λ è una partizione delle variabili in Var(c).

Il modello per definire “sicuro” di JVML0(3)

. variabilialtre le con e

livellocon di variabilile con

indichiamo , e ) (c, programmaun Dato

. sicurezza di livellocon variabilidi insiemeun

è )(: ogniper dove }|{

P

LP

cVarLL


segreta. tenutaè

sicurezza di livello ilcon neinformaziol’ che

fatto il descrive e sicurezza di livello a rispetto

aparametric è sicurezza,– con indicata introdurre

di intenzione ha si che sicurezza di nozione La

σ


programma. del one terminazisulla

neosservaziodall' scoperta non venga sicurezza di

altopiù livello al neinformaziol' che garantito è

piùIn eseguita. istruzione ultimadell' indirizzol'

esaminando ostack operanddell' elementi gli

esaminando macchina della stato dallo recuperata

essere puònon valorinesu taliinformaziol'

e in variabilidelle finale valoredal

einfluenzat sononon in variabilidelle iniziale

valoreil che assicura :(falle) leakages differenti

possibili di assenzal' garantisce sicurezza


modo. ogniin loro tra

dipendere possono in variabilile mentre

primo, il e gruppo secondo il traneinformazio

di flussoalcun èc’non che solo assicura

e ) torelated(not a relativonon oppure alto

più quello e , a uguale o minore quello :gruppi due

in sicurezza di livelli i divide sicurezza- realtàIn

. di che elevatopiù sicurezza

di livellocon variabilealtra una di valore

dal ainfluenzat sia variabileuna di finale

valoreil che escludenon sicurezza- di nozione La

x

y

x


.per sicurezza-

garantiscenon sicurezza- aconseguenz Come

Esempi di σ-non secure programs

Semantica concreta

Che cos’è : la semantica concreta non è altro che l’ estensione della semantica operazionale appena vista, in modo che possa controllare violazioni di security.

Come viene estesa:

• i valori trattati vengono arricchiti con un nuovo parametro, il livello di sicurezza. Durante la computazione di un programma il livello di sicurezza di un valore è dato dal LUB dei livelli di sicurezza dei flussi di informazione, sia esplicito che implicito, da cui il valore dipende.

• le istruzioni sono eseguite all’interno di un ambiente di sicurezza, che non è altro che un livello di sicurezza. In ogni momento dell’esecuzione, l’ambiente di sicurezza rappresenta il lub dei livelli di sicurezza del flusso implicito. L’ambiente di sicurezza può essere ”upgraded” (incrementato) da un’ istruzioni di branching (IF e RET) e può essere “downgraded” alla terminazione del flusso implicito.

Semantica concreta

Come trattare il flusso implicito

La semantica si basa sul control flow graph per manipolare il flusso implicito. Il flusso implicito di una istruzione IF o RET all’indirizzo i termina con l’istruzione all’indirizzo ipd(i). Eseguendo la IF o la RET all’interno di un ambiente sicuro (cioè un ambiente a cui è stato assegnato un livello di sicurezza ), la semantica memorizza la coppia (ipd(i), ), e l’ambiente viene upgraded per considerare:

• per la IF il livello di sicurezza della condizione, cioè il valore al top dello stack degli operandi

• per la RET X il livello di sicurezza dell’indirizzo memorizzato in x

Quando il flusso implicito termina cioè l’istruzione all’indirizzo ipd(i) è raggiunta, l’ambiente è reimpostato a , cioè al valore di sicurezza dell’ambiente in cui l’istruzione che ha generato il flusso implicito è stata eseguita.

Per modellare istruzioni di branching innestati, la semantica registra la coppia (ipd(i), )’ in uno stack, poiché, in presenza di istruzioni di branching innestati, il flusso implicito più interno termina prima.

Lo stack per contenere tali valori è chiamato ipd stack.

Semantica concreta

(k, ) è chiamato -valore e V è l’insieme di questi valori.

V = (Ve x L) è il dominio dei valori concreti indicati come v,v’,v1, …

M : var V è il dominio delle memorie concrete, indicato come M,M’,M1, … (cioè insieme delle funzioni che ad ogni variabile associano un valore)

S =V* sono gli stack degli operandi , indicati come S,S’,S1, … (sequenza finita di valori)

R = (N x L)* indicati come ’Sono ipd stack.

Le regole della semantica operazionale sono evidenziate nella slide successiva. Tali regole

definiscono una relazione di transizione C x C , dove C è l’insieme degli stati concreti.

vdi sicurezza di livello il indica L •

numerica parte la èk costanti), delle (insieme V k • e

Introduciamo i domini della semantica concreta:

I valori diventano coppie v = (k, )

concret operandi deglistack lo arappresent S $ S , concreta memoria la è M $ M counter, program del contenuto il è c}#,{1, $ i ambiente,l’ è sigma :dove rS,M,i,G sigma struttura la ha stato Ogni

stack.-ipd l’ è R e concreto operandi

deglistack lo arappresent S S , concreta memoria la è M counter, program del contenuto

il è c}#,{1, i ambiente,l’ è :dove rS,M,i, struttura la ha stato Ogni

M

) variabilidi insieme(un M di dominio il indica D(M) , M dato M

Regole della semantica concreta

Semantica concreta

Le regole assicurano che tutti gli elementi presenti nello stack degli operandi abbiano livello di sicurezza maggiore o uguale al livello di sicurezza dell’ambiente. E questo per il Lemma 1 che vedremo in seguito.

Per mantenere il livello di sicurezza di un valore uguale al livello di sicurezza dell’informazione da cui dipende, la semantica modifica il livello di sicurezza di ogni valore inserito (pushed) sullo stack degli operandi, in accordo con il livello di sicurezza dell’ambiente.

Le regole

La JRS associa l’indirizzo di ritorno inserito sullo stack con il livello di sicurezza dell’ambiente.

La LOAD X assegna al valore inserito (pushed) sullo stack il LUB tra il livello di sicurezza di M(x) e l’ambiente.

La PUSH assegna alla costante k il livello di sicurezza dell’ambiente (una costante non ancora usata può essere associata al minimo livello di sicurezza).

Semantica concreta

Come già osservato un flusso implicito comincia all’esecuzione di una IF o una RET.

Le regole IF true e IF false applicate alla IF all’indirizzo i: se il valore in cima (top) allo stack degli operandi (prossimo ad essere preso in considerazione) è (k,) il ramo selezionato verrà eseguito sotto l’ambiente di con sicurezza .

Inoltre (ipd(i), ) è inserito sul top dell’ipd stack ((ipd(i), ), ), dal quale sarà ripreso alla terminazione del flusso implicito.

Assumiamo che non consenta l’inserimento di un indirizzo i sull’ipd stack se tale i è gia sulla cima dello stack. Infatti, se due o più istruzioni di branching innestate terminano allo stesso ipd, alla terminazione del flusso l’ambiente deve essere quello che era stato preso all’entrata di quello più esterno.

L’indirizzo i non deve essere nell’ipd stack

Stato di partenza, con ambiente

Stato finale con ambiente

Semantica concretaLe regole per la IF upgrade (incrementano) il livello di sicurezza di ogni valore che viene assegnato ad una variabile tramite una STORE nel più corto dei due rami:

sia W = {x | c[j] = STORE x, e j appartiene ad un cammino del grafo di controllo che comincia da i e finisce in ipd(i), escludendo ipd(i)}.

Per ogni , se M(x) = (k, ), allora upgradeM(M,i,)(x) = (k, ). Il livello di sicurezza delle variabili che non appartengono a W non è modificato dall’ upgradeM(M,i,). Fare l’upgrade della memoria in questo modo tiene in considerazione il fatto che una variabile può essere modificata in un ramo e non nell’altro.

Anche lo stack degli operandi può essere influenzato dai flussi impliciti. Le regole infatti modificano anche il livello di sicurezza di ogni valore presente nello stack degli operandi applicando la funzione upgradeS(S,): esso aumenta il valore di ogni variabile v in S al LUB di ed il livello di sicurezza attuale di v. La RET X, è trattata allo stesso modo, imposta il nuovo ambiente al LUB tra l’ambiente attuale ed il livello di sicurezza di x, e fa l’upgrade della memoria in conformità con lo stack.

Nell’upgrade dello stack degli operandi all’entrata del flusso implicito bisogna tener conto del fatto che lo stack può essere manipolato in modi diversi da rami diversi. Un ramo può eseguire un numero diverso di POP e PUSH, e con un ordine differente. Così anche elementi che non vengono usati in nessun ramo possono cambiare la loro posizione all’interno dello stack, a causa del flusso implicito. Questi elementi possono essere usati anche dopo la terminazione del flusso implicito cioè quando l’ambiente precedente è ripristinato; ma in questo modo dovrebbero tener traccia del fatto che sono influenzati dal flusso implicito. La nostra scelta è di fare l’upgrade di tutti gli elementi dello stack degli operandi all’entrata del flusso implicito.

Wx

Semantica concreta

Vediamo più chiaramente tramite un esempio:

• quando l’istruzione c[6] = STORE X viene eseguita, in cima allo stack c’è il valore 0 o 1, a seconda del ramo scelto dalla IF all’indirizzo 4 che testa il valore della y.

• l’istruzione c[6] non appartiene allo scope del flusso implicito di valore piu’ alto generato dall’istruzione c[4], e così è eseguita sotto l’ambiente trattenuto prima dell’entrata nel flusso implicito che ha valore piu’ basso.

• in questo modo il flusso viene individuato come non sicuro tramite l’upgrade dello stack degli operandi, all’entrata del flusso implicito, che causa l’assegnamento di un valore elevato a x dall’istruzione c[6].

E’ NECESSARIO FARE L’UPGRADE DELLO STACK !

Semantica concreta

La regola dell’IPD, unica nuova regola, aggiorna l’ambiente di sicurezza quando il flusso implicito termina, cioè quando l’istruzione che è ipd di una istruzione di branching eseguita precedentemente è raggiunta. La regola è applicata solo se il contenuto del program counter è presente sulla cima di cioè se il contenuto del program counter è i e iper qualcheLa regola non cambia il program counter, ma modifica solo l’ambiente, che è impostato a

Dato un programma P = (ce una memoria M, la semantica concreta di P è il sistema di transizione C(P,M) = (C,, ) dove è il più basso livello di sicurezza, lo stato iniziale consiste nell’indirizzo della prima istruzione, la memoria è quella data, lo stack degli operandi è vuoto () e l’ipd stack anch’esso vuoto( ).

Nota che, se ignoriamo informazioni sulla sicurezza, la semantica concreta coincide con la semantica standard del linguaggio. Cosi può essere usata per eseguire il programma.

Ora passiamo a dare alcune definizioni e risultati. Introdurremo alcune definizioni e dei teoremi che ci permettono di affermare che la tecnica che stiamo utilizzando è corretta.

M ,M,1, 0

. a uguale o inferiore sicurezza di livellocon )(i, coppia la indichiamo } :){(i, RCon

VV anche Usiamo

. a inferiore o uguale livello di sicurezzacon valoreil indichiamo V U VCon

Semantica concreta

Tale lemma assicura, come era stato accennato prima, che in ogni stato con ambiente di sicurezza gli elementi nello stack degli operandi hanno livello di sicurezza maggiore o uguale a , mentre gli elementi nell’ipd stack hanno livello di sicurezza minore o uguale a e sono ordinati in maniera decrescente rispetto la sicurezza da top a bottom.

Definiamo la nozione di safeness.

• una memoria è -safe per P se ogni variabile associata in P con un livello di sicurezza minore o uguale a , mantiene in M un livello di sicurezza minore o uguale a .

• uno stack degli operandi è -safe per P se contiene solo valori con livello di sicurezza minore o uguale a .

Il seguente lemma esprime qualche proprietà della semantica concreta riguardante lo stack degli operandi e l’ ipd stack.

Lemma 1. Dato P=<c,> e ),MC(P, a teappartenen S,M,i, stato ogniin M 00 M,

R 1][i implica),(][:1-#1,..., i 3.

* )(R 2.

*)(V S .1

ji

Semantica concreta

Definizione 5. Dato P=<c,>

una memoria concreta M con D(M) = Var(c) è -safe per P se e solo se per ogni x

allora

Uno stack concreto S è -safe per P se e solo se

Il seguente teorema afferma l’adeguatezza della semantica concreta per la caratterizzazione di un flusso di informazione sicuro.

Dato P=<c,> , consideriamo una memoria concreta M con D(M) = Var(c) in cui, per ogni , la variabile con livello ha -valore. Chiamiamo questa memoria – consistente.

Teorema 1. Sia P=<c,> un programma e . Se ogni esecuzione terminante di P comincia da una memoria – consistente termina con uno stato <i,M,S

tale che M e S sono -safe per P e , allora P è -sicuro.

V M(x)

*) (V S

L

L

Più formalmente …

Semantica astrattaIn questa sezione presenteremo una semantica operazionale astratta in grado di controllare la security.

Perché utilizziamo la semantica astratta:

la semantica concreta non può essere usata come mezzo per l’analisi statica di una -security, perché mostra il flusso di informazioni di una particolare esecuzione, mentre la security fa riferimento a tutte le esecuzioni.

il sistema di transizioni concrete potrebbe anche essere infinito.

lo scopo dell’interpretazione astratta (o semantica astratta) è di approssimare correttamente la semantica concreta di tutte le esecuzioni in modo finito, in maniera da essere usata per costruire uno strumento utile nella pratica.

Come otteniamo la semantica astratta: tale semantica è un’astrazione della semantica concreta presentata nella precedente sezione: i valori concreti sono astratti considerando solo il loro livello di sicurezza e tralasciando la loro parte numerica. Tutte le altre strutture sono astratte di conseguenza.

Semantica astrattaI domini astratti :

• V# = L (il nuovo dominio dei valori è il dominio delle security)

• M# = varV# (dominio delle memorie astratte)

• S# = (V#)* (operandi concreti )

Il dominio dell’ipd stack rimane invariato, gli stati astratti C#, sono analoghi a quelli concreti, ma in cui la memoria M viene sostituita con una memoria astratta M# M# e lo stack S sostituito con uno astratto S# S#.

Le funzioni astratte (associano informazioni concrete a quelle astratte):

• la funzione astratta sui valori è V: V L , tale che V((k,s)) = (k tralasciato)

• la funzione astratta sulle memorie M: M M# , tale che (M(M))(x) = V(M(x)) per ogni x D(M).

• la funzione astratta sugli stack, S: S S# , tale che (S(S))[i] = V(S[i]), per ogni i {1,…,#S}.

• la funzione astratta sugli stati, C: C C# come segue:

αS(S), , αM(M) i, σ ) S,M,i, (σ C

Semantica astrattaLe regole della semantica concreta vengono ridefinite sui nuovi domini.

Le regole di IF e RET invece vengono modificate:

E è l’insieme degli archi del grafo di controllo del programma.

Consideriamo le regole IF: nella semantica astratta entrambe le diramazioni sono esplorate per ogni condizione .

Di conseguenza il sistema di transizioni astratte può contenere percorsi multipli. Le funzioni di upgrade sulla memoria e sullo stack sono le stesse viste nella semantica concreta, ma ridefinite sul dominio astratto.

Semantica astratta

La relazione di transizione della semantica astratta è denotata con #. Dato un programma P ed una memoria astratta M#, il sistema di transizione astratto definito con le regole di astrazione è denotato con A(P, M#) = (C#, #, ).

Teorema 2: sia P = <c,> un programma e M#0 M sia la memoria –consistente. Consideriamo lo

stato finale di A(P, M#0 ), cioè gli stati Se per ogn’uno di questi stati M#,

S# sono mantenuti safe per P e , allora P è sicuro.

Il teorema sopra è la base del nostro metodo di controllo della sicurezza: la dimostrazione della -safety di un programma P=(c, ) può essere fatta costruendo il sistema di transizione astratta che comincia da uno stato iniziale e con l’ambiente minimo in L, e in cui ogni variabile del programma è assegnata ad un livello di sicurezza secondo quanto specificato da Successivamente, gli stati finali sono esaminati secondo la - safety di memoria e di stack degli operandi, e secondo il valore degli ambienti. Nota che il sistema di transizione astratto è finito. Infatti, essendo livelli di sicurezza, gli ambienti e i valori astratti finiti, anche la memoria astratta è finita. Inoltre, gli ipd stack sono finiti poiché contengono al più tutti gli indirizzi. Infine gli stack degli operandi astratti sono finiti perché assumiamo stack limitati.

,,M1, #0

,,M1, ## S

Related Work (sviluppi innerenti)

In questa ultima parte quanto appena visto finora verrà messo brevemente in relazione con altri lavori che si prefiggono anch’essi di effettuare un controllo sulla sicurezza di un linguaggio.

Il tema della sicurezza dei linguaggi è molto diffuso e le proprietà del concetto di flusso di informazioni sicuro dei programmi è stato via via formulato in maniera sempre più precisa.

Le soluzioni finora affrontate si possono dividere in due categorie:

l’approccio basato sui tipi (type-based).

l’approccio basato sulla semantica (semantic-based).

Type-based

• questa tecnica prevede che le informazioni sulla sicurezza di ogni variabile appartengono al corrispondente tipo ed il flusso delle informazioni di sicurezza del sistema è controllato dal significato del sistema di tipi.

• viene introdotto il concetto di non-inferenza, che prevede di considerare gli stati in cui il valore finale di ogni variabile non dipende dal valore iniziale delle variabili a più alti valori di sicurezza.

• in alcune versioni più forti la non inferenza include anche l’assenza di un flusso non sicuro dovuto alla non terminazione.

• nelle nostre impostazioni tale proprietà è posseduta se il programma è – sicuro per ogni

• la non inferenza controlla che nell’ultimo stato del sistema di transizione astratta ogni variabile in abbia un livello di sicurezza minore o uguale a

• lavori recenti che seguono questo tipo di approccio considerano linguaggi funzionali e a cui danno un sistema di tipi; e altri in cui il linguaggio Java viene esteso dando ai programmi annotazioni sul flusso di informazioni.

Semantic-based

E’ l’approccio che abbiamo visto finora.

• alcuni lavori definiscono un interpretazione astratta per il controllo del flusso di informazioni in linguaggio imperativo ad alto livello, tale metodo è basato sulla semantica denotazionale del linguaggio. Si parte, come abbiamo visto, col definire una semantica concreta che poi viene sviluppata ottenendo uno strumento statico per l’analisi. La differenza è che noi utilizziamo la semantica operazionale, il vantaggio nell’usare l’ operazionale è che essa definisce una macchina astratta e così permette di tenere informazioni che non sono legate al comportamento del programma in input e output, ma riguardano gli stati della macchina durante l’esecuzione

• altri lavori prevedono un controllo della sicurezza basato sulla semantica assiomatica

• un altro approccio può essere basato su relazioni di equivalenza parziale ( che però ha lo svantaggio di essere difficilmente reso automatizzabile)

PROBLEMA: l’utilizzo di tecniche così diversificate comporta che molti programmi che possono considerarsi sicuri per un metodo non lo possano essere per un altro.

Typed vs Semantic-based

Il vantaggio dell’approccio semantico è che in generale consente di certificare la sicurezza di una larga classe di programmi.

Lo svantaggio è che la semantica richiede l’esecuzione del programma anche se in maniera astratta, e questo aumenta la complessità dell’analisi in termini di spazio e tempo che può essere elevata per programmi di notevoli dimensioni, che possono essere invece ben gestiti da sistemi di tipi poiché trattengono poche informazioni.

Progetti futuri : estensione del metodo proposto per consentire l’utilizzo di tale approccio all’intero Java Bytecode.

Checking Security of Java Bytecode by Abstract Interpretation R. Barbuti - C. Bernardeschi - N. De...

Documents

Transcript of Checking Security of Java Bytecode by Abstract Interpretation R. Barbuti - C. Bernardeschi - N. De...