Secure Compilation

The course will combine paper reading (at home), round table discussions with student presentations (in class, roughly 1 every week), as well as lectures (in class, in between presentations) to enable participants to understand the material fully. While the normal workload for a seminar is 60 hours classes + 150 hours homework, the lectures shift the level the workload to 80 - 130.

Students are expected to have some background in programming language semantics though lectures will also cover this, so it is not mandatory. No background in security is expected. 

---

Registration and Attendance

Registration for the course is mandatory, course registration is currently closed, you should first register at this page: https://cms.cispa.saarland/metasem18/ 

After you register at that url, please send an email to the lecturer (see below), explaining your background in programming languages and security as well as the department and program (Bachelors, Masters, PhD) in which you are enrolled. Indicate whether or not you would like UdS credits for the course. Like all seminars, the final list for the course will be decided at the beginning of the semester.
During the first two weeks (20/04 is the last day), if you are registered you can drop the seminar with no consequences, but you must notify the lecturer. On the contrary, if you stay longer, or if you do not notify the lecturer, then you fail.

The seminar can host up to 13 students.

---

Location, Time Slot and Lecturer

Location: CISPA, campus E9 1, Floor 2, room 22 (so: 2.22).

Time Slot: 

• Mondays, 16:00 (16:15) to 18:00 
• Thursdays 12:00 (12:15) to 14:00

The first lecture is on 12/04/2018 from 12:00 to 14:00 in the designated location.

Lecturer: Dr. Marco Patrignani (see homepage for details)

Assistant: Akram El-Korashy (see homepage for details)

---

Evaluation and Grading

For each paper every student will provide a paper summary to the lecturer and then one student will lead the discussion. The rest of the class will be the audience, providing questions, answers and clarifications.

Thus, a student's grade is split accordingly:

• paper presentation 30 %
• paper summaries (see guidelines below): 50%
• in-class participation: 20%

 

Good paper summaries must include the following and be concise while retaining clarity. 

• Context and Background: What is the domain of the work? Is there any basic concept to mention for understanding the paper?
• Problem: What is the problem being addressed in the paper? Why is a difficult problem? (Problem Statement and Challenges) Why did the authors decide to consider it? (Motivation) 
• Main Idea: What is the main idea of the authors presented in the paper? 
• Contribution: How does this paper advance the state of the art? What is exactly new and valuable in the paper?
• Evaluation: Precisely describe the languages, compiler and proof techniques adopted by the authors.
• Pros and Cons: Provide your opinion about what you think is good about the paper and what are the weaknesses. Likewise, report any limitation and possible ideas for improving the paper.

 

---

List of Papers

This is the list of papers you should pick from:

1. Pieter Agten, Raoul Strackx, Bart Jacobs, and Frank Piessens. 2012. Secure Compilation to Modern Processors.
2. Marco Patrignani, Dave Clarke, and Frank Piessens. 2013. Secure Compilation of Object-Oriented Components to Protected Module Architectures.
3. Marco Patrignani, Dominique Devriese, and Frank Piessens. 2016. On Modular and Fully Abstract Compilation.
4. Martín Abadi, Cédric Fournet, and Georges Gonthier. 1999. Secure Communications Processing for Distributed Languages.
5. Martín Abadi, Cédric Fournet, and Georges Gonthier. 2000. Authentication Primitives and their Compilation.
6. Martín Abadi, Cédric Fournet, and Georges Gonthier. 2002. Secure Implementation of Channel Abstractions.
7. Martín Abadi and Gordon D. Plotkin. 2012. On Protection by Layout Randomization.
8. Marco Patrignani and Deepak Garg. 2017. Secure Compilation as Hyperproperty Preservation.

 

---

Class Outline

We will provide the following lectures

• L1: Introduction to secure compilation, program equivalences as means to express security properties, fully abstract compilation
  • We will see examples of programs and how program equivalence can be used to specify security properties. We will then see how to use program equivalence to define fully abstract compilation (FAC). We will show why that makes FAC a secure compilation criterion.
• L2: (optional) Background on programming languages and semantics
  • We'll cover the basics of while languages syntax and semantics, both big and small steps. We'll have explanatory examples for both subjects.
• L3: (optional) Background on programming languages and semantics
  • We'll cover typing for expressions and statements of while programs and we'll see how to add features to while languages such as named functions and return statements. We'll have explanatory examples for these subjects.
• L4: Protected modules architectures (PMAs)
  • We'll describe how are PMAs realised and the kind of access control policies they enforce. We'll see examples of how PMA work and we'll see how to describe a PMA and how to reason about it. 
• L5: Protected modules architectures (if needed)
  • If needed, we'll finish topics from the previous lecture. Otherwise there'll be no lecture and on L4 we'll decide if to skip or to shift L6 here.
• L6: General (and gentle) introduction to proofs and to fully abstract compilation proofs
  • We'll cover the basics of induction and understand why we need to prove things. We'll discuss how to reason about fully abstract compilation proofs and why they are complicated. We'll define trace semantics and see how we can use it to make fully abstract compilation proofs simpler.
• L7: The backtranslation proof technique and its application to secure compilation
  • We will discuss trace-based backtranslation and why it can be used to prove fully abstract compilation. We'll go in the details of the backtranslation tool by means of examples and understand how and why it works.
• L8: Introduction to Process Algebra and Bisimulation
  • We will describe the foundations of concurrent and distributed programming and their relevance as opposed to batch programming. We will see how reasoning about concurrent systems introduces a number of concerns that do not exist in for sequential ones and how to perform this reasoning using bisimulation techniques.
• L9: Join and SJoin calculi
  • We will cover the basics about join and sjoin calculi: syntax, semantics, examples of programs (processes!) and of reductions. We will define bisimulation and equivalences between processes and how to reason about their behaviour. We will see how to use join and sjoin processes to model secure protocols.
• L10: Security protocols and reasoning about Join processes (if needed)
  • We will see how to use join and sjoin processes to model secure protocols. Possibly this will be discussed in L9, and we'll also see whether to skip L10 or shift L11.
• L11: Beyond fully abstract compilation and other means to express secure compilation
  • We will discuss properties (in the world of traces), specifically safety properties and how they can express security properties. We will see how to reason about source and target safety properties and how to preserve their intended meaning. Possibly, we will see how to extend this reasoning to liveness properties and to hypersafety.

 

The seminar will follow this outline:

• 12th of April: Kickoff Meeting: we'll see to agree on the lecture slots and assign the papers

Below is the week number together with the lecture number (L1, L2 ...) or the presentation number (P1, P2 ...) to be done that week. PN refers to the presentation of the Nth paper from the list above. The two slots refer to the two lecture slots described well above. When there is an X it means that slot happens on a public holiday, so no class that day.

1.  L1  L2
2.  L3  L4
3.  X(lecturers away)  L5(skipped)
4.  L6  X(10th of may)
5.  X  X (lecturers away on conference)
6. X(21st of may)  L7
7. L7bis  X(31st of may)
8. P1 L8 
9. L9  P2
10. P3  L11
11. P4+5  P6
12. P7+8

Please note that this is a rough overview of the schedule, which may vary.

Some presentations will be done jointly to a maximum of 2 presentations per slot, given that they are on related topics (they are marked with a +).