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: introduce students to the syntax and semantics of programming languages in Coq (a proof assistant); familiarize students with the principles and motivations of correct and secure compilation; teach students how to use the Coq proof assistant to support mechanical proofs of compiler correctness/security. The last few hours of the course will be dedicated to more advanced topics, such as modern proof techniques or state-of-the-art applications.

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

1. Knowledge and Understanding
1.1. gain a foundational understanding of the syntax and semantics of programming languages in Coq;
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 language and its compiler in Coq;
2.2. formalize security and correctness requirements of the compiler in Coq;
2.3. utilize Coq 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 OCaml, Haskell, Agda, F#, Scala, etc.) is required. Furthermore, a basic understanding of programming language theory (syntax, semantics, type systems, etc.) is suggested.

* Block 1 (1h + 3h lab)
+ Introduction to secure software and motivation
+ (Guided lab) Basics of the Coq theorem prover
+ (Lab) Q&A; Coq exercises
* Block 2 (4h + 2h lab)
+ Syntax and semantics of programming languages
+ Examples: imperative, functional and low level
+ Introduction to compilers, their structure and basic terminology
+ Compiler correctness
+ (Guided lab) Definition of a simple programming language and its compiler; Proof of correctness
* Block 3 (4h + 2h lab)
+ More on compiler correctness, optimizations
+ Introduction to compiler security, early examples
+ Fully Abstract Compilation (FAC), its relation to correctness
+ Quick overview of basic FAC proof techniques; Observations and examples
+ (Lab) Exercises on correctness and FAC
* Block 4 (4h + 2h lab)
+ Formal notions of security: trace properties, their characteristics
+ Non-interference, generalization to hyperproperties, and their preservation; Active attackers
+ (Lab) Modelling and proving (preservation of) non-interference
* Block 5 (4h)
+ Advanced topics: TBD
* Block 6 (4h)
+ (Lab) Q&A; More exercises

Being a course on an advanced topic, our main material for study will be research papers. Depending on the advanced topics of choice, more material will be provided during the course.

[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, both to be discussed with the instructor beforehand:
* 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)

Expected amount of work: 8-12 hours

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

English

oral