Write a Blog >>
Thu 22 Jun 2017 09:15 - 10:00 at Vertex WS216 - Intro & industry perspective on crypto Chair(s): Andrew W. Appel

Large commercial organizations have good reason to take the correctness of their cryptography seriously. The largest even employ “cryptography wizards”, experts in the field who are qualified to roll their own heavily optimized implementations. As skilled as these experts are, their work rarely comes with a formal, mathematical proof of implementation correctness.

I’ll discuss Google’s interest in formally verified implementations of cryptography and our experiences with an internship that focused on ECC curve P256. This project successfully verified modular arithmetic on the curve down to the specific machine representation – the register level – for an idealized bignum processor known as “Fancy Machine”.

We were able to use this experience with a different type of expert, one skilled in the art of formal verification, to build greater certainty in a prior implementation of the same curve. This is the story of the cryptography experts who told us what to prove and the formal verification experts who told us how to go about doing so.

Thu 22 Jun

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 10:00
Intro & industry perspective on cryptoDSW at Vertex WS216
Chair(s): Andrew W. Appel Princeton
09:00
15m
Day opening
Introduction to DeepSpec
DSW
Lennart Beringer Princeton University, Adam Chlipala Massachusetts Institute of Technology, USA
09:15
45m
Talk
Building Faith in Experts: Applying Formal Verification to Cryptography
DSW