Seminário Segurança de Informação 

24/10/2008, 16:30 — 17:30 — Sala P3.10, Pavilhão de Matemática
Tamara Rezk, INRIA, Sophia-Antipolis

A Provably Secure Cryptographic Compiler

It is common knowledge that cryptographic schemes are constructed to resist attacks guided by malicious attempts to deviate some intended functionality. However, very little is known about the level of security that we get by using cryptographic schemes in different environments, since security depends on the strength of the adversary. How much can we assume about an unknown adversary without compromising security? On one hand, many works that aim at proving that programs which use cryptography are secure assume specific strategies that the adversary may or may not use when attacking the system. Unfortunately, experience shows that limitations to the power of the adversary are not always realistic. On the other hand, 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 talk 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. A preliminary result of this work appeared in POPL'08.