Auditing Cryptographic Libraries with AI: What We Found in Cloudflare's CIRCL

Where AI Meets Cryptography

Cryptographic code has long been regarded as one of the hardest domains to audit in software engineering. It involves extensive number-theoretic operations, constant-time implementations, side-channel defenses, and countless other details—where even a tiny oversight can lead to catastrophic security vulnerabilities. As large language models (LLMs) rapidly advance in code comprehension, a natural question arises: Can AI handle the security auditing of cryptographic libraries?

The practice explored in this article centers precisely on this question—researchers applied AI tools to Cloudflare's open-source cryptographic library CIRCL (Cloudflare Interoperable Reusable Cryptographic Library), seeking to validate AI's auditing value in real-world cryptographic engineering. CIRCL is no toy project; it is a production-grade Go cryptographic library that is widely deployed and continuously maintained by a professional team, making it highly representative.

Why Choose CIRCL

CIRCL is a cryptographic toolkit written by Cloudflare in Go, covering cutting-edge algorithm implementations such as post-quantum cryptography (like Kyber and Dilithium), elliptic curve operations, hash-to-curve, and blind signatures. With its large codebase, high algorithmic complexity, and extensive low-level finite field operations and constant-time constraints, it is an ideal proving ground for testing AI's auditing capabilities.

The post-quantum cryptographic algorithms implemented in CIRCL (Kyber, Dilithium) come from the NIST Post-Quantum Cryptography Standardization project—launched in 2016 to counter the threat that quantum computers pose to existing public-key cryptosystems (RSA, ECC). Once quantum computers reach sufficient scale, RSA (based on the hardness of integer factorization) and ECC (based on the hardness of discrete logarithms) will simultaneously face the threat of Shor's algorithm, which can solve both classes of problems in polynomial time. Kyber is a key encapsulation mechanism based on module lattices (Module-LWE), while Dilithium is the corresponding digital signature scheme; both became official NIST standards in 2024 (named ML-KEM and ML-DSA, respectively). The security of these algorithms rests on the computational hardness of the Learning With Errors (LWE) problem on lattices—even for quantum computers, no known efficient algorithm can solve LWE in polynomial time, which is the mathematical foundation of their "post-quantum secure" property. The implementation of these algorithms involves operations over polynomial rings, the NTT (Number Theoretic Transform), and strict noise parameter management, with complexity far exceeding that of traditional cryptographic algorithms—making code auditing exponentially harder. This is precisely the deeper reason for choosing CIRCL as the testbed.

