Organizer: CRISP / CROSSING
Building secure cryptographic implementations is notoriously hard. In this talk, Prof. Gilles Barthe will outline a general methodology that delivers formal guarantees on assembly-level implementations through a combination of ideas from deductive program verification, program analysis, and verified compilation.
He will also outline the relevance of formal methods and programming languages in the broader context of cryptography.
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 is a scientific director at Max Planck Institute, Germany, and a part-time research professor at the IMDEA Software Institute, which he joined in April 2008.
His research interests include programming languages and program verification, software and system security, cryptography, formal methods and foundations of mathematics and computer science. His recent research develops programming language techniques and verification methods for security, with a focus on cryptographic implementations and differentially private computations.
Distinguished Lectures Series in Cybersecurity
With the Distinguished Lectures Series in Cybersecurity, every semester, we invite outstanding experts from science and industry to Darmstadt to discuss the multifaceted prospects and challenges of IT Security. In the lectures, the speakers present the results of trendsetting research from a variety of disciplines, give overviews of complex topics or show the current state of knowledge in their field of research. The lectures are free and open for everybody without prior registration.
After the lecture there is the possibility to get together.