Title:

CryptoBAP: Verifying closed-source protocol implementations

 

Abstract:

We present CryptoBap, a platform to verify weak secrecy and authentication for the (ARMv8 and RISC-V) machine code of cryptographic protocols. We achieve this by first transpiling the binary of protocols into an intermediate representation and then performing a crypto-aware symbolic execution to automatically extract a model of the protocol that represents all its execution paths. Our symbolic execution resolves indirect jumps and supports bounded loops using the loop-summarization technique, which we fully automate. The extracted model is then translated into models amenable to automated verification via ProVerif and CryptoVerif using a third-party toolchain or, more recently, into SAPIC+, which soundly translates to ProVerif, Tamarin. The latest proof is fully mechanized in HOL-4. Robert will talk the challenges of doing so, and about new principles for combining multiple programming languages operating on different atomic types that made the proofs manageable.

Bio:

Robert Künnemann obtained his Ph.D. from École normale supérieure de Cachan under the supervision of Steve Kremer and Graham Steel. He worked within the SECSI and PROSECCO teams at INRIA (Paris, France), interned at Cambridge University, UK and held positions at Technical University Darmstadt and Saarland University (Germany). Since 2019, he is a research group leader at CISPA. His specialties are protocol verification, accountability and infrastructure analysis.

 

Speaker:

Robert Künnemann

Ph.D.

Independent Group Leader, CISPA Helmholtz Center for Information Security