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

[Aviral Goel]

Reminder, the seminar is happening in 30 minutes.

Best,
Aviral


On Fri, Mar 1, 2019 at 2:12 PM Aviral Goel <goel.av at husky.neu.edu> wrote:

> *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