A Compiler for Security

Tamara Rezk

The area of provable or computational cryptography that started to develop since the early 90s proposes that the only assumptions on the adversary that can be justified are his/her computational abilities. Reasoning with arbitrary adversaries involves the handling of polynomial and probabilistic hypotheses on complex programs. Can we let the programmer specify security policies at an abstract level and let the compiler implement them using provable cryptography? This presentation will describe work in progress with Cedric Fournet and Gurvan Le Guernic on programming language abstractions for provable cryptography, and a compiler that implements it.