How To Minimize Bugs in Cryptography Code

How To Minimize Bugs in Cryptography Code

Speakers: Jade

Conference: 39C3

YouTube: https://www.youtube.com/watch?v=Lbs88JvGdrs

Overview

In this insightful talk, Jade tackles a critical challenge in cybersecurity: minimizing bugs in cryptography code. While the common adage "don't roll your own crypto" rightly advises developers to use well-established libraries, these foundational implementations don't appear out of thin air. They are meticulously crafted by experts, becoming high-impact targets for attackers due to their widespread use. The talk confronts the uncomfortable truth that even highly skilled cryptographers and programmers make mistakes, and bugs in cryptographic implementations can be exceptionally subtle, persisting undetected for years.

Jade’s presentation serves as a comprehensive tour through an "invisible ecosystem of tools" designed to increase confidence in cryptographic code. It explores a spectrum of techniques, from basic testing to advanced formal methods, illustrating how each step demands progressively more effort but yields a significantly higher level of assurance. The core message is a call to action for developers and security professionals to understand and adopt these sophisticated techniques, recognizing their increasing normalization and crucial role in securing the digital infrastructure that underpins our daily lives.

The talk not only dissects the capabilities and workflows of these tools but also highlights their growing prevalence in widely used cryptographic libraries and protocols, including OpenSSL, SSH, BoringSSL, HACL\*, and even standard libraries in languages like Go, Python, Zig, and Rust. By demystifying these high-assurance methods, Jade empowers the audience to better understand the security foundations of the internet and encourages their adoption to build more resilient and trustworthy systems.

Background

▶ Watch: Introduction: Minimizing bugs in cryptography code (0:00)

The security landscape is heavily reliant on robust cryptographic implementations. The prevailing wisdom, "don't roll your own crypto," encourages developers to leverage battle-tested, peer-reviewed cryptographic libraries rather than attempting to write their own from scratch. This advice is sound, as the complexities of cryptography often lead to subtle, exploitable vulnerabilities when implemented incorrectly. However, this raises a fundamental question: who writes and ensures the security of these trusted libraries?

The reality is that a select group of highly skilled individuals must, at some point, write this critical cryptography code. These implementations, by virtue of their widespread adoption, become incredibly high-impact targets for attackers. A single vulnerability in a core cryptographic library can have catastrophic consequences across countless applications and systems. Compounding this challenge is the nature of cryptographic bugs; they are often not immediately obvious. They can arise from intricate interactions between components, subtle timing discrepancies, or rarely triggered corner cases, remaining dormant and exploitable for years before discovery.

To address this, Jade introduces the concept of an "effort versus quality trade-off" in code assurance. Initial efforts, such as compiling code and running basic tests, yield a significant jump in confidence from zero. However, achieving the "last mile" of confidence—the level required for critical components like an operating system kernel or a TLS connection—demands exponentially more effort for incrementally smaller gains in assurance. This talk delves into the specialized tools and techniques that operate in this high-effort, high-assurance space, moving beyond conventional software testing to address the unique and stringent security requirements of cryptography.

Key Findings

▶ Watch: Initial steps: writing basic tests for crypto code (2:50)

The talk reveals that the journey to minimizing bugs in cryptography code is a progression through increasingly sophisticated and effort-intensive assurance techniques. A primary finding is the inherent limitations of basic and even advanced random testing for cryptographic implementations. Due to the astronomically large input spaces of cryptographic functions, random testing can never cover a significant portion of possibilities, leaving critical corner cases and subtle vulnerabilities, particularly those related to timing, undiscovered.

Jade meticulously outlines a spectrum of tools and methodologies that address these limitations:

1. Clever Testing: Moving beyond pure randomness, this involves using curated test vectors (like those found in Witch Proof), which are designed to trigger known past bugs or specific corner cases. Coverage-guided fuzzing is introduced as a more advanced form of testing that intelligently generates inputs to ensure every line of code, and thus every execution path, is exercised.

