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

News

28.04.2023

Your Papers and Summaries

Hello all,

not everyone has given their preferences with regards to the paper they want to present.
Regardless, paper assignment was due today. You can find your paper on your personal status page in the CMS.
If you are in e.g. tutorial slot 5, your paper is... Weiterlesen

Hello all,

not everyone has given their preferences with regards to the paper they want to present.
Regardless, paper assignment was due today. You can find your paper on your personal status page in the CMS.
If you are in e.g. tutorial slot 5, your paper is number 5. Ignore the tutorial time.

For the summaries, the assignment will be as follows:

If you have paper 1, you summarize papers 3 and 10.
If you have paper 3, you summarize papers 5 and 11.
If you have paper 5, you summarize papers 10 and 12.
If you have paper 10, you summarize papers 11 and 1.
If you have paper 11, you summarize papers 12 and 3.
If you have paper 12, you summarize papers 1 and 5.

Let us know if you've got any questions, be it with regards to your paper or organization of the seminar.
Cheers

24.04.2023

Pick Preferences

Hi all,

You should now be able to pick preferences for the respective paper of your interest.
Each paper corresponds to a tutorial, ignore the time slots.
If you pick Tutorial 1, you'll present paper 1. If you pick Tutorial 7, you'll present paper 7. et... Weiterlesen

Hi all,

You should now be able to pick preferences for the respective paper of your interest.
Each paper corresponds to a tutorial, ignore the time slots.
If you pick Tutorial 1, you'll present paper 1. If you pick Tutorial 7, you'll present paper 7. et cetera
Papers will be assigned at the end of the week.

Cheers

19.04.2023

Open seats

Hi all,

there are still some open seats available at the seminar. Just register in the CMS.
Additionally, the kick-off slides are now available in the Material section.

 

cheers

18.04.2023

Information regarding Kick-off meeting

Hi all,

the zoom link for the kick-off meeting can now be found in the Material section.
The kick-off meeting will start tomorrow 19.04.23 at 4 PM sharp.

 

see you there!

 

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



Datenschutz | Impressum
Bei technischen Problemen wenden Sie sich bitte an die Administratoren