Poly1305

The spec#

The property is stated by the C program harness/x_prim_poly1305.c, 68 lines. This is its main (lines 25–68):

int main(void)
{
	struct poly1305_desc_ctx d;
	u8 key[32], key0[32];
	u8 *msg, *copy, *tag, ref[16];
	size_t n, pos, i;

	nondet_bytes(key, 32);
	bytes_copy(key0, key, 32);
	n = draw_size();
	if (n > PTRDIFF_MAX)   /* no C object is larger than PTRDIFF_MAX: see the header comment */
		return 0;
	msg = malloc(n);
	copy = malloc(n);
	tag = malloc(16);
	if ((msg == NULL || copy == NULL) || tag == NULL) {
		free(msg); free(copy); free(tag);
		return 0;
	}
	nondet_bytes(msg, n);
	bytes_copy(copy, msg, n);
	poly1305_init(&d, key);
	pos = 0;
	while (pos < n) {
		size_t c = nondet_size();
		if (c > n - pos)
			c = n - pos;
		poly1305_update(&d, msg + pos, c);
		pos += c;
	}
	poly1305_final(&d, tag);
	ref_poly1305(ref, key, msg, n);
	CHECK(bytes_eq(tag, ref, 16));
	CHECK(bytes_zero(d.buf, 16) && d.buflen == 0);
	for (i = 0; i < 4; i++)
		CHECK(d.s[i] == 0);
	for (i = 0; i < 5; i++)
		CHECK(d.state.h.h[i] == 0 && d.state.core_r.key.r[i] == 0);
	for (i = 0; i < 4; i++)
		CHECK(d.state.core_r.precomputed_s.r[i] == 0);
	CHECK(bytes_eq(msg, copy, n) && bytes_eq(key, key0, 32));
	free(msg); free(copy); free(tag);
	return 0;
}

The full spec at commit 3c1fc13 ↗

Law `prim_poly1305`: the kernel's Poly1305 (lib/crypto/poly1305.c over poly1305-donna32.c) is Poly1305 (RFC 8439
2.5, the TweetNaCl-style reference ref_poly1305 of common.h), through its own streaming API.

For ANY 32-byte key and ANY message of any length (exact-size buffer) fed to poly1305_update in ANY split into
chunks (empty ones included; each chunk of ANY size_t length, the parameter being a size_t with patch P22 of
the series; chunks of 2^32 bytes and more run poly1305_update's UINT_MAX loop):
 - poly1305_final writes exactly the reference tag into a 16-byte buffer;
 - the context is all zero afterwards (poly1305_final clears it);
 - the message and key are not modified.
(The AEAD law only reaches whole 16-byte blocks; this law covers the partial final block.)
FALSE on unmodified upstream for a chunk of 2^32 - buflen bytes or more with 1..15 bytes buffered (buflen +
nbytes wrapped) and, with the parameter a size_t, for any chunk of 2^32 bytes or more (upstream's parameter is
an unsigned int: only length mod 2^32 bytes would be hashed); the code under test carries patch 4/5 of the
lib/crypto series (P22, 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#

poly1305_update in lib/crypto/poly1305.c, lines 37–67:

void poly1305_update(struct poly1305_desc_ctx *desc,
		     const u8 *src, size_t nbytes)
{
	if (nbytes >= POLY1305_BLOCK_SIZE - desc->buflen) {
		if (desc->buflen) {
			unsigned int l = POLY1305_BLOCK_SIZE - desc->buflen;

			memcpy(&desc->buf[desc->buflen], src, l);
			src += l;
			nbytes -= l;

			poly1305_blocks(&desc->state, desc->buf,
					POLY1305_BLOCK_SIZE, 1);
			desc->buflen = 0;
		}

		while (nbytes >= POLY1305_BLOCK_SIZE) {
			/* poly1305_blocks() takes an unsigned int length. */
			unsigned int bulk_len = round_down(min(nbytes, UINT_MAX),
							   POLY1305_BLOCK_SIZE);

			poly1305_blocks(&desc->state, src, bulk_len, 1);
			src += bulk_len;
			nbytes -= bulk_len;
		}
	}
	if (nbytes) {
		memcpy(&desc->buf[desc->buflen], src, nbytes);
		desc->buflen += nbytes;
	}
}

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_poly1305.v:

Theorem x_prim_poly1305 : 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_poly1305 : harness_safe WgNoise.contracts.x_prim_poly1305.whole_prog.
Proof. exact (proj1 (proj2 (proj2 (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):

• L11. x_prim_poly1305 gives poly1305_update chunks of any size_t length, bounded only by the message, itself bounded by L13 Why: with P22, poly1305_update takes a size_t
• 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_poly1305/ holds 4,257 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.