PRINCIPLES OF CORRECT AND SECURE COMPILATION

I metodi formali sono di fondamentale importanza per un informatico e questo corso di dottorato ambisce a fornire un'introduzione moderna ed aggiornata alla compilazione corretta e sicura, un filone dei metodi formali.
In particolare, gli obbiettivi del corso sono: introdurre le studentesse/gli studenti alla sintassi e alla semantica dei linguaggi di programmazione in Coq (un proof assistant); insegnare alle studentesse/agli studenti i principi e le motivazioni della compilazione corretta e sicura; mostrare alle studentesse/agli studenti come usare Coq per supportare prove meccaniche della correttezza/sicurezza dei compilatori. Le ultime ore del corso saranno dedicate ad aspetti più avanzati, come tecniche di prova moderne o applicazioni allo stato dell'arte.

La frequenza e la partecipazione attiva al corso e lo studio individuale consentiranno ai partecipanti di:
1. Conoscenza e comprensione
1.1. acquisire i fondamenti della sintassi e semantica dei linguaggi di programmazione in Coq;
1.2. acquisire i principi e le motivazioni della compilazione corretta e sicura
2. Capacità di applicare conoscenza e comprensione
2.1. sapere modellare un semplice linguaggio e il suo compilatore in Coq;
2.2. sapere formalizzare i requisiti di sicurezza e correttezza del compilatore in Coq;
2.3. sapere utilizzare Coq per dimostrare semplici proprietà dei compilatori.
3. Capacità di giudizio
3.1. sapere valutare le alternative formulazioni di correttezza e sicurezza dei compilatori, discutendone pregi e difetti

Gli studenti/le studentesse devono possedere una conoscenza di base della teoria degli insiemi, della logica e dell'induzione matematica. Inoltre, è richiesta familiarità con almeno un linguaggio di programmazione funzionale (ad esempio, OCaml, Haskell, Agda, F#, Scala, ...). Inoltre, è suggerita una conoscenza di base con la teoria dei linguaggi di programmazione (sintassi, semantica, sistemi di tipo, ...).

* Blocco 1 (1h + 3h laboratorio)
+ Introduzione al software sicuro e motivazioni
+ (Laboratorio guidato) Fondamenti di Coq
+ (Laboratorio) Q&A su Coq; Esercizi
* Blocco 2 (4h + 2h laboratorio)
+ Sintassi e semantica dei linguaggi di programmazione
+ Esempi: imperativo, funzionale e a basso livello
+ Introduzione ai compilatori, la loro struttura e terminologia di base
+ Correttezza dei compilatori
+ (Laboratorio guidato) Definizione di un semplice linguaggio di programmazione e del suo compilatore; Dimostrazione di correttezza
* Blocco 3 (4h + 2h laboratorio)
+ Ulteriori approfondimenti sulla correttezza dei compilatori, ottimizzazioni
+ Introduzione alla sicurezza dei compilatori
+ Fully Abstract Compilation (FAC) e la sua relazione con la correttezza
+ Breve panoramica delle tecniche di prova di base per la FAC; Osservazioni ed esempi
+ (Laboratorio) Esercizi su correttezza e FAC
* Blocco 4 (4h + 2h laboratorio)
+ Concetti formali di sicurezza: trace properties, loro caratteristiche
+ Non-interferenza, generalizzazione alle hyperproperties e la loro preservazione; Attaccanti attivi
+ (Laboratorio) Modellazione e dimostrazione dell preservazione della non-interferenza
* Blocco 5 (4h)
+ Argomenti avanzati
* Blocco 6 (4h)
+ (Laboratorio) Q&A; Altri esercizi

Essendo un corso su un argomento avanzato, il nostro materiale principale di studio saranno articoli di ricerca. A seconda degli argomenti avanzati scelti, durante il corso verrà fornito ulteriore materiale.

[1] B. C. Pierce et al., "Software foundations, Vol 1: Logical Foundations", https://softwarefoundations.cis.upenn.edu/lf-current/index.html
[2] B. C. Pierce et al., "Software foundations, Vol 2: Programming Language Foundations", https://softwarefoundations.cis.upenn.edu/plf-current/index.html
[3] X. Leroy, "A formally verified compiler back-end", Journal of Automated Reasoning, vol. 43, pp. 363–446,
2009.
[4] D. Patterson and A. Ahmed, "The next 700 compiler correctness theorems (functional pearl)",
Proceedings of the ACM on Programming Languages, vol. 3, no. ICFP, pp. 1–29, 2019.
[5] F. Piessens, "Security across abstraction layers: old and new examples", in 2020 IEEE European
Symposium on Security and Privacy Workshops (EuroS&PW), 2020, pp. 271–279.
[6] M. Patrignani, A. Ahmed, and D. Clarke, "Formal approaches to secure compilation: A survey of fully
abstract compilation and related work", ACM Computing Surveys (CSUR), vol. 51, no. 6, pp. 1–36, 2019.
[7] M. Busi, L. Galletta, and Others, "A brief tour of formally secure compilation", in ITASEC 2019.
[8] C. Abate, R. Blanco, D. Garg, C. Hritcu, M. Patrignani, and J. Thibault, "Journey beyond full abstraction:
Exploring robust property preservation for secure compilation", in 2019 IEEE 32nd Computer Security
Foundations Symposium (CSF), 2019, pp. 256–25615.
[9] A. Ahmed, D. Garg, C. Hritcu, and F. Piessens, "Secure compilation (Dagstuhl seminar 18201)", in
Dagstuhl Reports, 2018, vol. 8.
[10] D. Chisnall, D. Garg, C. Hritcu, and M. Payer, "Secure Compilation (Dagstuhl Seminar 21481)", in
Dagstuhl Reports, 2022, vol. 11.

Due opzioni, con un carico di lavoro previsto di circa 8/12 ore, entrambe da discutere con l'insegnante:
* Seminario: organizzare un seminario di 45 minuti/1 ora su un argomento avanzato a scelta
* Progetto: sviluppare un'estensione non banale a uno degli esercizi/argomenti trattati nel corso (ad esempio, funzionalità aggiuntive su un compilatore)

Corso frontale che si avvale anche di esercizi svolti durante le ore di laboratorio (eventualmente online) per consolidare i concetti e favorire la discussione tra gli studenti/studentesse.

Inglese

orale