1. Static Analysis: This category represents a significant leap, analyzing the program's logic without executing it. Basic forms include type systems and checkers for common C code pitfalls like buffer overflows, integer overflows, and undefined behavior (e.g., C and CPP check, Rust's borrow checker). Crucially for cryptography, static analysis can perform information flow analysis, tracking how secret values propagate through a program and ensuring properties like constant-time execution, which mitigates side-channel attacks.

1. Formal Methods: The apex of assurance, formal methods involve using computers to check that logical statements about code follow from a base set of mathematical assumptions. This provides a very high level of confidence because the verification process itself relies on a small, trusted code base and rigorous mathematical principles. Jade distinguishes between two main types:

• SAT/SMT Solvers: These tools automatically attempt to satisfy Boolean or more complex logical formulas derived from code and specifications. They excel at crunching through many simple proofs and can often provide counter-examples when a specification is violated. Tools like the C Bounded Model Checker (CBMC) and proof-aware languages like Daphne (which uses the Z3 SMT solver) demonstrate their power in verifying properties over potentially infinite input spaces.
• Proof Assistants: These tools are more interactive, requiring the programmer to guide the proof step-by-step. While more effort-intensive, they offer fine-grained control and are particularly suited for complex or novel mathematical proofs, as exemplified by projects using tools like Lean and Rocq.

A significant key finding is the increasing normalization and ubiquity of formal verification in modern cryptographic libraries and protocols. What was once considered a niche academic pursuit a decade ago is now standard practice in critical components of OpenSSL, SSH, Chromium's BoringSSL, Firefox's HACL\*, Signal's post-quantum ratchet, and the standard cryptographic libraries for languages like Go, Python, Zig, and Rust. This widespread adoption signifies a collective effort by cryptographers, programmers, and mathematicians to fundamentally enhance the security and trustworthiness of our digital communications and systems.

Technical Deep Dive

▶ Watch: Limitations of random testing; introduction to clever testing (4:00)

The journey to minimize bugs in cryptography code moves through several distinct technical stages, each offering a higher degree of assurance.

Clever Testing

Beyond rudimentary unit testing, "clever testing" involves strategies to specifically target the unique challenges of cryptographic code.

• Witch Proof: This repository is a prime example, providing a curated collection of test vectors for various cryptographic algorithms. These vectors are not random; they are specifically designed to trigger known vulnerabilities from past incidents in crypto libraries or to exercise rarely used functionality and corner cases. Integrating Witch Proof into a test suite significantly broadens coverage beyond typical inputs.
• Fuzzing: A dynamic analysis technique, fuzzing involves feeding a program with large amounts of semi-random, malformed, or unexpected inputs to uncover crashes, hangs, or incorrect behavior. Coverage-guided fuzzing is a more sophisticated variant. It instruments the code to monitor execution paths and then intelligently mutates inputs to maximize code coverage, attempting to hit every branch and statement. For instance, if a rare branch in the code is only executed under specific, unusual conditions, a coverage-guided fuzzer will observe that the branch hasn't been hit and will evolve its inputs to try and trigger it.

However, even advanced fuzzing has limitations, especially for cryptographic code designed for constant-time execution. Constant-time code aims to prevent information leakage through timing side-channels by ensuring that execution time does not depend on secret inputs. This often involves avoiding conditional branches that depend on secrets, instead performing all necessary computations and using bitwise operations to select the correct result. In such cases, a coverage-guided fuzzer might falsely report full coverage, as all code paths are technically executed, yet a subtle computational error in one of the "always-run" branches could remain undetected. This necessitates moving beyond execution-based testing.

Static Analysis

Static analysis involves analyzing a program's source code or compiled binaries without actually executing it. It examines the program's logic to infer properties and detect potential issues.

