Security
How To Minimize Bugs in Cryptography Code
"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.
Weitere Infos
| Live Stream | https://streaming.media.ccc.de/39c3/zero |
|---|---|
| Format | Talk |
| Sprache | Englisch |
Weitere Sessions
| 27.12.25 |
The Great Firewall of China (GFW) is one of, if not arguably the most advanced Internet censorship systems in the world. Because repressive governments generally do not simply publish their censorship rules, the task of determining exactly what is and isn’t allowed falls upon the censorship measurement community, who run experiments over censored networks. In this talk, we’ll discuss two ways censorship measurement has evolved from passive experimentation to active attacks against the Great ...
|
| 27.12.25 |
Reports of GNSS interference in the Baltic Sea have become almost routine — airplanes losing GPS, ships drifting off course, and timing systems failing. But what happens when a group of engineers decides to build a navigation system that simply *doesn’t care* about the jammer? Since 2017, we’ve been developing **R-Mode**, a terrestrial navigation system that uses existing radio beacons and maritime infrastructure to provide independent positioning — no satellites needed. In this talk, ...
|
| 27.12.25 |
Zwei Jahre nach dem ersten KIM-Vortrag auf dem 37C3: Die gezeigten Schwachstellen wurden inzwischen geschlossen. Weiterhin können mit dem aktuellen KIM 1.5+ nun große Dateien bis 500 MB übertragen werden, das Signaturhandling wurde für die Nutzenden vereinfacht, indem die Detailinformationen der Signatur nicht mehr einsehbar sind. Aber ist das System jetzt sicher oder gibt es neue Probleme?
|
| 27.12.25 |
While trying to apply fault injection to the AMD Platform Security Processor with unusual (self-imposed) requirements/restrictions, it were software bugs which stopped initial glitching attempts. Once discovered, the software bug was used as an entry to explore the target, which in turn lead to uncovering (and exploiting) more and more bugs, ending up in EL3 of the most secure core on the chip. This talk is about the story of trying to glitch the AMD Platform Security Processor, then ...
|
| 27.12.25 |
The Deutschlandticket was the flagship transport policy of the last government, rolled out in an impressive timescale for a political project; but this speed came with a cost - a system ripe for fraud at an industrial scale. German public transport is famously decentralised, with thousands of individual companies involved in ticketing and operations. Unifying all of these under one national, secure, system has proven a challenge too far for politicians. The end result: losses in the hundreds of ...
|
| 27.12.25 |
In August 2024, Raspberry Pi released their newest MCU: The RP2350. Alongside the chip, they also released the RP2350 Hacking Challenge: A public call to break the secure boot implementation of the RP2350. This challenge concluded in January 2025 and led to five exciting attacks discovered by different individuals. In this talk, we will provide a technical deep dive in the RP2350 security architecture and highlight the different attacks. Afterwards, we talk about two of the breaks in ...
|
| 27.12.25 |
FreeBSD’s jail mechanism promises strong isolation—but how strong is it really? In this talk, we explore what it takes to escape a compromised FreeBSD jail by auditing the kernel’s attack surface, identifying dozens of vulnerabilities across exposed subsystems, and developing practical proof-of-concept exploits. We’ll share our findings, demo some real escapes, and discuss what they reveal about the challenges of maintaining robust OS isolation.
|
