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@diNOSPAM.uniroma1.it salvo@diNOSPAM.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:

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.

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)


Topic attachments
I Attachment History Action Size Date Who Comment
PDFpdf dispense-tsl.pdf r15 r14 r13 r12 r11 manage 625.2 K 2009-04-17 - 10:32 DanieleGorla  
PDFpdf master08.pdf r1 manage 372.4 K 2009-06-16 - 10:17 IvanoSalvo slides riassuntive
Edit | Attach | Watch | Print version | History: r33 < r32 < r31 < r30 < r29 | Backlinks | Raw View | Raw edit | More topic actions
Topic revision: r33 - 2009-09-16 - DanieleGorla






 
Questo sito usa cookies, usandolo ne accettate la presenza. (CookiePolicy)
This site is powered by the TWiki collaboration platform Powered by PerlCopyright © 2008-2017 by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback