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.
Registration
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.