Browse WireGuard specs (3 of 38)

Proofs / WireGuard / The handshake

hs_begin_session_state

Beginning a session from a handshake in any state but HANDSHAKE_CREATED_RESPONSE or HANDSHAKE_CONSUMED_RESPONSE fails, allocates nothing and leaves the three keypair slots as they were.

spec
42 lines of C
with its headers
105 lines
status
Proved
3 of 38
On this page

The spec

The spec is the C program harness/hs_begin_session_state.c, 42 lines, shown whole as it is in the repository at 3c1fc13. It includes harness/hs_laws.h (63 lines). Its first comment states the property in full, with every bound.

C
// Law hs_begin_session_state: For devices A and B with any private keys and any preshared key, and any sequence of
// any number of calls of wg_noise_handshake_begin_session on A's handshake with B, before each of which the handshake's
// state field is set to any 32-bit value and its ephemeral keys, hash, chaining key, remote index and latest timestamp
// to any bytes: every call made while the state is neither HANDSHAKE_CREATED_RESPONSE nor HANDSHAKE_CONSUMED_RESPONSE
// returns false, allocates nothing and leaves A's three keypair slots as they were. (The other calls may create
// keypairs, so the slots hold any keypairs that such calls left; the shim's allocator may fail at any call.)
#include "hs_laws.h"

int main(void) {
	// Choose the inputs: the devices and their keys
	struct pair p;
	new_pair(&p);
	struct noise_handshake *h = &p.a_peer.handshake;
	struct noise_keypairs *slots = &p.a_peer.keypairs;
	do {
		// Any session state of the handshake
		h->state = (enum noise_handshake_state) nondet_u32();
		h->remote_index = nondet_u32();
		nondet_bytes(h->ephemeral_private, 32);
		nondet_bytes(h->remote_ephemeral, 32);
		nondet_bytes(h->hash, 32);
		nondet_bytes(h->chaining_key, 32);
		nondet_bytes(h->latest_timestamp, 12);
		int completed = h->state == HANDSHAKE_CREATED_RESPONSE || h->state == HANDSHAKE_CONSUMED_RESPONSE;
		struct noise_keypair *current = slots->current_keypair;
		struct noise_keypair *previous = slots->previous_keypair;
		struct noise_keypair *next = slots->next_keypair;
		unsigned long allocations = wg_shim_allocs;
		// Begin a session. WireGuard paper, 5.4.5: "After the above two messages have been exchanged, keys are
		// calculated by the initiator and responder for sending and receiving transport data messages"; Noise,
		// 5.3, ReadMessage/WriteMessage: "If there are no more message patterns returns two new CipherState
		// objects by calling Split()".
		bool began = wg_noise_handshake_begin_session(h, slots);
		// Check
		if (completed == 0) {
			gp_assert(began == 0 && wg_shim_allocs == allocations);
			gp_assert(slots->current_keypair == current && slots->previous_keypair == previous);
			gp_assert(slots->next_keypair == next);
		}
	} while (nondet_u8() != 0);
	return 0;
}
harness/hs_laws.h, 63 lines
C
// hs_laws.h: helpers shared by the handshake laws (hs_*): two devices with a peer for each other, set up as the
// kernel sets them up, and any clocks. No models, no algorithms.
#include "quickproof.h"
#include "noise.h"
#include "peer.h"
#include "device.h"
extern u64 wg_shim_boottime_ns;                       // the shim's clocks (patch/wg_shim.c): the laws set them
extern s64 wg_shim_real_sec;
extern long wg_shim_real_nsec;
extern unsigned long wg_shim_allocs;                  // the shim's count of successful kzalloc calls
static u64 any_u64(void) {                            // any 64-bit value
	u64 high = nondet_u32();
	return high << 32 | nondet_u32();
}
static int bytes_eq(const u8 *a, const u8 *b, size_t n) {   // a[0..n-1] == b[0..n-1]
	for (size_t i = 0; i < n; i++)
		if (a[i] != b[i])
			return 0;
	return 1;
}
static void any_clocks(void) {                        // any boot clock below 2^62 ns, any real-time clock
	wg_shim_boottime_ns = any_u64() >> 2;
	wg_shim_real_sec = (s64) any_u64();
	wg_shim_real_nsec = (long) (nondet_u32() % 1000000000u);
}
static void new_device(struct wg_device *wg, struct index_hashtable *indices, struct pubkey_hashtable *keys,
		       const u8 private_key[32]) {    // device.c (kzalloc'd), its private key set as netlink.c sets it
	wg->index_hashtable = indices;
	wg->peer_hashtable = keys;
	indices->head = NULL;
	keys->head = NULL;
	for (size_t i = 0; i < 32; i++)
		wg->static_identity.static_public[i] = 0;
	wg_noise_set_static_identity_private_key(&wg->static_identity, private_key);
}
static void new_peer(struct wg_peer *peer, struct wg_device *wg, const u8 public_key[32], const u8 psk[32]) {
	peer->device = wg;                            // peer.c, wg_peer_create: one reference, no keypairs, a new
	peer->is_dead = false;                        // handshake, listed in the device's public-key table
	peer->keypairs.current_keypair = NULL;
	peer->keypairs.previous_keypair = NULL;
	peer->keypairs.next_keypair = NULL;
	peer->refcount.refcount = 1;
	wg_noise_handshake_init(&peer->handshake, &wg->static_identity, public_key, psk, peer);
	peer->pubkey_next = wg->peer_hashtable->head;
	wg->peer_hashtable->head = peer;
}
struct pair {                                         // devices A and B, each with a peer for the other
	struct wg_device a, b;
	struct index_hashtable a_indices, b_indices;
	struct pubkey_hashtable a_keys, b_keys;
	struct wg_peer a_peer, b_peer;                // a_peer: A's peer for B; b_peer: B's peer for A
};
static void new_pair(struct pair *p) {                // any private keys, any preshared key (the same on both sides)
	u8 a_private[32], b_private[32], psk[32];
	nondet_bytes(a_private, 32);
	nondet_bytes(b_private, 32);
	nondet_bytes(psk, 32);
	wg_noise_init();
	new_device(&p->a, &p->a_indices, &p->a_keys, a_private);
	new_device(&p->b, &p->b_indices, &p->b_keys, b_private);
	new_peer(&p->a_peer, &p->a, p->b.static_identity.static_public, psk);
	new_peer(&p->b_peer, &p->b, p->a.static_identity.static_public, psk);
}

The theorem

QuickProof generated this statement from the spec, in src/contracts/hs_begin_session_state.v:

Rocq
Theorem hs_begin_session_state : harness_safe whole_prog.

src/contracts/laws.v states it on the spec's own program, whole_prog (the spec linked with the code under test), with its proof:

Rocq
Theorem hs_begin_session_state : harness_safe WgNoise.contracts.hs_begin_session_state.whole_prog.
Proof. exact (proj1 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 WgNoise.contracts.suite.suite))))))). Qed.

Read as a statement about runs, it says that no run of the program has undefined behaviour or a failing check, for every value the spec can draw. That reading rests on VST's adequacy theorem, which is not yet instantiated in Rocq (formerly Coq) for QuickProof's environment.

The C files (units) its program links
  • drivers/net/wireguard/noise.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

What it leaves out

  • What the first comment of the spec excludes, and its bounds.
  • Like every spec of this proof: runs of more than one thread (the locks and RCU are those of one 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 says what the proof as a whole covers.

How it was proved

AI agents wrote the proof, and Rocq checks it. qp verify passes on this repository: this statement is the one generated from the spec at the contract commit, and its proof uses only Rocq's standard axioms and VST's abstract malloc library.