Gilles Barthe

Building secure cryptographic implementations is notoriously hard. In this talk, I will outline a general methodology that delivers formal guarantees on assembly-level implementations through a combination of ideas from deductive program verification...