News
Tomorrow's presentationsWritten on 08.10.19 by Marco Patrignani Dear students, tomorrow's presentations will start at 13:30. please have the laptops set up by then.
marco |
Schedule for Monday and TuesdayWritten on 04.10.19 by Marco Patrignani Dear students, this is the schedule for the presentations of next week. Leave at least 10/15 minutes for discussion in your talks. Monday: 13:15 : paper 3 14:00 : paper 10 14:45 : paper 12 15:30 :… Read more Dear students, this is the schedule for the presentations of next week. Leave at least 10/15 minutes for discussion in your talks. Monday: 13:15 : paper 3 14:00 : paper 10 14:45 : paper 12 15:30 : paper 14 16:15 : paper 15 Tuesday: 13:15 : paper 16 14:00 : paper 17 14:45 : paper 19
The students of papers 5 and 10 have not shown up, and i doubt they will. If they manifest themselves, they will be added after paper 9. |
MaterialWritten on 29.09.19 by Marco Patrignani Dear students, slides and lecture notes are now available on my webage: http://theory.stanford.edu/~mp/mp/Teaching.html in the 2018-2019 year.
see you tomorrow. |
Room announcementWritten on 28.09.19 by Marco Patrignani Dear students, the room of the seminar will be 0.06 at cispa.
see you next week. |
Practical informationWritten on 24.09.19 (last change on 25.09.19) by Marco Patrignani Dear students, here is some practical information for the course: - the first week of the course will be classes: monday, tuesday, wednesday and friday.
Each presentation will be 40 minutes in total: prepare a talk… Read more Dear students, here is some practical information for the course: - the first week of the course will be classes: monday, tuesday, wednesday and friday.
Each presentation will be 40 minutes in total: prepare a talk with slides for 25 minutes and then we'll have 15 minutes for discussions. We'll have a 5 minutes break between each presentation so that you can set up your pc. Monday we'll have 6 presentations, tuesday we'll have 4.
Concerning reports/summaries, 2 pages per paper should suffice. Remember that all summaries must be turned in in 2 sundays. All of them, no extensions. |
ClarificationWritten on 14.07.19 by Marco Patrignani Dear students, i wanted to clarify that the papers to be summarised are only those that will be discussed in class, so only 10 of the 19 in the list. Specifically, they are numbers: 3 5 10 11 12 14 15 16 17 19. best -mp |
Secure Compilation (BLOCK Seminar)
This seminar will explore the nascent field of secure compilation.
The goal of secure compilation is to compile programs so as to preserve source security properties like data confidentiality and code integrity. This is challenging because attackers operating at the level of the compiler output are inherently more powerful than attackers in the source language.
This seminar will describe correctness criteria for secure compilation, specific instances of secure compilers as well as proof techniques for secure compilation.
Correctness criteria define that a compiler is secure. The seminar will explain why can we be sure that a criterion has any security meaning, i.e., what kinds of attacks can be defended against (and which not). Secondly, the seminar will discuss specific instances of secure compilers and how they achieve security, i.e., what mechanism (types, crypto, security architecture, etc.) do these compilers exploit to realise one of the presented criteria. Finally the seminar will cover basic proof techniques for secure compilation, i.e., how do you formally prove that a compiler is secure.
This is not a standard seminar, it includes Lectures.
Previous Offerings of this Seminar
- 2018 at CISPA: https://cms.cispa.saarland/sc101/
- 2019 at Stanford: http://theory.stanford.edu/~mp/mp/CS350-2018.html
Location, Time Slot and Lecturer
Location: CISPA, campus E9 1, TBD
Time Slot:
- every day from MON 30th of September 2019 to TUE 8th of October 2019
- that is MON 30, TUE 1, WED 2, THU 3, FRI 4, MON 7, TUE 8,
- 4:30 hours per day, including breaks, so every day from 13:00 to 17:30 (with some 15 minutes break)
While the class is held mostly in October, paper assignment is done in May, please see below for all dates.
The first lecture is Monday 30th of September 2019
Lecturer: Dr. Marco Patrignani (http://theory.stanford.edu/~mp/mp/Home.html, find my email in my website)
Registration and Attendance
Registration for the course is mandatory, course registration is currently closed, you should first register at this page: TBD
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.
See below for information about dropouts.
The seminar can host up to 19 students.
Paper Preferences and Dropouts
Given the block nature of the course, students must to provide their preferences ahead of time. That will give us ample time to assign papers to students, which in turn will give you ample time to read the papers ahead of time and not rush. Also, the early assignment of papers simplifies the logistics of the course.
The deadline for submitting paper preferences is
FRI 3rd May 2019
Each paper has a related tutorial from the tutorial list. Assign your preferences to all tutorials based on your paper preferences. We'll then use the built-in distribution algorithm to ensure tutorials are distributed fairly amongst students, according to your preferences.
You can expect the paper assignment to be known before the course starts, likely on MON 6th May 2019.
The deadline for dropping out of a seminar is formally 3 weeks after each student is assigned a paper, therefore by the time the seminar is held, no dropouts is available. The last day for dropping out of the seminar is:
MON 27rd May 2019
Evaluation, Grading, Deadlines
Course evaluation is based on the presentation and summary of research papers as well as the ability to relate said papers to the notions presented in class.
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%
The deadline for submitting all paper summaries is
SUN 6th October 2019
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 to pick from:
- Abadi and Plotkin. 2012. On Protection by Layout Randomization.
- Jagadeesan et al 2011. Local Memory via Layout Randomization.
- Patrignani and Garg. 2017. Secure Compilation as Hyperproperty Preservation.
- Devriese et al. 2016. Fully-Abstract Compilation by Approximate Back-Translation.
- New et al. 2016. Fully Abstract Compilation via Universal Embedding.
- Fournet et al. 2013. Fully Abstract Compilation to JavaScript.
- Bowman et al. 2015. Noninterference for free.
- Juglaret et al. 2016. Beyond Good and Evil: Formalizing the Security Guarantees of Compartmentalizing Compilation
- Abate et al. 2018. When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise.
- Patterson et al. 2017. FunTAL: Reasonably Mixing a Functional Language with Assembly.
- J. B. Almeida et al. 2017. Jasmin: High- assurance and high-speed cryptography.
- G. Barthe et al. 2018. Secure compilation of side-channel countermeasures: the case of cryptographic “constant-time”.
- Abate et al. 2018. Journey beyond Full Abstraction: Exploring Robust Property Preservation for Secure Compilation.
- Patrignani and Garg. 2019. Robustly Safe Compilation.
- Agten et al. 2012. Secure Compilation to Modern Processors.
- Patrignani et al. 2013. Secure Compilation of Object-Oriented Components to Protected Module Architectures.
- Patrignani et al. 2016. On Modular and Fully Abstract Compilation.
- Ahmed and Blume. 2011. An Equivalence-Preserving CPS Translation via Multi-Language Semantics.
-
Ahmed and Blume. 2008. Typed Closure Conversion Preserves Observational Equivalence.
Class Outline
We will provide the following lectures that introduce key notions used throughout the papers to read (please note that given the block nature of the course, the same day can host multiple lectures)
- L1: introduction to secure compilation, program equivalences as means to express security properties, fully abstract compilation
- L2: traces as means to express security properties, robust compilation
- L3: preserving the meaning of safety and hypersafety properties through compilation
- L4: background on programming languages and semantics (while language)
- L5: In-class example: devising and proving fully abstract compilation between simple languages
- L6: In-class example: devising and proving robustly-safe compilation between simple languages, comparison between the two examples for efficiency and proof complexity
- L7 (possibly): the PMA case study: fully abstract compilation for SGX-like security architectures
Once these lectures are covered, we will have students presentation on their chosen papers.
The (tentative) schedule is:
| FRI 3rd May | paper preferences are sent to the instructor | |
| ... | ||
| MON 6th May | paper assignments are communicated to students | |
| ... | ||
| MON 27th May | last day to drop out of class | |
| ... | ||
| MON 30th September | class starts | |
| TUE 1st October | ||
| WED 2nd October | ||
| THU 3rd October | no class | |
| FRI 4th October | ||
| SUN 6th October | last day to turn in all paper summaries | |
| MON 7th October | student presentations | |
| TUE 8th October | student presentations | class ends |