If you suspend your transcription on amara.org, please add a timestamp below to indicate how far you progressed! This will help others to resume your work!
Please do not press “publish” on amara.org to save your progress, use “save draft” instead. Only press “publish” when you're done with quality control.
Standard testing and fuzzing catch many bugs, but they don't catch all bugs. Masochists try to formally prove that crypto software does its job. Sadists try to convince you to do your own proof work and to let them watch. After years of pain, a team of fifteen authors has now proudly announced a verified crypto library: fast but unportable implementations of a few cryptographic functions specifically for CPUs that aren't in your smartphone. This is progress, but the progress needs to accelerate.
This talk will highlight a way to exploit the power of modern reverse-engineering tools to much more easily verify crypto software. This relies on the software being constant-time software, but we want constant-time software anyway so that we can guarantee security against timing attacks. Constant-time software is also surprisingly fast when cryptosystems are selected carefully.
This talk is meant as an introduction for a general audience, giving self-contained answers to the following questions: What are timing attacks? What is constant-time software? What are some examples of constant-time crypto? How can we be sure that code is constant-time? What do these reverse-engineering tools do? How does constant-time code help these tools? How do we get from reverse engineering to guaranteeing correctness?
The talk will be given as a joint presentation by Daniel J. Bernstein and Tanja Lange.