Browse WireGuard specs (21 of 38)

Proofs / WireGuard / Earlier, longer properties

Creating handshake messages

From any prior state of the device, the peer and its handshake, wg_noise_handshake_create_initiation and wg_noise_handshake_create_response return what the model returns, write exactly the model's message bytes and handshake fields, and change nothing else, on every failure path too.

  • Every way the creation can stop is covered: no usable identity, a zero ephemeral key, a zero Diffie-Hellman result, and success.
  • The message buffer starts with arbitrary bytes, so the property also says which bytes are left alone. The two MACs are never written here.
spec
x_create_any
length
188 lines of C
own proof
7,723 lines of Rocq
status
Proved
21 of 38
On this page

The spec

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

C
int main(void)
{
	...
	wg_shim_boottime_ns = draw_boottime();
	wg_noise_init();
	nondet_bytes(raw, 32);
	nondet_bytes(pub, 32);
	nondet_bytes(psk, 32);
	use_psk = nondet_u8() & 1;
	...
	CHECK(bytes_eq(p.handshake.precomputed_static_static, dh, 32));
	...
	p.refcount.refcount = draw_peer_refs();
	if (nondet_u8() & 1)
	...
	op = nondet_u8() & 1;
			...
			draw_real_clock();
			...
			r = wg_noise_handshake_create_initiation(m, &p.handshake);
				...
				CHECK(!bytes_zero(eph, 32));
			...
			CHECK(r == ok && bytes_eq(img, exp, INIT_LEN));
			...
			r = wg_noise_handshake_create_response(m, &p.handshake);
			...
			CHECK(r == ok && bytes_eq(img, exp, RESP_LEN));
		...
		CHECK(p.handshake.entry.index == wg_shim_random_u32 && table_has(&ita, &p.handshake.entry) &&
	...
	CHECK(hs_same(&x, &p.handshake));
	...
	CHECK(kents_same_but_next(kes, &ita));
	for (ke = kes; ke; ke = ke->next) {
		CHECK(ke->kp.entry.hashed);
	...
	CHECK(table_len(&ita) == n);
	...
	CHECK(pr_same(&ps, &p) && p.refcount.refcount == refs0 && dev_same(&ds, &wa) && shim_same(&ss));
...
}

The full spec at commit 3c1fc13 ↗

The property as the spec's first comment states it 
Law `create_any`: wg_noise_handshake_create_initiation and wg_noise_handshake_create_response from ANY prior
state, including every failure path, against a step-by-step model.

State: a device with ANY static key (usable or not); a peer with ANY public key (degenerate ones included:
the precomputed static-static DH may be zero) and ANY preshared key or none; ANY mutable handshake state
(common.h hs_randomize) and ANY other mutable peer state (common.h peer_randomize_rest), any reference count below
INT_MAX (common.h draw_peer_refs), its
index entry hashed or not, ANY number of keypairs of the peer (whole objects of ANY content,
common.h kents_add) in the table, possibly in its slots; ANY ephemeral randomness and
real-time clock; the output message pre-filled with ANY bytes.
Claims, for the call and for the model's step at which it stops (identity, ephemeral public key zero, es / ee /
se DH zero, precomputed ss zero, success):
 - the return value is true exactly at success;
 - EVERY byte of the output message is the model's: the fields written before the stop (type, receiver index,
   ephemeral, encrypted static / timestamp / nothing, sender index at success) and the pre-filled bytes
   elsewhere (the macs are never written);
 - EVERY field of the handshake is the model's: chaining key, hash and ephemeral private key as they are at the
   stop (create_initiation restarts the hash chain from the peer's public key; create_response continues from
   the current one), state CREATED_INITIATION / CREATED_RESPONSE only at success, everything else unchanged;
 - create_response does nothing at all unless the state is CONSUMED_INITIATION; create_initiation nothing
   without an identity;
 - at success the handshake's entry is (re)inserted with the random index the table drew, unique; the other
   entries of the table never change (peer, type, index, membership);
 - (whole-state frame) the rest of the peer (cookie state, keypair slots, last sent handshake, dead
   flag, ...) and its reference count, and the device (identity, cookie checker, public-key table) never change,
   and nothing is allocated or freed; no reference count warns.

The code it is about

wg_noise_handshake_create_initiation in drivers/net/wireguard/noise.c, lines 514–581 (... marks lines left out):

C
bool
wg_noise_handshake_create_initiation(struct message_handshake_initiation *dst,
				     struct noise_handshake *handshake)
{
	u8 timestamp[NOISE_TIMESTAMP_LEN];
	u8 key[NOISE_SYMMETRIC_KEY_LEN];
	bool ret = false;

	/* We need to wait for crng _before_ taking any locks, since
	 * curve25519_generate_secret uses get_random_bytes_wait.
	 */
	wait_for_random_bytes();

	down_read(&handshake->static_identity->lock);
	down_write(&handshake->lock);

	/* QUICKPROOF P03: `goto out` is `break` out of this block (VST has no goto); same statements in the same order */
	do {
	if (unlikely(!handshake->static_identity->has_identity))
		break;

	dst->header.type = cpu_to_le32(MESSAGE_HANDSHAKE_INITIATION);

	handshake_init(handshake->chaining_key, handshake->hash,
		       handshake->remote_static);

	/* e */
	curve25519_generate_secret(handshake->ephemeral_private);
	if (!curve25519_generate_public(dst->unencrypted_ephemeral,
					handshake->ephemeral_private))
		break;
	message_ephemeral(dst->unencrypted_ephemeral,
			  dst->unencrypted_ephemeral, handshake->chaining_key,
			  handshake->hash);

	/* es */
	if (!mix_dh(handshake->chaining_key, key, handshake->ephemeral_private,
		    handshake->remote_static))
...
}

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

Rocq
Theorem x_create_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_create_any : harness_safe WgNoise.contracts.x_create_any.whole_prog.
Proof. exact (proj1 (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.

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/create_any/ holds 7,723 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.