Formal Compiler Security Xaver Fabian, Matthis Kruse, Faezeh Nasrabadi, Robert Künnemann

Formal Compiler Security (7CP, BLOCK Seminar)

For registration, please apply for this seminar through the central seminar assignment system.

 

Compilers are used to compile source languages (e.g. Rust) to target languages (e.g. Assembly).
However, how can we be sure that security properties of the source code like Memory Safety or Constant Time are \textit{preserved} by the compiler?
One way to achieve this is by defining correctness criteria that specify when a compiler is secure.

 

In this seminar, we will explore different kinds of correctness criteria for compilers and what security guarantees they offer. Furthermore, the course will discuss specific instances of secure compilers and which mechanisms they exploit (i.e. types, hardware features like enclaves) to attain security.

During the seminar, participants will learn how to differentiate between correctness criteria, the kind of security they achieve and what their limitations are. 

 

Requirements: A basic understanding of programming (Programmierung 1, Programmierung 2) and compilers is required.
Having an interest in formal methods / semantics is a plus.

Course Organisation

This seminar is a block seminar and is structured as follows:

• Kick-off meeting in the first week of the semester (19.04.23 at 4 PM) (via zoom).
• During the semester, you will write 2-3 (depending on the number of students) summaries on a paper that you were not assigned on.
• During the semester break, we will have one block (a week 11.9 - 15.9) of lectures that enable participants to understand the material fully and better. Attendance is mandatory.
• Once the lectures are done, students will have time to prepare their presentations and have a practice talk with us. The presentations will be organized in a block format approximately 2 weeks after the lectures (~ 29.9). Following each presentation, we will have a round table discussion about the presented paper. Attendance and active participation are mandatory.

During the kick-off, we will present a short overview of the content and format of the seminar.

 

Evaluation and Grading

• Presentation: (50%) You will deliver a presentation (30 minutes) on the paper assigned to you and lead the round table discussion after your presentation. You will have the chance to have a practice talk with one of the lecturers before the final presentation.
• 2 -3 (depending on the number of students) summaries: (30%) Write a short (max 1-2 pages) paper summary about one of the papers that you are not presenting. A good paper summary should be concise while retaining clarity and must include the following:
  1. Context and Background: What is the domain of the work?
  2. Problem: What is the problem that is addressed in the paper? Why is the problem complex? Why is it interesting?
  3. Main Idea: What is the main idea that solves the problem in the paper?
  4. Contribution: How does it advance the state of the art? What exactly is new and valuable in the paper?
  5. Evaluation: Describe the languages, compiler, correctness criteria and proof techniques adopted by the authors.
  6. Pros and Cons: What do you think is good about the paper? What are its weaknesses and what are its limitations? Likewise, report any possible ideas for improving the paper.
• In addition to your summary, you will prepare and submit 3 questions that you will ask during the presentation. 
• In-class participation (20%): Active participation in the round table discussion is required.

List of Papers

This is the list of papers to pick from in no particular order:

1. MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code - paper

2. Formal Verification of a Constant-Time Preserving C Compiler - paper

3. Beyond Good and Evil Formalizing the Security Guarantees of Compartmentalizing Compilation - paper

4. When Good Components Go Bad Formally Secure Compilation Despite Dynamic Compromise - paper

5. DimSum: A Decentralized Approach to Multi-language Semantics and Verification - paper

6. CapablePtrs: Securely Compiling Partial Programs using the Pointers-as-Capabilities Principle - paper

7. Semantic Soundness for Language Interoperability - paper

8. Le temps des Cerises: efficient temporal stack safety on capability machines using directed capabilities - paper

9. SecurePtrs: Proving Secure Compilation with Data-Flow Back-Translation and Turn-Taking Simulation - paper

10. The High-Level Benefits of Low-Level Sandboxing - paper

11. Exorcising Spectres with Secure Compilers - paper

12. Jasmin: High-Assurance and High-Speed Cryptography - paper