Tecniche di Sicurezza Basate sui Linguaggi

dott. Ivano Salvo, con la collaborazione del dott. Daniele Gorla
anno accademico 2005/06

Introduzione
Programma del corso
Materiale e testi di consultazione
Letture consigliate
Orari
Modalità d'esame
Avvisi
Diario delle Lezioni

Ultima modifica: 25 maggio 2006

Introduzione

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.

Programma del corso

Introduzione [3]:Il problema della Sicurezza: approccio classico: limiti e potenziali alternative.
Introduzione ai sistemi di tipo: il lambda calcolo tipato semplice: principali proprietà e loro conseguenze.

Typed Assembly Language [7]: sintassi, semantica, 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.

Information Flow [6]: vari tipi di flussi impliciti; un semplice linguaggio imperativo (sintassi e semantica operazionale).
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). Cenni sulla declassification.

Reference Monitors [4]: 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.

Materiale e testi di consultazione

I materiali del corso saranno prevalentemente articoli scientifici che saranno via via distribuiti a lezione e/o resi disponibili qui sotto:

Per la parte introduttiva sul problema della Language Based Security, si consiglia la lettura dei seguenti lavori:
Attacking Malicous Code Gary McGraw, Greg Morrisett
Language-Based Security Dexter Kozen
A Language-Based Approach to Security Fred B. Schneider, Greg Morrisett, Robert Harper

Per i richiami di lambda-calcolo tipato, vedere le ottime slides di Henk Barendregt (le prime due sezioni, i curiosi possono leggere tutto...)
Applications of the Lambda Calculus Henk Barendregt

Per la parte relativa al Typed Assembly Language, seguo la dispensa di David Walker:
An Introduction to Typed Assembly Language David Walker

Per la parte finale sugli heap types, la dispensa di David Walker risulta alquanto esoterica.
Consiglio la lettura del lavoro: Alias Types Frederick Smith, David Walker, Greg Morrisett
Per la parte su Information Flow, si seguiranno la seguenti fonti (si consiglia comunque di leggere gli articoli per intero):
Language-based Information-flow Security (sezioni 1, 2 e 4) Andrei Sabelfeld, Andrew Meyers
Language Issues in Mobile Program Security (sezione 3) Dennis Volpano, Geoffrey Smith
A Sound Type System for Secure Flow Analysis (sezioni 4, 5 e 6) Dennis Volpano, Geoffrey Smith, Cynthia Irvine
Secure Information-flow in a Multi-threaded Imperative Language (sezioni da 3 a 8) Geoffrey Smith, Dennis Volpano
Verifying secrets and relative secrecy (sezioni da 1 a 5 e cenni delle sezioni restanti) Dennis Volpano, Geoffrey Smith

Per la parte sui Reference Monitor: si consiglia la lettura di:
Enforceable Security Policies Fred B. Schneider
Efficient Softwar-Based Fault Isolation R. Wahbe, S. Lucco, T. E. Anderson, S. L. Graham
SASI Enforcement of Security Policies: A Retrospective, Fred Schneider, Ulfar Erlingsson
Computability Classes for Enforcement Mechanisms (sezioni 1,2,3,5, dimostrazioni teoremi 1,2,3,4) Kevin W. Hamlen, Greg Morrisett, Fred B. Schneider

Letture consigliate:

Gli studenti con spiccato interesse alla teoria, possono consultare l'articolo fondamentale sul Typed Assembly Language: From System F to Typed Assembly Language Greg Morrisett, David Walker, Karl Crary, Neal Glew: si tratta di un articolo tecnicamente ostico, destinato a un pubblico adulto e motivato.
Chi viceversa fosse interessato a vedere come le cose viste a lezione prendono forma in tool per lo sviluppo di software, può consultare il lavoro: TALx86: A Realistic Typed Assembly Language Greg Morrisett et al.

Oltre ai materiali segnalati, esistono numerose pagine dedicate a progetti connessi a Language Based Security, che spesso contengono link utili.
Una raccolta di link particolarmente completa, è la seguente Language Based Security Notes and Papers curata da Greg Morrisett.

Orario

Lezioni:
martedì 13:45-15:15 (Aula Alfa)
giovedì 8:45-10:15 (Aula Alfa)
Ricevimento studenti (Via Salaria, stanza 310): mercoledì, ore 11:30 - 12:30.

Modalità d'esame

L'esame sarà diviso in due parti:

svolgimento e presentazione di una tesina da parte che può avere sia carattere teorico (approfondimento di qualche argomento del corso, attraverso la lettura di articoli scientifici) o pratico/implementativo (case studies). La tesina costituisce 2/3 della valutazione finale.
superamento di un test con domande a scelta multipla e/o aperta in cui verrà chiesto allo studente la conoscenza e la capacita' di mettere in relazione le nozioni apprese a lezione. Vale 1/3 della valutazione finale.

Avvisi

La lezione di martedì 23 maggio è annullata
causa occupazione aula alfa per la seduta di laurea.