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

Il/la docente ha il dovere di vigilare affinché siano rispettate le regole di autenticità e originalità delle prove d'esame. Di conseguenza, nei casi in cui vi sia il sospetto di un comportamento irregolare, l'esame può prevedere un ulteriore approfondimento, contestuale alla prova d'esame, che potrà essere realizzato anche in modalità differente rispetto alle modalità sopra riportate.

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.