Corso di Tecniche di Sicurezza basate sui Linguaggi (dott. Gorla and Salvo) - AA 2008-2009
IMPORTANTE: Prenotazione esame
Lo scritto del 17/9 si terrà nello studio dei docenti, stanza 310, Via Salaria, III piano
Presentazione del corso
L'idea fondamentale della Language-based Security è quella di spostare l'onere di verificare proprietà di sicurezza (quali ad esempio la protezione contro accessi indesiderati in memoria, virus, worms etc.) dal livello del sistema operativo, al livello delle applicazioni. Il corso ha l'obiettivo di presentare tecnologie utilizzate o in corso di sviluppo per scrivere software dimostrabilmente sicuro. In larga parte, le tecnologie presentate sono applicazioni alla Sicurezza di concetti introdotti per lo studio dei Linguaggi di Programmazione: semantica operazionale, sistemi di tipo, equivalenze osservazionali.
Orario delle lezioni
Le lezioni si svolgeranno secondo il seguente orario:
Orario |
Aula |
lun 12.00-13:30 |
Aula Alfa (Via Salaria, piano terra) |
ven 10:15-11:45 |
Aula Seminari (Via Salaria, 3° piano) |
Programma del Corso
Il programma, così come il corso, si svolge in tre parti:
- La prima parte è incentrata sull'Information Flow. Verranno affrontate le seguenti problematiche:
- vari tipi di flussi impliciti;
- un semplice linguaggio imperativo (sintassi e semantica operazionale) con relativo sistema di tipi per evitare flussi impliciti (subject reduction e non-interference).
- Generalizzazione dei risultati a un linguaggio imperativo multi-threaded (gestione di flussi basati su tempo e terminazione tramite sistemi di tipi).
- Quantified information flow
- Cenni sulla declassification e non-determinismo
- La seconda parte è incentrata su Typed Assembly Language (e sarà svolta dal dott. Ivano Salvo). Verranno affrontate le seguenti problematiche:
- sintassi, semantica e sistema dei tipi di un linguaggio assembler (TAL)
- Garanzie di sicurezza assicurate dalla proprietà di type soundness.
- Estensioni di TAL: polimorfismo, stack, heap.
- Typed Preserved Compilation: compilazione di un piccolo linguaggio type safe (TINY) in TAL.
- La terza parte è incentrata sui reference monitors. Verranno affrontate le seguenti problematiche:
- politiche di sicurezza che si possono forzare via monitor.
- Instrumentazione del codice per evitare accessi di memoria illegali.
- Formalismi per definire politiche di sicurezza application dependent: automi e guarded command.
- Generazione del codice instrumentato dalla specifica di una politicha di sicurezza.
- Clasi di Complessità e politiche di Sicurezza.
Testi consigliati
I materiali del corso saranno prevalentemente articoli scientifici disponibili sul web. A lezione si presenterà una opportuna selezione di tale materiale, come riportato di seguito; una lettura completa dei lavori è comunque suggerita per avere una visione più completa degli argomenti trattati. Sono disponibili delle dispense tratte dagli appunti di alcuni studenti che hanno seguito il corso nell'A.A. 2006-07, che rispecchiano in maniera fedele il modo in cui gli argomenti sono presentati a lezione. Le dispense sono ancora in uno stato preliminare e possono contenere errori: si sconsiglia fortemente l'uso delle dispense come unico materiale di studio.
- Per la parte introduttiva sul problema della Language Based Security, si consiglia la lettura di:
- Per la parte su Information flow, si utilizzeranno i seguenti lavori:
- Language-based Information-flow Security (sezioni 1, 2 e 4) Andrei Sabelfeld, Andrew Meyers: http://www.cs.cornell.edu/andru/papers/jsac/sm-jsac03.pdf
- Language Issues in Mobile Program Security (sezione 3) Dennis Volpano, Geoffrey Smith: http://cisr.nps.navy.mil/downloads/98paper_langiss.pdf
- A Sound Type System for Secure Flow Analysis (sezioni 4, 5 e 6) Dennis Volpano, Geoffrey Smith, Cynthia Irvine: http://citeseer.ist.psu.edu/cache/papers/cs/7437/http:zSzzSzwww.csl.sri.comzSz~volpanozSzlanguageszSzpaperszSzatsczSzjcs.pdf/volpano96sound.pdf
- Secure Information-flow in a Multi-threaded Imperative Language (sezioni da 3 a 8) Geoffrey Smith, Dennis Volpano: http://cisr.nps.navy.mil/downloads/98paper_multithread.pdf
- Verifying secrets and relative secrecy (sezioni da 1 a 5 e cenni delle sezioni restanti) Dennis Volpano, Geoffrey Smith: http://citeseer.ist.psu.edu/compress/0/papers/cs/26174/http:zSzzSzwww.cs.fiu.eduzSz~smithgzSzpaperszSzpopl00.ps.gz/volpano00verifying.ps
- Quantitative information flow, relations and polymorphic types (sezioni da 1 a 5)David Clark, Sebastian Hunt, and Pasquale Malacaria: http://logcom.oxfordjournals.org/cgi/reprint/15/2/181?ijkey=56At7mt7JtZw6&keytype=ref
- Per la parte su TAL, si utilizzerà la dispensa di David Walker:
- Per la parte sui Reference Monitor: si utilizzeranno:
Altre letture consigliate:
Modalità di esame
Ci sono varie modalità per sostenere l'esame:
- esoneri
- svolegimento di tesine su argomenti di ricerca di difficoltà ragionevole concordati con il docente da esporre nel corso delle lezioni agli altri studenti del corso (modalità consigliata a chi intende svolgere la propria tesi su questi argomenti)
- sostenere un esame orale su tutti gli argomenti svolti a lezione (N.B.: questa modalità è indicata agli studenti che non seguono le lezioni).
Diario delle Lezioni
- 2/3/09: introduzione alla Language Based Security e alle problematiche di information flow (capitoli 1 e 2 delle dispense)
- 3/3/09: sintassi e semantica di un linguaggio imperativo minimale (pagg. 8-14 delle dispense)
- 9/3/09: prime idee per un sistema di tipi che accetti solo programmi non-interferenti e sistema di tipi più permissivo (pagg. 14-21 delle dispense)
- 13/3/09: proprietà elementari del sistema di tipi, teorema di subject reduction e teorema di type safety (pagg. 21-24)
|