Cookie replies

wg_cookie_message_create writes exactly the model's cookie reply, and wg_cookie_message_consume on any 64 bytes, with any peers and tables, updates exactly the cookie the model updates, or nothing.

spec: x_cookie_reply
length: 283 lines of C
own proof: 15,240 lines of Rocq
status: Proved; 29 of 38

On this page

The spec

The property is stated by the C program harness/x_cookie_reply.c, 283 lines. Here is its main cut down to the inputs it draws, the calls into the code under test and the checks (lines 61–283; ... marks lines left out). The checks call helpers and the model in the spec and in harness/common.h.

int main(void)
{
	...
	wg_shim_boottime_ns = draw_boottime();
	wg_noise_init();
	nondet_bytes(raw_a, 32);
	nondet_bytes(raw_b, 32);
	...
	wg_cookie_message_create(reply, &skb, index, &wb.cookie_checker);
		...
		CHECK(bytes_eq(reply->nonce, wg_shim_random_log_prev, 24));
	...
	CHECK(wb.cookie_checker.secret_birthdate == secret_birth && bytes_eq(wb.cookie_checker.secret, secret, 32));
	...
	CHECK(reply->header.type == MESSAGE_HANDSHAKE_COOKIE && reply->receiver_index == index);
	xchacha20poly1305_encrypt(enc, cookie, 16, msg + len - 32, 16, reply->nonce, k);
	CHECK(bytes_eq(reply->encrypted_cookie, enc, 32));
	...
	CHECK(dev_same(&db, &wb) && skb_same(&sks, &skb));
	...
	for (i = 0; i < n; i++) {
	...
	for (it = peers; it; it = it->next) {
	...
	for (cn = cns; cn; cn = cn->next)
	...
	wg_cookie_message_consume(reply, &wa);
	...
	for (e = ita.head; e != NULL && e->index != reply->receiver_index; e = e->next)
		    ...
		    !xchacha20poly1305_decrypt(pt, reply->encrypted_cookie, 32, target->cs.last_mac1_sent, 16, reply->nonce,
			...
			CHECK(ck_same(&cn->cs, &cn->n->p->latest_cookie));
		...
		CHECK(hnodes_same_except(peers, tn->p));
		CHECK(hs_same(&tn->snap, &tn->p->handshake) && tn->p->refcount.refcount == tn->refs &&
	...
	CHECK(bytes_eq(img, img2, COOKIE_MSG_LEN));
		...
		CHECK(bytes_eq(np->p->latest_cookie.cookie, cookie, 16));
...
}

The full spec at commit 3c1fc13 ↗

The property as the spec's first comment states it

Law `cookie_reply`: the cookie reply message (wg_cookie_message_create) and its consumption
(wg_cookie_message_consume) against the model: exact bytes, the round trip, and ANY reply bytes.

Responder device B with ANY static key, ANY cookie secret and secret age; a packet with ANY message of length >=
32 (its mac1 at len-32), IPv4/IPv6/other source, ANY source address and port; ANY receiver index; ANY boot clock.
Initiator device A with ANY static key and ANY number of peers (unique public keys, ANY cookie states and other
mutable peer state (common.h peer_randomize_rest), any reference count below INT_MAX), whose handshake entries are
in A's index table or not, plus ANY number of keypairs (whole objects of ANY content, common.h kents_add) of ANY
peers in the table, possibly in their peers' slots; one peer P has B's public key.  The reply A consumes is B's
reply (honest: P's handshake index, P remembers the packet's mac1 and has sent it), or B's
reply with one byte changed, or ANY 64 bytes (receiver index drawn or taken from the table).
Claims:
 - create writes exactly: type 3, the receiver index, the nonce = 24 random bytes (the shim's draw), the
   cookie encrypted = XChaCha20-Poly1305(key HASH("cookie--" || S_pub_B), nonce, cookie, ad = the packet's
   mac1), where the cookie is MAC32(secret, source address || port) after the secret's rotation at age >= 120 s
   ((s64)(birthdate + 120 s) <= (s64)now: at exactly 120 s the secret is new; as in law cookie_mac); B's
   checker changes only by that rotation (B as a whole - identity, both checker keys, the checker's
   device, tables - but that rotation); the packet is not modified (no field of it: data, length,
   protocol, source address and port);
 - consume accepts exactly when: the table entry with the receiver index exists (handshake or keypair entry),
   its peer has sent a mac1, and the encrypted cookie decrypts under that peer's cookie key
   HASH("cookie--" || its remote static) with its last mac1 as associated data.  Then that peer's cookie
   state is exactly: cookie = the plaintext, birthdate = now, valid, mac1 no longer pending; else nothing
   changes.  Other peers never change; references are balanced; the reply is not modified;
 - (whole-state frame) consume changes nothing but that cookie state: every other peer as a whole, the
   rest of that peer (handshake, reference count, keypair slots, ...), device A (identity, cookie checker,
   public-key table), the index table (first entry, every entry's peer, type, index, membership, list link), every
   keypair (byte for byte) stay as they were, and nothing is allocated or freed, no peer is released and no
   reference count warns;
 - round trip: if B has an identity, B's unmodified reply to a packet whose mac1 P sent is accepted, and P then
   holds exactly B's cookie for that source.

The code it is about

wg_cookie_message_consume in drivers/net/wireguard/cookie.c, lines 200–240:

void wg_cookie_message_consume(struct message_handshake_cookie *src,
			       struct wg_device *wg)
{
	struct wg_peer *peer = NULL;
	u8 cookie[COOKIE_LEN];
	bool ret;

	if (unlikely(!wg_index_hashtable_lookup(wg->index_hashtable,
						INDEX_HASHTABLE_HANDSHAKE |
						INDEX_HASHTABLE_KEYPAIR,
						src->receiver_index, &peer)))
		return;

	/* QUICKPROOF P09: `goto out` is `break` out of this block (VST has no goto); same statements in the same order */
	do {
	down_read(&peer->latest_cookie.lock);
	if (unlikely(!peer->latest_cookie.have_sent_mac1)) {
		up_read(&peer->latest_cookie.lock);
		break;
	}
	ret = xchacha20poly1305_decrypt(
		cookie, src->encrypted_cookie, sizeof(src->encrypted_cookie),
		peer->latest_cookie.last_mac1_sent, COOKIE_LEN, src->nonce,
		peer->latest_cookie.cookie_decryption_key);
	up_read(&peer->latest_cookie.lock);

	if (ret) {
		down_write(&peer->latest_cookie.lock);
		memcpy(peer->latest_cookie.cookie, cookie, COOKIE_LEN);
		peer->latest_cookie.birthdate = ktime_get_coarse_boottime_ns();
		peer->latest_cookie.is_valid = true;
		peer->latest_cookie.have_sent_mac1 = false;
		up_write(&peer->latest_cookie.lock);
	} else {
		net_dbg_ratelimited("%s: Could not decrypt invalid cookie response\n",
				    wg->dev->name);
	}

	} while (0); /* QUICKPROOF P09: was the label `out:` */
	wg_peer_put(peer);
}

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

Rocq

Theorem x_cookie_reply : 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:

Rocq

Theorem x_cookie_reply : harness_safe WgNoise.contracts.x_cookie_reply.whole_prog.
Proof. exact (proj1 (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.

The C files (units) its program links

drivers/net/wireguard/noise.c
drivers/net/wireguard/cookie.c
patch/counter_validate.c
lib/crypto/blake2s.c
lib/crypto/chacha.c
lib/crypto/chacha-block-generic.c
lib/crypto/poly1305.c
lib/crypto/poly1305-donna32.c
lib/crypto/chacha20poly1305.c
lib/crypto/curve25519.c
lib/crypto/curve25519-fiat32.c
patch/wg_shim.c
quickproof/libc/libc.c
quickproof/libc/malloc_unit.c

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.

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

How it was proved

src/proof/harness/cookie_reply/ holds 15,240 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 cookie.c: see the list on the left, or the summary.

The spec#

The code it is about#

The theorem#

What it leaves out#

How it was proved#

The spec

The code it is about

The theorem

What it leaves out

How it was proved