ChaCha20-Poly1305 and XChaCha20-Poly1305

The spec#

The property is stated by the C program harness/x_prim_aead.c, 15 lines. This is its main (lines 65–118 of harness/prim_aead.h):

int main(void)
{
	u8 key[32], xnonce[24];
	u64 nonce;
	size_t adlen, n;
	u8 *ad, *pt, *ct, *rct, *dec, *ad_copy, *pt_copy;
	int x, ok;

	x = nondet_u8() & 1;
	nondet_bytes(key, 32);
	nondet_bytes(xnonce, 24);
	nonce = draw_u64();
	adlen = draw_size();
	if (adlen > PTRDIFF_MAX)   /* no C object is larger than PTRDIFF_MAX: see the header comment */
		return 0;
	n = draw_size();
	if (n > PTRDIFF_MAX - 16)   /* no C object is larger than PTRDIFF_MAX, and ct/rct are n + 16 bytes */
		return 0;
	if (adlen > LEN_LIMIT || n > LEN_LIMIT || n > SIZE_MAX - 16)
		return 0;
	ad = malloc(adlen);
	ad_copy = malloc(adlen);
	pt = malloc(n);
	pt_copy = malloc(n);
	ct = malloc(n + 16);
	rct = malloc(n + 16);
	dec = malloc(n);
	if ((ad == NULL || ad_copy == NULL) || (pt == NULL || pt_copy == NULL || dec == NULL) ||
	    ct == NULL || rct == NULL) {
		free(ad); free(ad_copy); free(pt); free(pt_copy); free(ct); free(rct); free(dec);
		return 0;
	}
	nondet_bytes(ad, adlen);
	bytes_copy(ad_copy, ad, adlen);
	nondet_bytes(pt, n);
	bytes_copy(pt_copy, pt, n);

	if (x) {
		xchacha20poly1305_encrypt(ct, pt, n, ad, adlen, xnonce, key);
		ref_xaead_encrypt(rct, pt, n, ad, adlen, xnonce, key);
	} else {
		chacha20poly1305_encrypt(ct, pt, n, ad, adlen, nonce, key);
		ref_aead_encrypt(rct, pt, n, ad, adlen, nonce, key);
	}
	CHECK(bytes_eq(ct, rct, n + 16));
	ok = x ? xchacha20poly1305_decrypt(dec, ct, n + 16, ad, adlen, xnonce, key)
	       : chacha20poly1305_decrypt(dec, ct, n + 16, ad, adlen, nonce, key);
	CHECK(ok && bytes_eq(dec, pt, n));

	check_decrypt_any(x, key, nonce, xnonce, ad, adlen, ct, n);
	CHECK(bytes_eq(ad, ad_copy, adlen) && bytes_eq(pt, pt_copy, n));
	free(ad); free(ad_copy); free(pt); free(pt_copy); free(ct); free(rct); free(dec);
	return 0;
}

The full spec at commit 3c1fc13 ↗

