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)
Torna al Dipartimento di Informatica
This site is powered by the TWiki collaboration platform Powered by PerlCopyright © 2008-2024 by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback