PRINCIPLES OF CORRECT AND SECURE COMPILATION

Formal methods are of the fundamental importance for computer scientists, and this PhD-level course aims to provide a modern and up-to-date introduction to a specific subfield of formal methods: correct and secure compilation.
In particular, the goals of this course are: familiarize students with the principles and motivations of correct and secure compilation; teach students how to use the Rocq proof assistant to support mechanical proofs of compiler correctness/security.

Attendance and active participation in the course, along with individual study, will enable participants to:

1. Knowledge and Understanding
1.2. acquire the principles and motivations of correct and secure compilation.

2. Ability to Apply Knowledge and Understanding
2.1. be able to model a simple language and its compiler in Rocq;
2.2. formalize security and correctness requirements of the compiler in Rocq;
2.3. utilize Rocq to demonstrate simple properties of compilers.

3. Ability to Judge
3.1. evaluate alternative formulations of compiler correctness and security, discussing their merits and drawbacks.

Students are required to have a basic knowledge of set theory, logic, and mathematical induction. Additionally, familiarity with at least one functional programming language (such as Rocq, OCaml, Haskell, Agda, F#, Scala, Lean, etc.) is required. Furthermore, a basic understanding of programming language theory (syntax, semantics, type systems, etc.) is suggested.

The course "[PHD226] FOUNDATIONS OF PROGRAMMING LANGUAGES IN COQ" is to be considered preparatory to this one, and attendance is strongly recommended.

Block 1 (1h + 2h lab)
– Introduction to secure software and motivations
– (Guided lab) Review of the contents of "[PHD226] Foundations of Programming Languages in Coq"

Block 2 (1h + 2h lab)
– Introduction to compilers, their structure, and basic terminology
– Compiler correctness
– (Guided lab) Definition of a simple compiler in Rocq and proof of correctness

Block 3 (2h + 2h lab)
– Introduction to compiler security
– Fully Abstract Compilation (FAC) and its relation to correctness
– Brief overview of basic proof techniques for FAC; observations and examples
– Formal security concepts: trace properties and their characteristics
– Noninterference, generalization to hyperproperties and their preservation; active attackers
– (Lab) Exercises on FAC and noninterference

[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.

Two options, expected amount of work ~4/8h, both to be discussed with the instructor:
* Seminar: organize a 45m/1h seminar on an advanced topic of choice
* Project: develop a non-trivial extension to one of the exercises/topics covered in the course (e.g., additional features on a compiler)

oral

The exam result can be either "approved" or "not approved". The "approved" result requires:
- sufficient knowledge of the course topics and adequate applied understanding;
- autonomous and coherent capacities for analysis, evaluation, and interpretation;
- appropriate and controlled use of technical terminology;
- clear and well-structured presentation.

Classroom-based course supplemented by exercises conducted during laboratory hours (potentially online) to reinforce concepts and encourage discussion among students.