Browse WireGuard specs (27 of 38)

Proofs / WireGuard / Earlier, longer properties

Configuring keys and peers

The seven configuration functions of noise.c and cookie.c, called over any prior contents, set exactly what the model says (a degenerate private key gives an unusable identity) and change nothing else.

  • The functions are called in the order that netlink.c, device.c and peer.c use when a device's key changes and a peer is added. Those callers are not in the code under test.
spec
x_config_any
length
177 lines of C
own proof
6,226 lines of Rocq
status
Proved
27 of 38
On this page

The spec

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

C
int main(void)
{
	...
	now = draw_boottime();
	...
	nondet_bytes(raw0, 32);
	...
	nondet_bytes(pub, 32);
	...
	nondet_bytes(w.static_identity.static_public, 32);
	...
	wg_noise_set_static_identity_private_key(&w.static_identity, raw);
	...
	CHECK(dev_same(&ds, &w) && hs_same(&hs0, &p.handshake) && pr_same(&ps0, &p) && p.refcount.refcount == refs0 &&
	...
	wg_noise_precompute_static_static(&p);
	...
	CHECK(dev_same(&ds, &w) && hs_same(&hs0, &p.handshake) && pr_same(&ps0, &p) && p.refcount.refcount == refs0 &&
	...
	wg_cookie_checker_precompute_device_keys(&w.cookie_checker);
	...
	CHECK(dev_same(&ds, &w) && hs_same(&hs0, &p.handshake) && pr_same(&ps0, &p) && p.refcount.refcount == refs0 &&
	...
	wg_cookie_checker_precompute_peer_keys(&p);
	...
	CHECK(dev_same(&ds, &w) && hs_same(&hs0, &p.handshake) && pr_same(&ps0, &p) && p.refcount.refcount == refs0 &&
	...
	wg_noise_handshake_init(&q.handshake, &w.static_identity, qpub, use_psk ? psk : NULL, &q);
	...
	CHECK(hs_same(&hq, &q.handshake));
	...
	wg_cookie_init(&q.latest_cookie);
	CHECK(q.latest_cookie.birthdate == 0 && !q.latest_cookie.is_valid && bytes_zero(q.latest_cookie.cookie, 16) &&
	...
	CHECK(hs_same(&hq, &q.handshake));
	CHECK(dev_same(&ds, &w) && hs_same(&hs0, &p.handshake) && pr_same(&ps0, &p) && p.refcount.refcount == refs0 &&
	...
	wg_cookie_checker_init(&w.cookie_checker, &w);
	...
	CHECK(dev_same(&ds, &w) && hs_same(&hs0, &p.handshake) && pr_same(&ps0, &p) && p.refcount.refcount == refs0 &&
...
}

The full spec at commit 3c1fc13 ↗

The property as the spec's first comment states it
Law `config_any`: the configuration functions of noise.c and cookie.c from ANY prior state.

The other laws set devices and peers up from zeroed memory (common.h setup_device, setup_peer); this one calls
each configuration function on ANY prior contents of what it writes, in the order netlink.c / device.c / peer.c
call them when a device's private key is changed and a peer is added:
 1. wg_noise_set_static_identity_private_key(identity, ANY 32 bytes) over ANY prior identity (any public and
    private key bytes, usable or not): private = clamp(key); public = X25519(key, 9), except that an all-zero
    key leaves the public key as it was; usable exactly when the key is not all zero and X25519(key, 9) is not
    zero (common.h m_identity_of);
 2. wg_noise_precompute_static_static(P) for a peer P with ANY public key and ANY prior precomputed bytes:
    X25519(private, P's key) if the identity is usable and that is not zero, else all zero;
 3. wg_cookie_checker_precompute_device_keys over ANY prior keys: HASH("cookie--" || S_pub) and
    HASH("mac1----" || S_pub) if the identity is usable, else both all zero;
 4. wg_cookie_checker_precompute_peer_keys(P) over ANY prior keys: HASH("cookie--" || P's key), HASH("mac1----"
    || P's key);
 5. a new peer Q: wg_noise_handshake_init over ANY prior handshake contents (every field drawn, pointers
    included) with ANY public key and ANY preshared key or none: the whole handshake is the initial one (entry of
    Q, type HANDSHAKE, not hashed, no link, index 0; state ZEROED; no last consumption; the device's identity;
    the remote static key and preshared key (zero if none) as given; precomputed DH as in 2; everything else
    zero); then wg_cookie_init over ANY prior cookie state: all zero;
 6. wg_cookie_checker_init over ANY prior secret, birthdate and device: a fresh random secret (the shim's draw),
    born now, the device; its keys unchanged.
After every step: nothing else changes (the device as a whole but the fields the step writes, P as a whole -
handshake, reference count, cookie state, keypair slots, ... - but those, Q's handshake after it is set up, the
index table and ANY keypairs of P - whole objects of any content, in the table and possibly in P's slots - byte for
byte), and nothing is allocated or freed; no reference count warns.

The code it is about

wg_noise_set_static_identity_private_key in drivers/net/wireguard/noise.c, lines 294–303:

C
void wg_noise_set_static_identity_private_key(
	struct noise_static_identity *static_identity,
	const u8 private_key[NOISE_PUBLIC_KEY_LEN])
{
	memcpy(static_identity->static_private, private_key,
	       NOISE_PUBLIC_KEY_LEN);
	curve25519_clamp_secret(static_identity->static_private);
	static_identity->has_identity = curve25519_generate_public(
		static_identity->static_public, private_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_config_any.v:

Rocq
Theorem x_config_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_config_any : harness_safe WgNoise.contracts.x_config_any.whole_prog.
Proof. exact (proj1 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/config_any/ holds 6,226 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.