How To Minimize Bugs in Cryptography Code (39c3)

"Don't roll your own crypto" is an often-repeated aphorism. It's good advice -- but then how does any cryptography get made? Writers of cryptography code like myself write code with bugs just like anyone else, so how do we take precautions against our own mistakes? In this talk, I will give a peek into the cryptographer's toolbox of advanced techniques to avoid bugs: targeted testing, model checking, mathematical proof assistants, information-flow analysis, and more. None of these techniques is a magic silver bullet, but they can help find flaws in reasoning about tricky corner cases in low-level code or prove that higher-level designs are sound, given a defined set of assumptions. We'll go over some examples and try to give a high-level feel for different workflows that create "high-assurance" code. Whether you know it or not, you use this type of cryptography code every day: in your browser, your messaging apps, and your favorite programming language standard libraries. Over the last 10 years or so, using mathematical proof assistants and other formal-logic tools for cryptography code has gone from a relatively new idea to standard practice. I've been lucky enough to have a front-row seat to that transformation, having started doing formal-methods research in 2015 and then switched to a focus on cryptography implementation since 2021. Code from my master's thesis project, ["fiat-crypto"](https://github.com/mit-plv/fiat-crypto), is [included](https://andres.systems/fiat-crypto-adoption.html) in every major browser as well as AWS, Cloudflare, Linux, OpenBSD, and standard crypto libraries for Go, Zig, and Rust (RustCrypto, dalek). In addition to verifying code correctness, designers of high-level protocols like Signal's recently announced post-quantum ratchet increasingly use mathematical tools (ProVerif in Signal's case) to check their work. Despite the growing popularity of these formal techniques and their relevance to personal information security, few people are aware of them, and they maintain a reputation for being hard to learn and esoteric. I'd like to demystify the topic and show examples of how anyone can use proof assistants in small, standalone ways as part of the coding or design process. My hope is that next time a colleague asks for review of a complex high-speed bit-twiddling algorithm, instead of staring at the code line-by-line, attendees of my talk will know they can write a computer-checked proof to confirm or deny that the algorithm achieves its intended result. Licensed to the public under http://creativecommons.org/licenses/by/4.0 about this event: https://events.ccc.de/congress/2025/hub/event/detail/how-to-minimize-bugs-in-cryptography-code