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: insegnare alle studentesse/agli studenti i principi e le motivazioni della compilazione corretta e sicura; mostrare alle studentesse/agli studenti come usare Rocq per supportare prove meccaniche della correttezza/sicurezza dei compilatori.

La frequenza e la partecipazione attiva al corso e lo studio individuale consentiranno ai partecipanti di:
1. Conoscenza e comprensione
1.1. 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 Rocq;
2.2. sapere formalizzare i requisiti di sicurezza e correttezza del compilatore in Rocq;
2.3. sapere utilizzare Rocq 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, Rocq, OCaml, Haskell, Agda, F#, Scala, Lean, ...). Inoltre, è suggerita una conoscenza di base con la teoria dei linguaggi di programmazione (sintassi, semantica, sistemi di tipo, ...).

Il corso "[PHD226] FOUNDATIONS OF PROGRAMMING LANGUAGES IN COQ" è da considerarsi propedeutico a questo e la sua frequenza è fortemente consigliata.

* Blocco 1 (1h + 2h laboratorio)
+ Introduzione al software sicuro e motivazioni
+ (Laboratorio guidato) Ripasso dei contenuti di "[PHD226] Foundations of Programming Languages in Coq"

* Blocco 2 (1h + 2h lab)
+ Introduzione ai compilatori, la loro struttura e terminologia di base
+ Correttezza dei compilatori
+ (Laboratorio guidato) Definizione di un semplice compilatore in Rocq e prova di correttezza

* Blocco 3 (2h + 2h laboratorio)
+ 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
+ Concetti formali di sicurezza: trace properties, loro caratteristiche
+ Non-interferenza, generalizzazione alle hyperproperties e la loro preservazione; Attaccanti attivi
+ (Laboratorio) Esercizi su FAC, modellazione e dimostrazioni di non-interferenza

[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 4/8h 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)

orale

L'esito dell'esame può essere: "approvato" oppure "non approvato". L'esito è "approvato" richiede:
- conoscenza sufficiente degli argomenti del programma e capacità di comprensione applicata adeguata;
- capacità autonome e coerenti di analisi, valutazione e interpretazione;
- uso appropriato e controllato della terminologia tecnica;
- esposizione chiara e ordinata.

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.