Clearing a handshake

The spec#

The property is stated by the C program harness/x_handshake_clear.c, 91 lines. Here is its main cut down to the inputs it draws, the calls into the code under test and the checks (lines 26–91; ... 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();
	nondet_bytes(raw, 32);
	...
	n = draw_steps();
	for (i = 0; i < n; i++) {
		nondet_bytes(pub, 32);
	...
	for (nd = peers; nd; nd = nd->next) {
		...
		if (nondet_u8() % 4 != 0)
	...
	wg_noise_handshake_clear(h);
	...
	CHECK(hs_zeroed_from(&target->snap, h) && !h->entry.hashed && h->entry.index == target->snap.index);
		...
		CHECK(h->entry.next == NULL);
		...
		CHECK(h->entry.next == target->snap.next);
	CHECK(target->p->refcount.refcount == target->refs && pr_same(&target->rest, target->p));
	...
	for (nd = peers; nd; nd = nd->next) {
		...
		CHECK(hs_same_but_next(&nd->snap, &nd->p->handshake) && nd->p->refcount.refcount == nd->refs &&
			...
			CHECK(table_has(&it, &nd->p->handshake.entry));
	...
	CHECK(kents_same_but_next(kes, &it));
	CHECK(table_len(&it) == hashed + kents_hashed(kes));
	CHECK(dev_same(&ds, &w) && shim_same(&ss));
...
}

The full spec at commit 3c1fc13 ↗

Law `handshake_clear`: wg_noise_handshake_clear from ANY state destroys exactly the handshake's
session secrets and its index, and nothing else.

State: a device 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), any reference count below INT_MAX (common.h draw_peer_refs); each peer's handshake entry is
in the device'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; the handshake cleared is that of ANY
peer P (hashed or not, in any state: clearing a cleared handshake is included).
Claims (the model: handshake_zero of the WireGuard paper's state machine, and the index table's removal):
 - P's handshake is exactly the zeroed one: state ZEROED, ephemeral private key, remote ephemeral key, hash,
   chaining key and remote index all zero; its long-term configuration (remote static key, precomputed
   static-static DH, preshared key, static identity) and its replay state (latest timestamp, last
   consumption time) unchanged: a cleared handshake still rejects every initiation it rejected before;
 - P's entry has left the index table (not hashed; its index, type and peer unchanged; its list link NULL if it
   was hashed, else unchanged): no receiver index leads to P's handshake any more;
 - the table holds exactly the other entries it held before, each once and unchanged (peer, type, index; every
   keypair byte for byte);
 - everything else is unchanged: the rest of P (cookie state, keypair slots, last sent handshake, dead flag,
   ...) and its reference count, every other peer as a whole (its entry's list link excepted: the entry before
   P's in the list now skips it), the device (identity, cookie checker, public-key table); nothing is
   allocated or freed, no peer is released and no reference count warns (common.h shim_same).

The code it is about#

wg_noise_handshake_clear in drivers/net/wireguard/noise.c, lines 88–96:

void wg_noise_handshake_clear(struct noise_handshake *handshake)
{
	down_write(&handshake->lock);
	wg_index_hashtable_remove(
			handshake->entry.peer->device->index_hashtable,
			&handshake->entry);
	handshake_zero(handshake);
	up_write(&handshake->lock);
}

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

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

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

How it was proved#

src/proof/harness/handshake_clear/ holds 5,622 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.