WebHome < TSL

<table border=2><tr valign=top><td width="80%">

---++ Corso di Tecniche di Sicurezza basate sui Linguaggi (dott. Gorla and Salvo) - AA 2008-2009


| *Docenti* | Daniele Gorla | Ivano Salvo|||
| *Telefono* | 06-4991 8434 | 06-4991 8432|||
| *Ricevimento studenti* | per appuntamento | |||
| *Studio* | Via Salaria 113, 3° Piano, st. 310 | Via Salaria 113, 3° Piano, st. 310|||
| *Email* | gorla@di.uniroma1.it   | salvo@di.uniroma1.it  |||


----
---++ 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:
<center>
| *Orario*    | *Aula* |
| lun 12.00-13:30 | Aula Alfa (Via Salaria, piano terra) |
| ven 10:15-11:45 | Aula Seminari (Via Salaria, 3° piano) |
</center>


---++ 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.

   * [[%ATTACHURL%/dispense-tsl.pdf][Dispense]] 
 
   * Per la parte introduttiva sul problema della <b>Language Based Security</b>, si consiglia la lettura di:
      * A Language-Based Approach to Security <i>Fred B. Schneider, Greg Morrisett, Robert Harper </i>: http://www.cs.cmu.edu/~rwh/papers/langsec/dagstuhl.pdf

   * Per la parte su <b>Information flow</b>, si utilizzeranno i seguenti lavori:
      * Language-based Information-flow Security (sezioni 1, 2 e 4) <i>Andrei Sabelfeld, Andrew Meyers</i>: http://www.cs.cornell.edu/andru/papers/jsac/sm-jsac03.pdf
      * Language Issues in Mobile Program Security (sezione 3) <i>Dennis Volpano, Geoffrey Smith</i>: http://cisr.nps.navy.mil/downloads/98paper_langiss.pdf
      * A Sound Type System for Secure Flow Analysis (sezioni 4, 5 e 6) <i>Dennis Volpano, Geoffrey Smith, Cynthia Irvine</i>: 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</a> (sezioni da 3 a 8) <i>Geoffrey Smith, Dennis Volpano</i>: http://cisr.nps.navy.mil/downloads/98paper_multithread.pdf
      * Verifying secrets and relative secrecy (sezioni da 1 a 5 e cenni delle sezioni restanti) <i>Dennis Volpano, Geoffrey Smith</i>: 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)<i>David Clark, Sebastian Hunt, and Pasquale Malacaria</i>: http://logcom.oxfordjournals.org/cgi/reprint/15/2/181?ijkey=56At7mt7JtZw6&keytype=ref

   * Per la parte su <b>TAL</b>, si utilizzerà la dispensa di David Walker:
      * An Introduction to Typed Assembly Language <i>David Walker</i>: http://www.cs.cmu.edu/~dpw/papers/tal-intro.ps

   * Per la parte sui <b>Reference Monitor:</b> si utilizzeranno:
      * Enforceable Security Policies <i>Fred B. Schneider</i>: http://www.cs.cornell.edu/fbs/publications/EnfSecPols.pdf
      * SASI Enforcement of Security Policies: A Retrospective <i>Fred Schneider, Ulfar Erlingsson</i>: http://www.research.microsoft.com/users/ulfar/tr99_1758.pdf
      * Computability Classes for Enforcement Mechanisms <i>Kevin W. Hamlen, Greg Morrisett, Fred B. Schneider</i>: http://www.cs.cornell.edu/fbs/publications/EnfClassesTR2003-1908.pdf


Altre letture consigliate:
   * Attacking Malicous Code</a> <i>Gary Mc Graw, Greg Morrisett</i>: http://www.cs.cornell.edu/home/jgm/cs711sp02/maliciouscode.pdf
   * Language-Based Security</a> <i>Dexter Kozen</i>: http://www.cs.purdue.edu/homes/jv/smc/pubs/kozen-mfcs99.ps
   * Alias Types <i>Frederick Smith, David Walker, Greg Morrisett</i>: http://www.cs.cornell.edu/talc/papers/alias.pdf
   * Efficient Softwar-Based Fault Isolation <i>R. Wahbe, S. Lucco, T. E. Anderson, S. L. Graham</i>: http://www.cs.sunysb.edu/~rtjohnso/teaching/cse509-sp07/sfi.pdf

----
---++ 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)
<!--
   * 5/3/08: teorema di type safety (pagg. 23-24)
   * 11/3/08: flussi di informazione impliciti in linguaggi multi-threaded; sintassi, semantica operazionale e sistema di tipi per linguaggi multi-threaded; teorema di non-interferenza sequenziale (pagg. 25-30)
   * 12/3/08: teroema di non interferenza per programmi multithreaded; aggiunta del clock; studio di politiche di scheduling di tipo Round Robin; studio di politiche di scheduling probabilistiche e cenni alla non-interferenza probabilistica (pagg. 31-35)
   * 18/3/08: due formulazioni della relative secrecy per programmi che accedono a un segreto tramite il costrutto 'match' e per programmi tipabili (pagg. 36-41)
   * 19/3/08: varianti sulla relative secrecy; nozioni basilari di teoria dell'informazione: entropia (pagg.41-45)
   * 26/3/08: proprietà dell'entropia; entropia condizionata, mutua informazione, mutua informazione condizionata e loro proprietà; mutua informazione condizionata come misura del flusso di informazioni (pagg.46-50)
   * 1/4/08: definizione relazionale del flusso di informazioni e lemmi preliminari (pagg. 51-53)
   * 2/4/08: teorema di coincidenza delle nozioni di flusso nullo e non-interferenza relazionale (pagg. 54-55)
   * 8/4/08: Introduzione a TAL e PCC. Sintassi e Semantica Operazionale di TAL.
   * 9/4/08: Cenni alla rappresentazione della logica con lambda calcoli tipati. Sistema di tipo per TAL. 
   * 15/4/08: Subtyping. Principali proprieta' di TAL: type safety e suo significato.
   * 16/4/08:  Dimostrazione della proprieta' di Type Safety. Polimorfismo.
-->

----


</td></tr>
</table>

   * [[%ATTACHURL%/master08.pdf][master08.pdf]]: slides riassuntive
Attachments
Topic attachments
I	Attachment	History	Action	Size	Date	Who	Comment
pdf	dispense-tsl.pdf	r15 r14 r13 r12 r11	manage	625.2 K	2009-04-17 - 10:32	DanieleGorla
pdf	master08.pdf	r1	manage	372.4 K	2009-06-16 - 10:17	IvanoSalvo	slides riassuntive
This topic: TSL > WebHome
Topic revision: r33 - 2009-09-16 - DanieleGorla