Vincent Laporte will give a talk at the Grace seminar on tuesday, march 12 at 13h30 in Salle Henri Poincaré.

Abstract: High-efficiency low-level programming — and in particular the implementation of cryptographic primitives — challenges formal verification methods for correctness and security of the implementations. To overcome this difficulty, the Jasmin language and compiler provide high-level abstractions and predictability of the generated assembly so as to write verifiable efficient low-level programs. The compiler is also formally verified in Coq so as to enable reasoning about functional correctness at the source level. Moreover we’ll present in this talk a proof methodology to enable reasoning about side-channel attack resistance at the source level: building on compiler correctness arguments, we show how to justify preservation, along the compilation process, of the constant-time property.