- You are subscribed to this talk through .
- You are watching this talk through .
- You are subscribed to this talk. (unsubscribe, watch)
- You are watching this talk. (unwatch, subscribe)
- You are not subscribed to this talk. (watch, subscribe)
Computer-aided cryptography advocates the adoption of computer-aided proofs for certifying the security of cryptographic constructions. In this talk, I will outline our earlier work on developing relational program logics for reasoning about probabilistic computations with adversarial code, and present our more recent efforts to carry the security guarantees down to implementation level, using advances in verified compilation and verified static analyses. I will also outline some limitations of the approach.
Gilles Barthe received a Ph.D. in Mathematics from the University of Manchester, UK, in 1993, and an Habilitation à diriger les recherches in Computer Science from the University of Nice, France, in 2004. He joined the IMDEA Software Institute in April 2008. Previously, he was head of the Everest team on formal methods and security at INRIA Sophia-Antipolis Méditerranée, France. He also held positions at the University of Minho, Portugal; Chalmers University, Sweden; CWI, Netherlands; University of Nijmegen, Netherlands. He has published more than 100 refereed scientific papers. He has been coordinator/principal investigator of many national and European projects, and served as the scientific coordinator of the FP6 FET integrated project "MOBIUS: Mobility, Ubiquity and Security" for enabling proof-carrying code for Java on mobile devices (2005-2009). He has served as PC (co-)chair of VMCAI 2010, ESOP 2011, FAST 2011, SEFM 2011 and ESSOS 2012, and been a PC member of more than 70 conferences, including CCS, CSF, EUROCRYPT, ESORICS, FM, ICALP, LICS, and POPL. He is a member of the editorial board of the Journal of Automated Reasoning and of the Journal of Computer Security.
His research interests include programming languages and program verification, software and system security, cryptography, formal methods and foundations of mathematics and computer science. Since joining IMDEA, his research has focused on building foundations for computer-aided cryptography and privacy and on the development of tools for proving the security of cryptographic constructions and differentially private computations. He was awarded the Best Paper Award at CRYPTO 2011 and PPoPP 2013, and was an invited speaker at numerous venues, including CSF, ESORICS, ETAPS, FAST, ITP, QEST and SAS.