Verifying code that uses encryption

Code that calls encryption is code that passes keys, plaintext, ciphertext and associated data to a primitive such as AES-GCM, and that builds protocols and file formats around the results. Formal verification of such code takes the primitive as given, a specification the verifier trusts but does not examine, and proves properties of the caller: that it passes the right key and associated data, builds distinct nonces, honours failure results, and rejects messages that violate a policy. The field sits between three traditions that differ in what they prove. Program verifiers check caller code against written specifications; protocol and game-based provers reason about security in the symbolic or computational model; and static misuse detectors check usage rules without proving anything about security. The main disputes concern what an assumed primitive hides, which security properties a program verifier can state at all, and what a proof of functional correctness fails to catch.

History

The work spans two decades and approached the problem from different sides. Terauchi and Aiken (2005) showed that checking secure information flow can be reduced to a safety problem by a program transformation, which Barthe, D’Argenio and Rezk later named self-composition (Terauchi & Aiken, 2005). Clarkson and Schneider (2010) then gave the formal vocabulary of trace properties and hyperproperties used to say what kind of property noninterference is (Clarkson & Schneider, 2010).

Work on how encryption fits into information-flow checking is of the same period. Askarov, Hedin and Sabelfeld (2008) treated encryption inside noninterference through cryptographically-masked flows (Askarov et al., 2008), and Fournet and Rezk (2008) connected a typed information-flow language to cryptographic hypotheses (Fournet & Rezk, 2008). Aizatulin, Gordon and Jürjens (2011) extracted symbolic cryptographic models from C protocol code by symbolic execution (Aizatulin et al., 2011). Barthe and colleagues (2011) described computer-aided security proofs built as sequences of games (Barthe et al., 2011).

Later work moved toward practice. Krüger and colleagues (2018) published CrySL, a rule language and static analysis for correct cryptographic API usage in Java (Krüger et al., 2018; Krüger et al., 2017). A 2016 Galois write-up describes a proof that s2n’s C HMAC code is equivalent to a Cryptol specification (Galois, 2016). Cecchetti, Myers and Arden (2017) generalised noninterference to allow controlled downgrading (Cecchetti et al., 2017), and Eilers (2022) extended product-program verification, implemented in Viper, to mainstream languages (Eilers, 2022). The AWS Encryption SDK and AWS Database Encryption SDK are the main industrial case: AWS describes the Database Encryption SDK for DynamoDB as a Dafny product that assures functional correctness, a vendor claim whose proof scope is not stated (Amazon Web Services, n.d.).

Earlier history (when protocol verification and API-level verification of encryption code began) is not covered in the research.

Core concepts

Assuming the primitive

A verifier of caller code needs some model of the primitive. Two models are in use. In the symbolic approach to C protocol code, the primitive implementations are not analysed at all: symbolic models of them are the trusted base, and the method assumes the primitives are implemented correctly (Aizatulin et al., 2011). In the contract approach, the primitive is an extern declaration with a specification. The AWS Cryptographic Material Providers library declares AES-GCM encryption and decryption as externs marked {:axiom}, which tells the Dafny verifier to trust the contract without proof. Their postconditions tie ciphertext, plaintext, key and associated data (AAD) together only through predicates with no body, such as “decrypted with this AAD”, “generated from this ciphertext” and “decrypted with this key”; callers can cite these predicates in their own postconditions, so a proof about a caller can check that the AAD was as expected (AWS Cryptographic Material Providers Library maintainers, n.d.). The decrypt extern’s preconditions require the key, initialization vector (IV) and tag to have the lengths the algorithm requires, which callers must prove (AWS Cryptographic Material Providers Library maintainers, n.d.). ECDSA signature verification is an extern function with no body or postcondition beyond a comment that a non-matching signature returns Success(false), so callers reason only through the history of calls made to it (AWS Cryptographic Material Providers Library maintainers, n.d.). The Dafny SDK’s tests need native implementations of the primitives, which sit outside the proof (aws (aws-encryption-sdk-dafny repository maintainers), n.d.).

