Keepalives

The spec#

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

int main(void)
{
	...
	nondet_bytes(key, 32);
	...
	steps = draw_steps();
	for (i = 0; i < steps; i++) {
		...
		kind = nondet_u8() % 4;
			...
			enc_len = nondet_u8() % 16;    // 0..15: a tag-less / truncated packet
		...
		nonce = (kind == 2 && have_auth) ? last_nonce : (wm.top + (u64)(nondet_u32() % 64) - 16);
		...
		le32_store(pkt + 4, nondet_u32());
			...
			chacha20poly1305_encrypt(pkt + MD_HDR, NULL, 0, NULL, 0, nonce, key);
				...
				j = nondet_u8() % 16;
				pkt[MD_HDR + j] ^= (u8)(1 + nondet_u8() % 255);
			...
			nondet_bytes(pkt + MD_HDR, enc_len);
		...
		ok = chacha20poly1305_decrypt(pt_out, pkt + MD_HDR, enc_len, NULL, 0, nonce, key);
		...
		CHECK(ok == ref_ok);
			...
			CHECK(rc_same(&snap, &rc));            // bad tag / tag-less: counter untouched, nothing consumed
			...
			int r = wg_counter_validate(&rc, nonce);
			CHECK(r == pred);
				...
				CHECK(pt_len == 0);           // a keepalive delivers no plaintext
			...
			CHECK(rc.counter == wm.top);
...
}

The full spec at commit 3c1fc13 ↗

Law `transport_keepalive`: a keepalive is a data packet with a ZERO-length payload; it obeys the same
auth + counter rules as a normal data packet (authenticated, counter-validated), it delivers no plaintext, and
a truly empty / tag-less packet is handled without over-reading.

One receiving keypair and a sequence of ANY length of keepalive-shaped packets:
  - an authentic keepalive: the real chacha20poly1305_encrypt of the EMPTY plaintext under the key at a drawn
    nonce -> encrypted_data is exactly the 16-byte Poly1305 tag (total length = MESSAGE_MINIMUM_LENGTH);
  - that keepalive with its tag corrupted (bad tag);
  - a replay of an authentic keepalive's nonce;
  - a tag-less packet: encrypted_data of 0..15 bytes, with no room for a tag.
The harness runs receive.c's two stages (as transport_order), on an EXACT-size encrypted_data buffer.
Shadow model: ref_aead_decrypt over the empty payload for the tag; the window model for the counter.
CHECKs after every packet:
  - ok == (the reference tag verifies);  a tag-less packet (enc_len < 16) is rejected, ok == 0, never over-read;
  - BAD TAG / tag-less => the replay counter is byte-for-byte unchanged, nothing delivered;
  - authentic keepalive => reaches wg_counter_validate, verdict == the window model, counter advances to top,
    and on acceptance the delivered plaintext length is 0 (a keepalive carries no data);
  - an authentic keepalive follows exactly the same accept/replay rule as a full data packet (same window).

The code it is about#

__chacha20poly1305_decrypt in lib/crypto/chacha20poly1305.c, lines 126–168:

static bool
__chacha20poly1305_decrypt(u8 *dst, const u8 *src, const size_t src_len,
			   const u8 *ad, const size_t ad_len,
			   struct chacha_state *chacha_state)
{
	const u8 *pad0 = page_address(ZERO_PAGE(0));
	struct poly1305_desc_ctx poly1305_state;
	size_t dst_len;
	int ret;
	struct { /* QUICKPROOF P17: was a union of block0, mac (= block0[0..15]) and __le64 lens[2] (VST: typed memory) */
		u8 block0[POLY1305_KEY_SIZE];
	} b;

	if (unlikely(src_len < POLY1305_DIGEST_SIZE))
		return false;

	chacha20_crypt(chacha_state, b.block0, pad0, sizeof(b.block0));
	poly1305_init(&poly1305_state, b.block0);

	poly1305_update(&poly1305_state, ad, ad_len);
	if (ad_len & 0xf)
		poly1305_update(&poly1305_state, pad0, 0x10 - (ad_len & 0xf));

	dst_len = src_len - POLY1305_DIGEST_SIZE;
	poly1305_update(&poly1305_state, src, dst_len);
	if (dst_len & 0xf)
		poly1305_update(&poly1305_state, pad0, 0x10 - (dst_len & 0xf));

	/* QUICKPROOF P17: the two lengths as 16 little-endian bytes (were b.lens[0..1]) */
	put_unaligned_le64(ad_len, b.block0);
	put_unaligned_le64(dst_len, b.block0 + 8);
	poly1305_update(&poly1305_state, b.block0, 16);

	poly1305_final(&poly1305_state, b.block0); /* QUICKPROOF P17: b.mac was block0[0..15] */

	ret = crypto_memneq(b.block0, src + dst_len, POLY1305_DIGEST_SIZE);
	if (likely(!ret))
		chacha20_crypt(chacha_state, dst, src, dst_len);

	memzero_explicit(&b, sizeof(b));

	return !ret;
}

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

Theorem x_transport_keepalive : 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_transport_keepalive : harness_safe WgNoise.contracts.x_transport_keepalive.whole_prog.
Proof. exact (proj1 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (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.

Recorded for this property in DEVIATIONS.md (section L, what the properties exclude or assume):

• L15. The specs x_transport_order and x_transport_keepalive, and the admitted-packet half of x_transport_len, assume that receive.c runs the AEAD check and the replay counter in this order: decrypt_packet (in wg_packet_decrypt_worker) verifies the tag and marks the packet PACKET_STATE_CRYPTED or PACKET_STATE_DEAD without touching the counter; wg_packet_rx_poll calls counter_validate(&keypair->receiving_counter, nonce) only for a CRYPTED packet and delivers only an accepted one (wg_packet_consume_data_done). The specs compose the real functions of the two stages (the kernel's chacha20poly1305_decrypt, the contiguous-buffer form of what decrypt_packet runs through chacha20poly1305_decrypt_sg_inplace, and wg_counter_validate of S19) in that order and check the invariants: a bad tag leaves the replay counter unchanged byte for byte and delivers nothing; a good tag reaches the counter, whose verdict and new state agree with the window model; a keepalive delivers 0 bytes. The wiring itself is assumed: decrypt_packet, wg_packet_rx_poll and wg_packet_consume_data_done use sk_buff, scatterlists, skb_cow_data, NAPI, RCU and the per-peer queues, which are not modelled; likewise how the type word and the length reach validate_header_len (S24) Why: the pipeline cannot be extracted to Clight

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

How it was proved#

src/proof/harness/transport_keepalive/ holds 2,342 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 receive.c: see the list on the left, or the summary.