It is worth adding that the NTT (Number Theoretic Transform) is the core performance bottleneck in post-quantum cryptography implementations. It is essentially the finite-field analog of the discrete Fourier transform, reducing the complexity of polynomial multiplication from O(n²) to O(n log n)—crucial for polynomial-ring-based algorithms like Kyber and Dilithium. However, correctly implementing NTT is extremely delicate: it requires not only precisely selecting a prime modulus that satisfies specific divisibility conditions (known as an NTT-friendly prime; for example, Kyber's q=3329 satisfies q≡1 mod 256, ensuring the 256th root of unity exists in the field), but also correctly handling bit-reversal permutation in the butterfly operations and precomputing constant factors. The butterfly operation is the core computational unit of FFT-class algorithms, and each transformation stage involves precise twiddle factor multiplications—an error in any single twiddle factor introduces a global error in the polynomial multiplication result, yet such errors are often hard to catch in standard unit tests because the error pattern itself has algebraic structure and may happen to pass test cases designed for specific inputs. Once an implementation is faulty, the result may pass most functional tests yet produce incorrect ciphertexts or signatures under specific inputs. Such "silent failures" are extremely difficult to detect in real deployments, yet can completely undermine the security of a cryptographic scheme. Furthermore, the security of the Module-LWE problem depends on precise noise parameter selection: too narrow a noise distribution harms security, while too wide a distribution affects decoding correctness. This precise mapping between mathematical constraints and code implementation constitutes the core challenge of cryptographic auditing.

Equally important to the NTT as a foundational technique is Montgomery multiplication. This is a widely used finite-field arithmetic optimization in modern cryptographic implementations: field elements are transformed into "Montgomery space" (i.e., representing $a$ as $aR \bmod p$, where $R$ is a chosen auxiliary constant, typically $R = 2^{256}$ or an integer power of the machine word size). Performing multiplication in this space completely avoids the expensive trial-division step of traditional modular arithmetic, replacing it with shifts and additions and significantly boosting the efficiency of large-number modular multiplication. Entering and leaving Montgomery space each require a conversion operation (multiplying by $R \bmod p$ and by $R^{-1} \bmod p$), and when performing a large number of consecutive modular multiplications, the amortized cost of these two conversions becomes negligible—making Montgomery multiplication nearly ubiquitous in the finite-field operations of RSA, elliptic curves, and post-quantum cryptography. However, this also introduces an implicit representation invariant: whether a function's inputs and outputs are in Montgomery form must remain consistent throughout the entire call chain, or the result will silently produce incorrect values without triggering any exception. Such "implicit module contracts" are often documented only in comments rather than enforced by the type system—precisely the kind of scenario where AI is prone to misjudgment when its context window is limited, and also where formal type systems can offer unique value in verifying cryptographic implementations.

Manually auditing such a library typically requires experts with deep cryptographic backgrounds to invest weeks or even months. If AI can assist with, or even partially replace, this process, its engineering value would be considerable.

What Can AI Auditing Uncover

The core challenge in applying AI to cryptographic library auditing is that the model must not only understand code syntax but also grasp the mathematical correctness and security semantics behind the algorithms. This is far more complex than finding an ordinary null pointer or buffer overflow.

Current LLMs demonstrate capabilities beyond traditional static analysis tools in code auditing, rooted in the fact that their pretraining phase absorbed massive amounts of code repositories, security reports, academic papers, and technical documentation, forming cross-modal semantic association capabilities. Unlike rule-based static analysis (such as CodeQL) or symbolic execution tools, LLMs can understand the intent of comments, recognize the semantics behind naming conventions, and infer data flow even in the absence of complete type information. CodeQL works by parsing code into a relational database, allowing users to write SQL-like queries to detect specific vulnerability patterns (such as "tainted data flowing from user input into a SQL query"); its strength lies in precision and reproducibility, but it is powerless against logical errors that cross semantic boundaries. Symbolic execution tools (such as KLEE and angr) enumerate execution paths by replacing variables with symbolic values and can discover boundary-condition vulnerabilities, but they suffer from the path explosion problem and are often not scalable on large cryptographic libraries. However, LLMs also introduce the risk of "hallucination": the model's output is essentially probabilistic pattern matching rather than logical deduction. Research shows that combining LLMs with traditional program analysis techniques (such as taint analysis and abstract interpretation) can effectively complement each other's weaknesses—a direction that is becoming the mainstream approach in the design of AI security auditing toolchains.

Detecting Constant-Time Implementations

One of the most insidious and dangerous classes of problems in cryptographic code is timing side-channel attacks caused by non-constant-time execution. The principle behind timing side-channel attacks is that modern processors do not take exactly the same amount of time to execute conditional branches, memory accesses, and certain arithmetic operations. If a cryptographic implementation contains branches or table lookups that depend on secret data, an attacker only needs to precisely time a large number of cryptographic operations and can then use statistical methods to recover the private key bit by bit—famous examples include the Bleichenbacher attack against OpenSSL's RSA implementation and cache-timing attacks against AES lookup tables. Constant-time programming requires that the execution path and timing of all operations be completely independent of secret values, typically achieved by replacing conditional branches with bitmask operations. For example, a constant-time conditional assignment if secret { x = a } else { x = b } would be rewritten as x = (mask & a) | (~mask & b), where mask is generated from secret through arithmetic operations (rather than branches), ensuring the entire operation sequence executes the same instruction sequence regardless of the value of secret.

Modern cache-timing attacks have evolved into highly sophisticated variants, further underscoring the importance of constant-time implementations. The Flush+Reload attack exploits the physical sharing of shared memory pages and the CPU's last-level cache (LLC)—the attacker and victim share the same memory-mapped page (such as a shared library), and by periodically flushing the target cache line (the clflush instruction) and then precisely measuring the time difference to reload that memory line (cache hit ~4ns, miss ~200ns), the attacker can infer the victim's memory access sequence and thereby reconstruct the key. This technique has achieved a precision level capable of distinguishing between different lookup-table indices within a single AES round function, making even carefully optimized table-based implementations vulnerable. The disclosure of the Spectre and Meltdown vulnerabilities pushed side-channel issues to new heights—even code that "looks constant-time" generated by compiler optimizations may introduce timing differences at the microarchitectural level due to the processor's speculative execution and out-of-order execution mechanisms. The core mechanism of Spectre is this: when the processor mispredicts a branch, it rolls back the architectural state (register values), but the already-polluted cache state cannot be rolled back, allowing the attacker to probe the memory content accessed during the speculative execution phase. This means that constant-time guarantees must extend down to the hardware microarchitecture level; source-code-level checks alone are no longer sufficient. It is precisely for this reason that Go's subtle standard library package provides a series of constant-time operation primitives (such as subtle.ConstantTimeCompare). CIRCL's implementation relies extensively on these primitives, and determining whether they are used correctly and completely is exactly the kind of scenario where AI auditing can leverage its semantic-understanding advantages.

Traditionally, detecting such problems requires specialized tools (such as dudect and ctgrind) or extremely meticulous manual review. dudect performs statistical t-tests on large numbers of random inputs to determine whether the execution time distribution correlates with the input, capable of detecting statistically significant timing leaks—but it requires a real hardware environment and cannot provide code-location information for the vulnerability. AI demonstrates a unique advantage here: it can understand data flow across function boundaries, identify dangerous patterns such as "secret-dependent conditional branches" or "secret-dependent memory accesses," and provide explanations in natural language that point directly to specific locations in the source code. This semantic-understanding-based static analysis is precisely what traditional tools struggle to achieve, fusing "finding the vulnerability" and "locating the cause" into a single step.

Reviewing Algorithm Logic and Boundary Conditions

Beyond side-channel issues, AI can also examine whether an algorithm implementation faithfully adheres to its mathematical specification. For example: whether carries are handled correctly in modular arithmetic, whether the special case of the point at infinity is missed in elliptic curve point operations, and whether decoding functions adequately validate illegal inputs. These logical oversights often do not cause the program to crash but may quietly undermine the overall security of a cryptographic scheme.

A classic historical lesson is the ROCA vulnerability (CVE-2017-15361) disclosed in 2017: Infineon's RSA key generation implementation adopted a non-standard prime generation method in pursuit of efficiency, causing the generated RSA keys to have a special structure identifiable by mathematical tools, allowing attackers to factor 1024-bit RSA keys within hours. This vulnerability affected millions of smart cards and TPM chips worldwide, with the root cause being that the algorithm implementation deviated from the mathematical intent of "uniformly randomly sampling primes." ROCA's discoverers analyzed the number-theoretic characteristics of a large number of public keys and noticed that the RSA moduli generated by the affected chips exhibited anomalous regularity in their factorization over a specific integer base, thereby reverse-engineering the non-standard generation algorithm—this methodology of identifying implementation patterns from cryptographic artifacts itself embodies the importance of "mathematical intuition" in cryptographic auditing. Similarly, if an elliptic curve implementation fails to validate the legitimacy of an input point on the curve (i.e., an invalid curve attack), an attacker can submit a forged point that is not on the target curve, forcing the private-key operation to be performed in a small-order subgroup, and then gradually recover the private key using the Chinese Remainder Theorem. Such attacks require auditors not only to understand the code but also to understand its correspondence with the cryptographic scheme's security proof—precisely the area where AI, after being trained on cryptographic corpora, can provide unique value.

The Boundaries of AI Auditing

Although AI has demonstrated real potential in cryptographic auditing, we must also soberly recognize its limitations.

Context Window and Hallucination Problems

The correctness of a cryptographic library often depends on global invariants spanning multiple files. When the code scale exceeds the model's effective context window, AI may produce judgments that seem reasonable but are actually wrong—so-called "hallucinations." It may "discover" a vulnerability that does not exist, or raise pointless doubts about correct code. Therefore, AI's output must undergo cross-validation by human experts and cannot be directly treated as an audit conclusion.

This limitation is especially pronounced in cryptographic library auditing, because the correctness of cryptographic code often depends on cross-module "implicit contracts." The Montgomery form mentioned earlier is a classic case: a finite-field multiplication function may output an intermediate value in Montgomery space, and the caller must be aware of this precondition to use it correctly, yet such conventions often appear only in comments or internal documentation rather than in the type system. When the model's context is insufficient to simultaneously hold all links in the call chain, it is prone to misjudging such conventions. Mainstream models (such as GPT-4 and Claude 3) have expanded their effective context windows to 100,000–200,000 tokens, but the complete codebase of a large cryptographic library like CIRCL may still exceed the boundary of a single analysis. One effective engineering mitigation strategy is to build a code summarization layer—first having the model generate structured functional summaries and interface-contract descriptions for each module, then performing cross-module analysis at a higher abstraction level, thereby achieving an understanding of the overall architecture within a limited context. Another complementary strategy is to introduce a Retrieval-Augmented Generation (RAG) architecture: semantically chunk the codebase and store it in a vector database, and when analyzing a particular function, dynamically retrieve its most semantically relevant callers, callees, and related documentation comments to expand the context on demand rather than cramming all the code into the window at once—this can, to some extent, alleviate the limitations that a fixed context window imposes on cross-module reasoning.

The Absence of Formal Proofs

AI currently excels at pattern recognition and heuristic reasoning, not rigorous formal proof. For cryptography, there is a fundamental gap between "the code looks correct" and "the code is proven correct." Truly high-assurance cryptographic implementations often require the support of formal verification tools—HACL* (High-Assurance Cryptographic Library), jointly developed by INRIA and Microsoft Research, is written in the F* language and comes with machine-checked security proofs; it has been adopted by mainstream software such as Firefox and the Linux kernel. Fiat-Crypto, on the other hand, adopts a "specification-to-code" approach, automatically synthesizing proven finite-field arithmetic code directly from mathematical specifications, and is used in Chrome's elliptic curve implementation.

The technical approaches adopted by these two classes of tools are worth understanding in depth. HACL* is based on the Refinement Types system—the F* language allows mathematical assertions to be embedded in types; for example, one can define the type FieldElement = {x: uint64 | x < p} to statically guarantee that a variable always stays within the finite-field range. During the type-checking phase, the compiler invokes an SMT solver (such as Microsoft's Z3) to automatically determine the satisfiability of these assertions, without requiring manually supplied step-by-step proofs. Z3 is an industrial-grade SMT (Satisfiability Modulo Theories) solver developed by Microsoft Research, capable of deciding the satisfiability of first-order logic formulas under various theories such as arithmetic, bit-vectors, and arrays; its reasoning power is sufficient to automatically verify most finite-field arithmetic constraints appearing in cryptographic implementations. This means that a function annotated as "the input must be a finite-field element in the interval [0, p), and the output is its multiplicative inverse mod p" has its correctness machine-proven at compile time, rather than relying on runtime testing. Fiat-Crypto goes even further: the entire finite-field arithmetic code is not hand-written and then verified, but rather directly "extracted" from a mathematical specification in the Coq proof assistant, fundamentally eliminating the gap between specification and implementation. Coq's program extraction mechanism is based on the Curry-Howard isomorphism—mathematical proofs and computer programs have a deep correspondence at the level of type theory, and a correctness proof is itself a runnable program that can be translated into executable OCaml or Haskell code via "extraction." By contrast, AI's analysis is closer to "the intuitive judgment of an experienced human expert"—fast and broad in coverage, but lacking formal reliability guarantees. The two form a well-layered, complementary relationship between assurance level and engineering efficiency: formal verification provides absolute guarantees for core primitives, while AI auditing offers rapid security scanning at the more macroscopic architectural level.

Implications for Cryptographic Engineering Practice

The most important insight from this practice is that AI should be positioned as an amplifier of auditing efficiency, not a replacement for human experts.

A New Paradigm of Human-AI Collaboration

A reasonable workflow is: let AI first perform broad-range scanning to quickly flag suspicious code regions and potential timing-leak points, and then have cryptographic experts focus on these regions for in-depth verification. The combination of "AI handles breadth, humans handle depth" can significantly improve auditing efficiency, concentrating scarce expert resources on the parts that truly require judgment.

This collaborative model has precedents worth drawing on in the field of security engineering. The Google Project Zero team introduced semi-automated code-diff analysis tools in vulnerability research to quickly locate security-relevant changes across version iterations of large codebases, and then had researchers focus on these change points for in-depth analysis—this model of "automation narrows the search space, humans perform deep verification" aligns closely with the logic of AI-assisted cryptographic auditing. In concrete engineering implementation, one can build an "AI auditing pipeline": first perform module-level automated scanning of the codebase to generate a list of suspicious locations ranked by risk level; then trigger deeper contextual analysis for high-risk locations; finally, output the results as a structured audit report annotated with confidence levels and reasoning bases, so that human experts can prioritize high-confidence findings. Confidence estimation can be approximated by the consistency of results across multiple independent prompt runs: if multiple analyses of the same code segment all point to the same problem, confidence is high; if the conclusions are unstable, it is flagged for manual review. This layered design can keep the cost of AI's false positives within an acceptable range while maximizing the discovery efficiency of true positives.

Driving a Virtuous Cycle in Open-Source Security

For open-source libraries like CIRCL, lowering the barrier to auditing is itself a major boon. In the past, only large institutions or professional security teams had the capacity to systematically review complex cryptographic libraries; now AI tools enable more researchers and community contributors to participate, forming a broader oversight mechanism. This is a structural strengthening of the security of the entire open-source cryptographic ecosystem—especially at a time when post-quantum cryptographic algorithms are being deployed rapidly and a large number of new implementations urgently await review, the value of this "distributed auditing capability" is particularly prominent.

This structural strengthening has traceable roots in the history of open-source security. The OpenSSL Heartbleed vulnerability (CVE-2014-0160) disclosed in 2014 affected roughly 17% of HTTPS servers worldwide, and the code containing the vulnerability had existed in the codebase for about two years—despite OpenSSL being one of the most widely used cryptographic libraries in the world. The vulnerability stemmed from a lack of validation of the user-supplied length field in the implementation of the TLS Heartbeat extension—when responding to a heartbeat request, the server would read and return data from memory according to the message length claimed by the client rather than the actual message length, allowing attackers to read up to 64KB of arbitrary content from server memory each time, which could include private keys, user passwords, and session cookies. Post-incident analysis revealed that one root cause was the chronic shortage of auditing resources that open-source projects face: there are many code contributors, but contributors with a cryptographic engineering background who are willing to perform systematic security reviews are extremely scarce. The Heartbleed incident directly gave rise to the Linux Foundation's Core Infrastructure Initiative (now renamed OpenSSF, the Open Source Security Foundation), which pooled funding and engineering resources from major tech companies such as Google, Microsoft, and Amazon to provide dedicated security audits and developer training for critical infrastructure like OpenSSL and curl. Its Best Practices Badge program requires projects to pass multiple security checks covering cryptographic usage, vulnerability response processes, and more, and has become an important quantitative metric for open-source security governance. OpenSSF also launched the Scorecard tool, which can automatically evaluate the security maturity of GitHub projects across dimensions such as dependency management, code review coverage, and CI/CD security configuration, providing a quantifiable security baseline for the open-source ecosystem. Today, the emergence of AI-assisted auditing tools offers a new approach to solving this dilemma—it cannot replace professional auditing, but it can significantly lower the "barrier to possessing effective auditing capability," enabling more community participants to make meaningful security contributions and thereby structurally compensating for the long-standing shortage of professional resources.

Conclusion

"AI meets cryptography" is not about using large models to replace cryptographers, but about exploring a more efficient way of collaboration. The CIRCL auditing practice demonstrates that AI can already provide valuable leads in practical tasks such as constant-time detection and algorithm-logic review, but its output still requires the gatekeeping and verification of professional judgment.

As model capabilities continue to evolve and specialized toolchains mature, AI-assisted cryptographic auditing is poised to gradually become a standard part of security engineering. At a time when post-quantum cryptography is being deployed rapidly and cryptographic implementations are growing ever more complex, the arrival of this assistive force could not be more timely.

Key Takeaways