What the assumption hides is stated explicitly. Because the predicates have no body, nothing is proved about what they mean, and the real AES-GCM is trusted to honour them (AWS Cryptographic Material Providers Library maintainers, n.d.). The failure case (tampered input) has no postcondition at this level (AWS Cryptographic Material Providers Library maintainers, n.d.). For symbolic models, the computational soundness result used requires an IND-CCA secure public-key encryption operation, and some verified programs fell outside its conditions because they used other primitives (Aizatulin et al., 2011). Some primitives, such as XOR, could not be modelled symbolically in the tool used, which forced use of CryptoVerif and shows that the model choice limits what can be checked (Aizatulin et al., 2011).

Verified primitive libraries prove less than a caller might hope. HACL* verifies its primitives for memory safety, functional correctness and secret independence; its project description lists no cryptographic security proof (such as IND-CPA or AEAD security), so a caller proving things on top gets a functional specification, not a security theorem (hacl-star project (Project Everest), n.d.).

Properties proved about callers

In the AWS Encryption SDK for Dafny, the proved properties are stated as postconditions over the call history of the primitive, tied to the written specification.

• Binding each result to a primitive call. Frame encryption postconditions state that each frame’s IV, ciphertext and tag equal the input and output of the AES-GCM call that was made, and that the key is the key in use (AWS (aws-encryption-sdk-dafny contributors, n.d.b).
• AAD binding. The AAD passed to AES-GCM equals the body AAD built from the message ID in the header (AWS (aws-encryption-sdk-dafny contributors, n.d.b).
• Decrypt-side integrity. The returned plaintext equals the concatenation of the outputs of the successful AES-GCM decrypt calls, so plaintext comes only from authenticated decryption (AWS (aws-encryption-sdk-dafny contributors, n.d.b). Some requirements, such as not releasing unauthenticated plaintext, appear as comments tied to code, and decrypt checks the header authentication tag before use. These proofs are implementation-level postconditions, not a separate security theorem (AWS (aws-encryption-sdk-dafny contributors, n.d.a).
• Nonce uniqueness within a message. A lemma states that distinct frame sequence numbers give distinct IVs, and it is tagged with the specification requirement that the IV be unique within the message (AWS (aws-encryption-sdk-dafny contributors, n.d.b). This is a property of how the calling code builds IVs, stated per message. Across messages, the SDK uses a unique data key per message, so cross-message nonce reuse is addressed by key freshness rather than by IV counters (Amazon Web Services (Encryption SDK Developer Guide), n.d.).
• Encryption-context rules. The specification requirement that encryption fails if the encryption context uses the reserved “aws-crypto-” key prefix is written as a postcondition (AWS Encryption SDK maintainers (EncryptDecrypt.dfy), n.d.).
• Signature verification. The signature step is specified against the call history of the extern crypto client: ECDSAVerify was called exactly once more, with the algorithm, verification key, message and signature taken from the decryption materials and buffer, and a false or failed result implies that decryption returns Failure. The postconditions constrain the arguments the code passes and how it uses the result; the primitive’s own computation is not proved there (AWS Encryption SDK maintainers (EncryptDecrypt.dfy), n.d.).
• Serialization. Readers carry a postcondition (CorrectlyRead) stating that the reader inverts the writer, a round-trip property for message-format code (AWS Encryption SDK maintainers (Serialize), n.d.).
• Key commitment policy. A suite rejected by the commitment policy makes encrypt fail (AWS (aws-encryption-sdk-dafny contributors, n.d.a). See below.

Tracing proofs to a specification

The Dafny SDK repository uses Duvet to document the written specification alongside the implementation; running make duvet outputs any missing specification coverage (aws (aws-encryption-sdk-dafny repository maintainers), n.d.). The specification is language independent and is the source of truth for the SDKs’ behaviour (awslabs (AWS Encryption SDK Specification maintainers), n.d.). Duvet annotations are comments in the code that cite a specification section and quote the requirement text verbatim, giving a two-way link between specification text and implementation; it checks that annotations cover requirements, not that the code is correct (awslabs (Duvet maintainers), n.d.). In the Dafny source, a requirement is written as a Duvet citation with type=implication directly above an ensures postcondition, so the postcondition is the machine-checked form of the quoted MUST (AWS Encryption SDK maintainers (EncryptDecrypt.dfy), n.d.). The verification itself is run by the Dafny verifier over all source files, with specification coverage tracked separately by Duvet (aws (aws-encryption-sdk-dafny repository maintainers), n.d.).

Trace properties and hyperproperties

Clarkson and Schneider define a trace property as a set of traces; a system satisfies it when every one of its traces is in the set, so it is judged trace by trace (Clarkson & Schneider, 2010). A hyperproperty is a set of trace properties, so it constrains the whole set of a system’s traces and can relate executions to each other (Clarkson & Schneider, 2010). Noninterference, a confidentiality policy, cannot be expressed as a property of individual traces, because whether one trace is allowed depends on what other traces exist (Clarkson & Schneider, 2010). They describe 1-safety as ordinary safety, and Terauchi and Aiken’s 2-safety as a property refuted by observing two finite traces, which self-composition reduces to a safety check on a product program (Clarkson & Schneider, 2010).

For encryption this matters because plain noninterference rules out programs with encryption: ciphertext depends on the secret plaintext and key (Askarov et al., 2008). Several responses exist. A common one declassifies the encryption result; Askarov and colleagues instead extend noninterference to allow safe encryption, decryption and key generation, enforced by a type system that stops key leaks and prevents confusing keys with non-keys (Askarov et al., 2008). Nonmalleable information flow generalises noninterference to allow controlled downgrading (declassification and endorsement), also enforced by a type system (Cecchetti et al., 2017). A deductive approach handles declassification as delimited information release, tracking dependencies instead of comparing two runs (van Delft & Bubel, 2015).

Tools exist for two-run properties. Relational Hoare logics verify properties of two runs, such as confidentiality (Naumann, 2020). Noninterference is a hyperproperty that most standard verifiers do not support; modular product programs let standard verifiers check it using relational specifications, implemented for Viper, and prove information-flow properties including value-dependent sensitivity and termination-sensitive noninterference (Eilers, 2022).

Tools at the application level

By the projects’ own descriptions, the tools divide as follows.

• Dafny checks code against specifications written in the same language and compiles to several target languages, which is how a verified SDK can ship in Java or .NET (Dafny project, n.d.).
• Verus proves that Rust code meets user-written functional specifications for all executions (Verus project, n.d.).
• Kani is a bit-precise model checker for Rust that checks undefined behaviour, panics, overflows and custom properties written as assertions or function contracts over nondeterministic inputs; checks are bounded, not full proofs (Kani project, n.d.).
• hax translates a subset of Rust into proof languages: F* (stable), Rocq (experimental), ProVerif, EasyCrypt and SSProve, so proofs happen in the target prover; it can extract a symbolic Dolev-Yao model through ProVerif for protocol-level analysis (Cryspen & hax contributors, n.d.).
• SAW reasons about programs in C, Java, Rust and Cryptol models, checking code against Cryptol specifications (Galois, n.d.). It was used to prove s2n’s C HMAC code equivalent to a Cryptol specification, a result bounded to fixed 64-byte message and key sizes (Galois, 2016).
• EasyCrypt is for code-based, game-based security proofs, which are relational properties of probabilistic code with adversaries, and also for functional correctness of low-level (Jasmin) implementations against specifications; it is aimed at primitives and constructions rather than application code (EasyCrypt contributors (Formosa Crypto project), n.d.).
• CryptoVerif proves protocol-level secrecy, correspondence (authentication) and indistinguishability in the computational model, with the security assumptions on primitives stated explicitly, and can translate models to OCaml or F* (Blanchet et al., n.d.).

Misuse detection

Cryptographic API misuse detectors check usage rules without proving properties. CrySL specifies correct API use as method-call sequences, data-flow constraints and constraints on algorithms and parameters, and compiles the rules to a static analysis of Java and Android apps (Krüger et al., 2018; Krüger et al., 2017). The authors report that 96 percent of 10,001 analysed Android apps had at least one crypto API misuse (Krüger et al., 2017), and that earlier lightweight syntactic checkers have many false negatives on non-trivial cryptography misuse (Krüger et al., 2018). A warning is judged against the written rule, “irrespective of that rule’s semantic correctness” (Krüger et al., 2018). The analysis can flag forbidden calls that are unreachable at runtime, because it depends on call-graph precision, and in the authors’ evaluation false negatives appeared when the off-the-shelf alias analysis timed out, so a clean report is not a guarantee (Krüger et al., 2018).

Questions, controversies, and new developments

What a proof of correct use does not catch: key commitment

Key commitment means that a ciphertext decrypts only under the key that made it: each ciphertext decrypts to a single plaintext (Amazon Web Services (Encryption SDK Developer Guide), n.d.). The AWS developer guide describes the failure as one ciphertext decrypting under two different keys to different plaintexts (Amazon Web Services (Encryption SDK Developer Guide), n.d.). Non-committing AEADs, including AES-GCM, XSalsa20/Poly1305 and ChaCha20/Poly1305, enable partitioning oracle attacks, and the authors call for committing AEAD (Len et al., 2020).

A proof of ordinary correctness holds for the honest single-key case; the key commitment failure needs a second, adversarially chosen key, which a same-key round-trip statement does not mention (Amazon Web Services (Encryption SDK Developer Guide), n.d.). So the property needs its own statement. In the Dafny SDK, key commitment appears as a requirement on encrypt (only commitment-bearing suites) and a policy check that makes encrypt fail, proved as an explicit postcondition, not obtained from functional correctness (AWS (aws-encryption-sdk-dafny contributors, n.d.a). At the format level, the V2 header reader fails unless the algorithm suite uses HKDF commitment, and the specification requires the header’s suite data to be the derived commit key. The code proves the format is read and written consistently; that the commit key binds the ciphertext to one data key rests on HKDF and AES-GCM primitives outside the proof (AWS Encryption SDK maintainers (Serialize), n.d.).

The known vulnerabilities concern code outside the proof. CVE-2020-8897 was in the AWS Encryption SDKs for Java, Python, C and JavaScript before 2.0.0, before the Dafny SDK existed; the fix was a new major version adding key commitment (CVE Program, 2020). In 2026 the hand-written Python SDK had a key commitment policy bypass through a shared key cache, a bug in the caching layer, not in the AEAD primitive (Open Source Vulnerabilities, 2026). A separate 2025 bulletin describes a key commitment issue in S3 Encryption Clients that arises when the encrypted data key is stored in an instruction file, not cryptographically bound to the ciphertext (Amazon Web Services, 2025).

Can information-flow verifiers say what encryption promises?

Computational statements about encryption come from two routes. EasyCrypt proves security of cryptographic systems as a sequence of games, a computational-security tool class separate from information-flow verifiers (Barthe et al., 2011). A line of type-system work states cryptographic hypotheses as probabilistic polynomial-time games and obtains computational noninterference for probabilistic programs; information-flow checking reaches computational statements only when the type system builds in those assumptions (Fournet & Rezk, 2008). That work describes its result as a language-based model ranging from computational noninterference down to standard cryptographic hypotheses, with type rules for controlled robust declassification and endorsement (Fournet & Rezk, 2008).

Symbolic versus computational models

The symbolic-execution approach to C code depends on a computational soundness result requiring IND-CCA encryption, and some programs fell outside it (Aizatulin et al., 2011). CryptoVerif works in the computational model directly and states the assumptions on primitives explicitly (Blanchet et al., n.d.).

Broader connections

The trace-versus-hyperproperty distinction links verification of encryption-calling code to information-flow control (Clarkson & Schneider, 2010) and to relational verification (Naumann, 2020). It also connects to the theory of authenticated encryption, since properties such as key commitment come from cryptographic analysis of the primitive rather than from the calling code (Len et al., 2020).

Further reading

• Clarkson and Schneider, Hyperproperties (Clarkson & Schneider, 2010): the definitions of trace property and hyperproperty, and why noninterference is the latter.
• Aizatulin, Gordon and Jürjens (Aizatulin et al., 2011): symbolic models extracted from C protocol code, with the computational soundness caveats.
• The AES-GCM extern contract in the AWS Cryptographic Material Providers library (AWS Cryptographic Material Providers Library maintainers, n.d.): a compact example of a primitive assumed through axiom predicates.
• Duvet (awslabs (Duvet maintainers), n.d.): how specification text is linked to code.
• Krüger and colleagues, CrySL (Krüger et al., 2018): rule-based misuse detection and its limits.
• Galois on verifying s2n HMAC with SAW (Galois, 2016): a bounded equivalence proof of C code against a Cryptol specification.