Secure Compilation Marco Patrignani

News

Currently, no news are available
 

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.
In order to enable participants to understand the material fully and better, the course will combine paper reading (at home), round table discussions with student presentations (in class), as well as lectures (in class, before presentations) 

Previous Offerings of this Seminar

To have an idea of what this seminar looks like, you can take a look at its previous offerings:

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)


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.

Non-credit participation is welcome.
 
Attendance is mandatory for getting credit hours. If for any reason you cannot attend, notify the lecturer in time. Absence for sickness is of course tolerated, though a proper medical note must be provided (and notification is anyway needed).

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

Once the preferences are known, we will assign papers to students and let them know their assignments. You can expect this 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:

  1. Abadi and Plotkin. 2012. On Protection by Layout Randomization.
  2. Jagadeesan et al 2011. Local Memory via Layout Randomization.
  3. Patrignani and Garg. 2017. Secure Compilation as Hyperproperty Preservation.
  4. Devriese et al. 2016. Fully-Abstract Compilation by Approximate Back-Translation.
  5. New et al. 2016. Fully Abstract Compilation via Universal Embedding. 
  6. Fournet et al. 2013. Fully Abstract Compilation to JavaScript. 
  7. Bowman et al. 2015. Noninterference for free. 
  8. Juglaret et al. 2016. Beyond Good and Evil: Formalizing the Security Guarantees of Compartmentalizing Compilation
  9. Abate et al. 2018. When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise. 
  10. Patterson et al. 2017. FunTAL: Reasonably Mixing a Functional Language with Assembly. 
  11. J. B. Almeida et al. 2017. Jasmin: High- assurance and high-speed cryptography. 
  12. G. Barthe et al. 2018. Secure compilation of side-channel countermeasures: the case of cryptographic “constant-time”. 
  13. Abate et al. 2018. Journey beyond Full Abstraction: Exploring Robust Property Preservation for Secure Compilation.
  14. Patrignani and Garg. 2019. Robustly Safe Compilation.
  15. Agten et al. 2012. Secure Compilation to Modern Processors.
  16. Patrignani et al. 2013. Secure Compilation of Object-Oriented Components to Protected Module Architectures.
  17. Patrignani et al. 2016. On Modular and Fully Abstract Compilation.
  18. Ahmed and Blume. 2011. An Equivalence-Preserving CPS Translation via Multi-Language Semantics.
  19. 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 L1 L2(part) class starts
TUE 1st October L2(end) L3  
WED 2nd October L4 L5(part)  
THU 3rd October L5(end)  
FRI 4th October L6  
SUN 6th October   last day to turn in all paper summaries
MON 7th October student presentations (or L7)  
TUE 8th October student presentations class ends


Privacy Policy | Legal Notice
If you encounter technical problems, please contact the administrators