• Type Systems: The simplest form of static analysis, a strong type system (e.g., in Rust, Go, Haskell) can prevent entire classes of bugs by ensuring that operations are only performed on compatible data types. An extension for cryptography might involve distinguishing between "secret" and "non-secret" integer types, flagging errors if a secret value is used where a non-secret is expected.
• General Bug Checkers: Tools like C and CPP check analyze C/C++ code for common vulnerabilities such as buffer overflows (accessing memory outside array bounds), integer overflows (arithmetic operations exceeding data type limits), and undefined behavior. These are crucial for C, a language widely used in performance-critical cryptographic implementations.
• Rust's Borrow Checker: Built into the Rust compiler, the borrow checker is a powerful static analysis tool that enforces memory safety by ensuring that at any given time, a variable has either one mutable reference or any number of immutable references. This eliminates entire categories of bugs like data races and use-after-free errors common in C/C++.
• Information Flow Analysis and Constant-Time Verification: For cryptographic code, a particularly valuable application of static analysis is tracking information flow, especially concerning secrets. Jade describes a custom Python script developed for a proprietary processor with its own instruction set. This script parses the binary, identifies initial secret values (e.g., in specific registers), and then builds a dependency graph as instructions are processed. It ensures that no value depending on a secret flows into an instruction that could influence timing. This is critical for verifying constant-time properties and mitigating timing attacks. The speaker emphasizes that static analysis tools are essentially "code that checks other code" and can be custom-built or integrated into continuous integration (CI) pipelines.

Formal Methods

Formal methods represent the highest tier of assurance, employing mathematical rigor to prove properties about software or hardware. They involve a computer checking that a logical statement (a specification) follows from a base set of mathematical assumptions, often with a very small, trusted kernel of code performing the actual checking.

• SAT/SMT Solvers:
• SAT (Boolean Satisfiability) solvers determine if a system of Boolean equations can be made true by assigning true/false values to variables.
• SMT (Satisfiability Modulo Theories) solvers extend SAT solvers by incorporating theories for other data types like integers, arrays, and real numbers. They are powerful automated backend engines for many verification tools.
• C Bounded Model Checker (CBMC): This tool takes C code and a specification (often expressed as contracts using requires and ensures clauses) and translates them into a form that an SMT solver can process. For instance, a contract might specify that a function expects an array of a certain size, guarantees it will only modify memory within that array, and ensures elements remain within a new maximum bound. CBMC can then automatically check if the code adheres to this contract within a bounded execution.
• Daphne: A proof-aware programming language, Daphne is designed specifically to facilitate formal verification. It allows developers to write code alongside comprehensive specifications (e.g., "this function returns the maximum value, max, from a list, and max is in the list, and all other elements are at most max"). Daphne automatically translates both the code and the specification into a format understandable by an SMT solver like Z3. The solver then attempts to prove the correctness of the function, even over an infinite input space, often in mere seconds. This showcases the immense power of automation for general correctness proofs.
• Workflow and Challenges: The typical workflow involves writing code and a specification, a tool translating it for the solver, and the solver attempting to prove or disprove the property. If disproven, the solver often provides a counter-example, detailing the input that violates the specification. A key challenge, however, is the halting problem: SMT solvers can time out. When this happens, it's unclear if the code is correct but the proof is too complex, or if a bug exists but the solver couldn't find a counter-example in time. In such cases, the user must provide "hints" to guide the solver. Project Everest, a decade-long effort to formalize TLS and FSAR, found that while SMT solvers offered incredible scale and automation, they introduced opacity (unclear how the solver arrived at a proof) and proof instability (minor code/solver version changes could break proofs).

