[Pl-seminar] 6th March: David Pichardie: Verification of constant-time implementations in a verified compiler toolchain

[Aviral Goel]

*Date:* Wednesday, March 6th 2019
*Location:* WVH 366
*Time:* 10:00 AM to 11:30 AM
*Speaker:* David Pichardie
*Faculty Host:* Jan Vitek

*Verification of constant-time implementations in a verified compiler
toolchain
<http://prl.ccs.neu.edu/seminars.html#pichardie-verification-of-constant-time-implementations-in-a-verified-compiler-toolchain>*
*David Pichardie*



*Abstract*Constant-time programming is an established discipline to secure
programs against timing attackers. Several real-world secure C libraries
such as NaCl, mbedTLS, or Open Quantum Safe, follow this discipline. We
propose two advanced compile-time verification techniques to enforce this
discipline. The first one operates at assembly level with help from alias
informations that are computed at source level and transmitted by the
compiler. The second one operates at source level, using advanced abstract
interpretation techniques. For this last approach, we also study how to
ensure that the compiler will not break the property during compilation.
These techniques have been implemented in the CompCert compiler toolchain
and tested on several crypto libraries. These works have been presented at
CCS’14, CSF’17 and ESORICS’17.

*Bio*

I am professor of Computer Science and head of the Department of Computer
Science at ENS Rennes. My research activities take place in the Celtique
team (joint team between University of Rennes, ENS Rennesand Inria Rennes,
under the IRISA joint lab). I received a Ph.D. in Computer Science from the
University of Rennes, France, in 2005, and a Habilitation à diriger les
recherches in Computer Science from the ENS Cachan, France, in 2012. I
joined ENS Cachan in September 2013 as full professor (in 2014, the
brittany extension of ENS Cachan has becomed ENS Rennes). Between 2007 and
2013, I was a full research at INRIA Rennes research center. Earlier, I was
holding a postdoc position at INRIA Sophia-Antipolis under the supervision
of Gilles Barthe. In the 2011-13 academic years, I took a sabbatical and
visited Jan Vitek's group at Purdue University, Indiana, USA, during the
first year, and then Greg Morrisett's group at Harvard University,
Cambridge, USA, during the second year. My research interests include
formal methods, programming languages, program verification, software, and
system security. I am a long time happy user of the Coq proof assistant and
the theory of Abstract interpretation. More recently I have been conducting
several researches about the verified C compiler CompCert. My research is
currently funded by an ERC Consolidator Grant "VESTA: VErified STatic
Analysis platform" (2018-2023).


Best,
Aviral
-------------- next part --------------
HTML attachment scrubbed and removed