Language techniques for secure compilation

MPI-SWS/Saarland University
Winter 2016/17

Time: TBD
Location: TBD

Instructors: Deepak Garg, Marco Patrignani

Language: English

Overview and prerequisites

This course will explore programming language techniques in 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 assembly-level attackers are inherently more powerful than attackers in the source language. The course will focus on correctness criteria for secure compilation and programming language techniques for proving that a specific compiler satisfies one or more of those criteria. We expect to cover topics like full abstraction, cross-language logical relations and back translations.

This is NOT a standard seminar. The goal is to develop some depth in the area, not just breadth. The course will combine paper reading, in-class (round table) discussions, student presentations, lectures and homeworks to enable participants to understand the material. Students are expected to have some background in programming language semantics and inductive proofs. No background in security is expected.

More details on the course structure will be provided soon. For a rough idea, take a look at this course, which was structured similarly. Non-credit participation is welcome.


To register, send an email to the course instructors, 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.