Accepting a response

wg_noise_handshake_consume_response on any 92 bytes and any contents of the index table accepts exactly when the model does; it then updates the peer exactly as the model does, and on rejection it changes nothing.

Acceptance needs a handshake entry with that receiver index in the state CREATED_INITIATION, two non-zero Diffie-Hellman results, and an empty payload whose tag verifies.

spec: x_consume_response_any
length: 170 lines of C
own proof: 9,872 lines of Rocq
status: Proved; 23 of 38

On this page

The spec

The property is stated by the C program harness/x_consume_response_any.c, 170 lines. Here is its main cut down to the inputs it draws, the calls into the code under test and the checks (lines 29–170; ... 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);
	...
	n = draw_steps();
	for (i = 0; i < n; i++) {
		nondet_bytes(pub, 32);
	...
	for (it = peers; it; it = it->next) {
		...
		if (nondet_u8() % 4 != 0)
		...
		mode = nondet_u8() % 3;
		if (mode == 0 && ita.head != NULL && (nondet_u8() & 1)) {
			...
			size_t k = nondet_size();
			...
			nondet_bytes(eraw, 32);
		...
		ret = wg_noise_handshake_consume_response(msg, &wa);
		...
		CHECK(bytes_eq(img, img_after, RESP_LEN));
		CHECK(dev_same(&ds, &wa) && ita.head == head0 && kents_same(kes) && shim_same(&ss));
			...
			CHECK(ret == NULL && hnodes_same_except(peers, NULL));
			...
			CHECK(ret == target->p && target->p->refcount.refcount == target->refs + 1);
			...
			CHECK(hnodes_same_except(peers, target->p));
			CHECK(h->state == HANDSHAKE_CONSUMED_RESPONSE);
			CHECK(bytes_eq(h->remote_ephemeral, msg->unencrypted_ephemeral, 32));
			CHECK(bytes_eq(h->hash, st.h, 32) && bytes_eq(h->chaining_key, st.ck, 32));
			CHECK(h->remote_index == msg->sender_index);
			CHECK(h->entry.peer == s->peer && h->entry.next == s->next && h->entry.hashed == s->hashed &&
			...
			CHECK(target->p->refcount.refcount == target->refs && pr_same(&target->rest, target->p));
...
}

The full spec at commit 3c1fc13 ↗

The property as the spec's first comment states it

Law `consume_response_any`: wg_noise_handshake_consume_response on ANY message and ANY prior state.

State: initiator device A with ANY static private key; ANY number of peers (unique public keys) with ANY public
and preshared keys, ANY mutable handshake state (common.h hs_randomize), ANY other mutable peer state (common.h
peer_randomize_rest: dead flag, last sent handshake, cookie state), any reference count below INT_MAX (common.h
draw_peer_refs); each peer's handshake entry is in A's index table or not (any), and ANY number of keypairs (whole
objects of ANY content, common.h kents_add) of ANY peers are in the table too, possibly in their peers' slots; one
peer (B) has a public key whose private key the harness knows; ANY boot clock. Message: ANY 92 bytes (with the
receiver index drawn, or one of the table's indices), or B's valid response to that peer's CURRENT state (built by
the model from the peer's hash, chaining key, ephemeral and preshared key, any responder ephemeral), optionally
with one byte changed.
Claims (exact agreement with the model, common.h):
 - the result is the peer the model accepts, or NULL; acceptance exactly when: A has an identity, the table's
   entry with the receiver index exists and is a handshake entry, its peer's state is CREATED_INITIATION,
   DH(E_a, E_msg) and DH(S_a, E_msg) are not zero and the empty payload's tag verifies under the key and hash
   of Noise_IKpsk2 (psk mixed in);
 - on acceptance, that handshake is exactly: state CONSUMED_RESPONSE, remote ephemeral = the message's, hash and
   chaining key = the model's, remote index = the message's sender index; everything else of it and ALL the
   rest of that peer (cookie state, keypair slots, last sent handshake, dead flag, ...), every other peer as a
   whole, unchanged; the peer holds one more reference;
 - on rejection NOTHING changes: every peer as a whole (handshake byte for byte, references, cookie state, ...);
 - in both cases (whole-state frame): the device (identity, cookie checker, public-key table) and the
   index table (its first entry, every entry's peer, type, index, membership and list link) and every keypair (byte
   for byte) are unchanged, nothing is allocated or freed, no peer is released and no reference count warns; the
   message is never modified.

The code it is about

wg_noise_handshake_consume_response in drivers/net/wireguard/noise.c, lines 732–825 (... marks lines left out):

struct wg_peer *
wg_noise_handshake_consume_response(struct message_handshake_response *src,
				    struct wg_device *wg)
{
	enum noise_handshake_state state = HANDSHAKE_ZEROED;
	struct wg_peer *peer = NULL, *ret_peer = NULL;
	struct noise_handshake *handshake;
	u8 key[NOISE_SYMMETRIC_KEY_LEN];
	u8 hash[NOISE_HASH_LEN];
	u8 chaining_key[NOISE_HASH_LEN];
	u8 e[NOISE_PUBLIC_KEY_LEN];
	u8 ephemeral_private[NOISE_PUBLIC_KEY_LEN];
	u8 static_private[NOISE_PUBLIC_KEY_LEN];
	u8 preshared_key[NOISE_SYMMETRIC_KEY_LEN];
	bool quickproof_success = false; /* QUICKPROOF P06 */

	down_read(&wg->static_identity.lock);

	/* QUICKPROOF P06: `goto out` is `break` out of the outer block, `goto fail` `break` out of the inner block,
	 * and the fail path runs when the inner block did not reach its end (VST has no goto); same statements
	 * in the same order */
	do {
	if (unlikely(!wg->static_identity.has_identity))
		break;

	handshake = (struct noise_handshake *)wg_index_hashtable_lookup(
		wg->index_hashtable, INDEX_HASHTABLE_HANDSHAKE,
		src->receiver_index, &peer);
	if (unlikely(!handshake))
		break;

	down_read(&handshake->lock);
	state = handshake->state;
	memcpy(hash, handshake->hash, NOISE_HASH_LEN);
	memcpy(chaining_key, handshake->chaining_key, NOISE_HASH_LEN);
	memcpy(ephemeral_private, handshake->ephemeral_private,
	       NOISE_PUBLIC_KEY_LEN);
	memcpy(preshared_key, handshake->preshared_key,
...
}

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

Rocq

Theorem x_consume_response_any : 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_consume_response_any : harness_safe WgNoise.contracts.x_consume_response_any.whole_prog.
Proof. exact (proj1 (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/consume_response_any/ holds 9,872 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 noise.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