dott. Ivano Salvo, con la collaborazione
del dott. Daniele Gorla
anno accademico 2005/06
Introduzione e prerequisiti
[1] martedì 7 marzo
Presentazione al corso. Il problema della sicurezza: dei
programmi. L'evoluzione dell problema della sicurezza.
L'impatto delle nuove tecnologie di rete sul problema della sicurezza.
Approccio classico: limiti e
possibili alternative: sistemi di tipo, in-lined reference monitors.
[2] giovedì 9 marzo
Principi base: minimo accesso, minimo codice fidato.
Limiti dell'approccio basato su reference monitor: flessibilità ed
efficienza.
Formalizzazione di politiche di sicurezza.
Introduzione agli approcci basati sui linguaggi: IRM e TAL e PCC.
[3] martedì 14 marzo
I sistemi di tipo nella loro forma più pura: il lambda calcolo
tipato semplice.
Cenni al lambda calcolo come modello di calcolo: rappresentazione dei
numeri e funzioni numeriche.
Parte I: Typed Assembly Language
[4] martedì 21 marzo
Principali proprietà del lambda calcolo e loro significato: subject
reduction, terminazione, unicità del tipo (sistemi
à la
Church), esistenza tipo principale (sistemi à la Curry).
Il concetto di Type Soundness.
Typed Assembly Language: sintassi e semantica operazionale
Definizione degli stati di errore (bad states).
[5] giovedì 23 marzo
Typed Assembly Language: sistema dei tipi. Esempi di programmi mal
tipati. Sottotipaggio.
Enunciato di Type Soundness per TAL.
[6] martedì 28 marzo
Cenni alla dimostrazione del risultato di Type Soundness per TAL.
Estensioni di TAL: polimorfismo.
[7] giovedì 30 marzo
Estensioni di TAL: stack types.
Il linguaggio funzionale Tiny.
[8] martedì 4 aprile
Typed Preserved Compilation: uso di TAL (polimorfo) come target language
della compilazione di Tiny.
[9] giovedì 6 aprile
TAL: estensione con heap, e gestione di alias: alias types.
[10] martedì 11 aprile
Alias types, compilazione separata, linking.
Parte II: Tipi per Information Flow
[11] giovedì 20 aprile
Introduzione: vari tipi di flussi di informazione e relative definizioni
di non-interference per evitarli.
[12] giovedì 27 aprile
Sintassi e semantica operazionale di un semplice linguaggio imperativo;
sistema di tipi per evitare flussi impliciti.
[13] martedì 2 maggio
Dimostrazione dei teoremi di Subject reduction e Non-interference
per il sistema di tipi che gestisce flussi impliciti.
[14] giovedì 4 maggio
Possibilistic non-interference e multi-threads; un semplice
linguaggio
per programmi multi-threaded; un sistema di tipi rivisto per gestire
flussi impliciti; teorema di non-interference.
[15] martedì 9 maggio
Influenze di tempo e politiche di scheduling (round-robin e
probabilistico) sulla possibilistic non-interference; cenni alla
probabilistic non-interference.
[16] giovedì 11 maggio
Introduzione al problema della declassification: svelare informazioni
parziali su variabili segrete. Assenza di attacchi polinomiali in
ambito
sequenziale esteso con la primitiva 'match(.)'; attacco polinomiale
con espressioni generiche o con concorrenza sincrona.
Parte III: In-Lined Reference Monitors
[17] martedì 16 maggio
Generalità sui Reference Monitors.
Caratterizzazione delle politiche di Sicurezza forzabili da un
monitor.
Instrumentazione del codice per proteggere gli accessi in memoria:
segment matching e sandboxing.
[18] giovedì 18 maggio
Cenni all'uso di interpreti come reference monitor. Partial
Evaluation.
Linguaggi di specifica di politiche di Sicurezza: Security Automata
e Guarded Command.
[19] giovedì 25 maggio
Implementazione SASI di in-lined reference monitor.
Confronto tra versione x86 e JVM: i benefici delle annotazioni di
tipo.
Classi di computabilità e politiche di sicurezza:
formalizzazione del modello di computazione con MdT.
Equivalenza tra statically enforceable e predicati decidibili.
[20] martedì 30 maggio
Equivalenza tra EM enforceable e predicati coRE.
La classe RW-enforceable.
Relazioni tra EM e RW.