• Proof Assistants:
• In contrast to automated solvers, proof assistants prioritize interactive control. The programmer explicitly guides the proof step-by-step, telling the assistant which logical inferences to make. Tools like Lean and Rocq (which Jade demonstrates) provide an interactive environment where the user types proof steps on one side, and the assistant displays the current state of the proof and remaining goals on the other.
• Advantages: This fine-grained control is invaluable for very complex, novel, or mathematically intricate proofs (e.g., the four-color theorem, the fifth busy beaver number). While more time-consuming to develop, the resulting proofs are highly stable and transparent. Proof assistants are essentially "really fancy type checkers" based on set and type theory.
• Hybrid Approaches: The line between automated and interactive tools is not always sharp. Some proof assistants incorporate automated solvers for sub-goals (e.g., Rocq's LEA for linear arithmetic), and some SMT-focused tools offer interactive modes. The choice depends on the problem's complexity: automated for many simple proofs, interactive for fewer, highly complex ones.
• Code Generation and Verification (Fiat Cryptography): Jade highlights Fiat Cryptography, a project she worked on, as an example of a powerful approach. Instead of proving individual modular multiplication routines for different moduli or architectures, they wrote a program that generates these routines. The proof then applies to the generator code, making a much stronger statement: "any code generated by this program will be correct." This leverages the power of proof tools not just to verify existing code, but to guarantee the correctness of code generation itself.

Beyond Code

The application of these high-assurance techniques extends beyond pure software. They can be used to:

• Hardware Verification: Ensure processors correctly implement their instruction sets.
• Algorithm Verification: Prove that cryptographic schemes (e.g., signature or encryption) fulfill their theoretical security properties.
• Protocol Verification: Verify that complex protocols (e.g., Signal's sparse post-quantum ratchet) correctly assemble cryptographic primitives to achieve high-level properties like secrecy and authenticity. Signal's protocol, for instance, was verified using Proverifth, and its underlying code relies on the verified libcrux library.

The speaker concludes this section by emphasizing that formal methods, once niche, are now "pretty ubiquitous." Components of widely used software like OpenSSL, SSH, Chromium's BoringSSL (which uses Fiat Cryptography), and Firefox's HACL\* (a verified elliptic curve cryptography library) incorporate formally verified code. Even standard libraries in Go, Python, Zig, and Rust leverage these techniques, marking a significant advancement in the security posture of critical digital infrastructure.

Demo / Proof of Concept

▶ Watch: Fuzzing limitations for constant-time cryptographic code (6:00)

While the talk did not feature a live, interactive demonstration of a specific tool or a single proof-of-concept exploit, Jade effectively illustrated the capabilities and workflows of various assurance techniques through detailed examples and descriptions of practical applications.

For static analysis, the speaker described a custom Python script they developed to perform information flow analysis and constant-time verification for code running on a custom processor. This script parsed the processor's binaries, tracked dependencies of secret values, and ensured that these secrets did not influence timing-sensitive instructions. This practical example, born out of the speaker's own work on the OpenTitan big number co-processor, served to demystify static analysis, showing it as "code that checks other code" rather than some abstract magic.

In the realm of formal methods, Jade presented screenshots and pseudo-code examples to convey the user experience. For SMT solvers, she showed an example contract for C code used with the C Bounded Model Checker (CBMC) from the MLM native project, illustrating how requires and ensures clauses specify function behavior. She also presented a code snippet from Daphne, a proof-aware programming language, demonstrating how a full correctness condition for a max function could be written and then automatically verified by the Z3 SMT solver over an infinite input space.

For proof assistants, a screenshot from Rocq vividly depicted the interactive nature of these tools, with the programmer's input on the left and the proof assistant's real-time feedback on the current proof state on the right. This visual aid helped convey the iterative, guided process of constructing a formal proof.

Finally, the discussion of Fiat Cryptography, a project Jade contributed to, served as a powerful conceptual proof-of-concept for code generation with formal verification. Instead of verifying many individual, highly optimized cryptographic routines, the project focused on proving the correctness of the generator that produces these routines. This demonstrates a strategic application of formal methods to achieve broad correctness guarantees across a family of implementations.

Through these detailed descriptions and conceptual examples, Jade successfully conveyed the practical application and workflow of these high-assurance tools, even without a live, step-by-step demo.

Defensive Implications

▶ Watch: Transitioning to static analysis for whole program logic (7:00)

The increasing sophistication of attacks on cryptographic implementations necessitates a proactive and rigorous defensive posture. Jade's talk provides a clear roadmap for defenders seeking to minimize bugs and enhance the security of their cryptographic code:

1. Embrace Incremental Assurance: Not all code requires the highest level of formal verification. Defenders should identify critical cryptographic components and apply assurance techniques commensurate with their impact. Start with lower-effort, high-impact methods before moving to more intensive ones.

1. Enhance Testing with Clever Strategies:

• Integrate Specific Test Vectors: Utilize resources like Witch Proof to test against known past vulnerabilities and edge cases. This immediately raises the bar for detecting common pitfalls.
• Implement Coverage-Guided Fuzzing: Employ fuzzers that intelligently explore code paths to uncover crashes, logic errors, and other bugs. While fuzzing has limitations for constant-time code, it remains an indispensable tool for broad bug discovery.

1. Leverage Static Analysis for Foundational Security:

• Utilize Language-Specific Tools: For C/C++ code, integrate C and CPP check to detect buffer/integer overflows and undefined behavior. For Rust, fully leverage the compiler's borrow checker for memory safety.
• Implement Information Flow Analysis: For highly sensitive cryptographic code, especially where side-channel attacks are a concern, develop or adapt static analysis tools to track secret dependencies. This is crucial for verifying constant-time execution, ensuring that secrets do not influence control flow or memory access patterns that could leak information through timing.

1. Adopt Formal Methods for the Highest Assurance:

• Start with Automated Solvers: For components where a clear mathematical specification can be written, SAT/SMT solvers (e.g., using CBMC for C or Daphne with Z3) can automatically prove correctness or provide valuable counter-examples. This is particularly effective for verifying many simple proofs at scale.
• Consider Proof Assistants for Complex Proofs: For extremely critical, mathematically complex, or novel cryptographic algorithms or protocols, proof assistants like Lean or Rocq offer the fine-grained control needed to construct rigorous, transparent proofs. While requiring more effort, they provide unparalleled confidence.
• Verify Code Generators: As demonstrated by Fiat Cryptography, consider verifying the code that generates cryptographic primitives. This provides a powerful guarantee for an entire family of implementations, rather than verifying each one individually.

1. Prioritize Verification of Tricky Components: Recognizing that end-to-end formal verification of entire systems is still a significant research challenge, defenders should focus on applying these high-assurance techniques to the "trickiest parts" of their cryptographic implementations—those most prone to subtle bugs or with the highest security impact.

1. Utilize Existing Verified Libraries: Defenders should actively seek out and integrate cryptographic libraries that have undergone formal verification. The increasing ubiquity of formally verified components in OpenSSL, SSH, BoringSSL, HACL\*, libcrux, and standard language libraries means that a significant portion of the security burden can be offloaded to trusted, rigorously checked foundations.

By systematically applying these techniques, defenders can significantly elevate the quality and trustworthiness of their cryptographic code, moving beyond mere bug hunting to constructing implementations that are provably correct under defined specifications, thereby bolstering the overall security posture against sophisticated adversaries.

Key Takeaways

• The "don't roll your own crypto" adage relies on a foundation of highly assured, well-vetted libraries, which themselves require rigorous bug minimization techniques.
• A spectrum of assurance tools exists, from basic testing and fuzzing to advanced static analysis and formal methods, each offering progressively higher confidence at increased effort.
• Random testing is insufficient for cryptographic code due to vast input spaces and the need to detect subtle side-channel vulnerabilities like timing attacks.
• Static analysis, particularly for information flow and constant-time verification, and formal methods (SAT/SMT solvers and proof assistants) are critical for catching logical flaws and ensuring fundamental security properties that dynamic testing might miss.
• Formal verification, once a niche academic pursuit, is now becoming standard practice in major cryptographic libraries and protocols, including OpenSSL, BoringSSL, Signal, and standard language libraries.
• Defenders should strategically adopt these high-effort, high-assurance techniques for critical cryptographic components to build more resilient and trustworthy systems.

About the Speaker(s)

The talk was given by Jade. Based on the details shared during the presentation and the Q&A, Jade possesses significant expertise in the field of cryptographic implementation and verification. She has practical experience in developing custom static analysis tools, specifically mentioning writing Python scripts to check hardware loop instructions and information flow for a custom processor with its own instruction set, identified as the OpenTitan big number co-processor. Jade also contributed to Project Fiat Cryptography, a notable initiative focused on generating and formally verifying highly optimized cryptographic routines. Her perspective is informed by approximately a decade of working in this domain, during which she witnessed the evolution of formal methods from a niche academic area to an increasingly mainstream and indispensable practice in securing critical cryptographic infrastructure.