Law `prim_aead`: the kernel's ChaCha20-Poly1305 and XChaCha20-Poly1305 (lib/crypto/chacha20poly1305.c over
chacha.c, chacha-block-generic.c, poly1305.c, poly1305-donna32.c) are the RFC 8439 constructions, for ANY
length of message and associated data (size_t, as the API declares).  Claim: see prim_aead.h.
FALSE on unmodified upstream for lengths of 2^32 and more (the length was truncated to 32 bits); the code under
test carries patches 4/5 and 5/5 of the lib/crypto series (P22, P23: size_t lengths in poly1305_update and
chacha_crypt; DEVIATIONS.md), applied verbatim.
Buffer lengths above PTRDIFF_MAX (2^63 - 1) end the run: no real C implementation creates an object larger than
PTRDIFF_MAX (pointer differences inside it must fit ptrdiff_t; glibc's malloc returns NULL beyond it), but
CompCert's memory model and VST's malloc_spec' allow objects of up to 2^64 - 1 bytes, which would make the law
cover buffers that cannot exist (e.g. blake2s_update's DIV_ROUND_UP(inlen, 64) wraps for inlen >= 2^64 - 63).
This is an assumption about the environment, recorded as DEVIATIONS.md L13; it may later move into the
framework's malloc specification.

The code it is about#

chacha20poly1305_encrypt in lib/crypto/chacha20poly1305.c, lines 89–110:

void chacha20poly1305_encrypt(u8 *dst, const u8 *src, const size_t src_len,
			      const u8 *ad, const size_t ad_len,
			      const u64 nonce,
			      const u8 key[at_least CHACHA20POLY1305_KEY_SIZE])
{
	struct chacha_state chacha_state;
	u32 k[CHACHA_KEY_WORDS];
	u8 iv[16]; /* QUICKPROOF P16: was __le64 iv[2], read through (u8 *)iv (VST: typed memory) */

	chacha_load_key(k, key);

	/* QUICKPROOF P16: iv[0] = 0; iv[1] = cpu_to_le64(nonce) as bytes */
	put_unaligned_le64(0, iv);
	put_unaligned_le64(nonce, iv + 8);

	chacha_init(&chacha_state, k, iv);
	__chacha20poly1305_encrypt(dst, src, src_len, ad, ad_len,
				   &chacha_state);

	memzero_explicit(iv, sizeof(iv));
	memzero_explicit(k, sizeof(k));
}

This is the code under test as the proof sees it: Linux at 551c722f with the two lib/crypto patches, and with the idiom rewrites that VST needs, each marked QUICKPROOF in the code and listed in DEVIATIONS.md.

The theorem#

QuickProof generated this statement from the spec in src/contracts/x_prim_aead.v:

Theorem x_prim_aead : harness_safe whole_prog.

whole_prog is the spec linked with the code under test. The 19 x_ specs are proved together, as the theorem suite_x, from one specification of every function of the code. src/contracts/laws.v states each spec on its own program and takes it from suite_x:

Theorem x_prim_aead : harness_safe WgNoise.contracts.x_prim_aead.whole_prog.
Proof. exact (proj1 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 WgNoise.contracts.suite.suite_x)))))))))))). Qed.

qp verify checks that this statement is the one generated from the spec at the contract commit, and that its proof uses no axiom beyond the 13 that every spec here uses: standard logical axioms and VST's abstract malloc library.

What it leaves out#

• Like every spec of this proof: runs of more than one thread (locks and RCU are those of a single thread), termination (a run that never returns is not a counterexample), and binaries built by a compiler (the theorem is about the code as CompCert defines C for 64-bit x86).
• The kernel around the code is a shim of plain C for one thread, and the code carries rewrites of idioms that VST cannot handle. Both are tested against the kernel's code, not proved.

Recorded for this property in DEVIATIONS.md (section L, what the properties exclude or assume):

• L08. x_prim_aead covers every size_t length of message and associated data Why: with P22 and P23, poly1305_update and chacha_crypt take the size_t lengths themselves
• L13. The specs x_prim_blake2s, x_prim_poly1305 and x_prim_aead end the run when a drawn buffer length (message, associated data, the bytes given to decrypt) exceeds PTRDIFF_MAX (2^63 - 1), and so do x_transport_order (payload length above PTRDIFF_MAX - 32) and x_transport_len (packet length above PTRDIFF_MAX - 32). The lengths are otherwise unbounded. The ae_ specs draw their lengths up to PTRDIFF_MAX (PTRDIFF_MAX - 16 for a message that gets a 16-byte tag) Why: no C implementation creates an object larger than PTRDIFF_MAX (pointer differences inside it must fit ptrdiff_t; glibc's malloc returns NULL beyond it), but CompCert's memory model and VST's malloc_spec' allow objects of up to 2^64 - 1 bytes, which would make the specs cover buffers that cannot exist: blake2s_update's DIV_ROUND_UP(inlen, 64) wraps for inlen of 2^64 - 63 or more. This is an assumption about the environment, not about the code

The summary page lists what the proof as a whole does not cover.

How it was proved#

src/proof/harness/prim_aead/ holds 5,836 lines of Rocq (formerly Coq) that are specific to this spec. It builds on the specifications and proofs of the functions of noise.c, cookie.c and lib/crypto, the protocol model, and the Diffie-Hellman agreement of X25519. The whole proof of the 38 specs is about 300,000 lines. AI agents wrote it, Rocq checks all of it, and nobody has to read it. What people have to read is the spec above, with harness/common.h, and the kernel shim that DEVIATIONS.md describes.

Other specs about lib/crypto: see the list on the left, or the summary.