Data packet lengths

The spec#

The property is stated by the C program harness/x_transport_len.c, 115 lines. Here is its main cut down to the inputs it draws, the calls into the code under test and the checks (lines 28–115; ... 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);
	nonce = draw_u64();
	...
	switch (nondet_u8() % 4) {
	case 0: tot = nondet_u8() % 40; break;                 // 0..39: straddles 4 and 32
	case 1: tot = 32 + nondet_u8() % 8; break;             // at / just above the minimum
	case 2: tot = nondet_u8() % 300; break;
	default: tot = draw_size(); break;
	...
	switch (nondet_u8() % 4) {
	...
	case 2: type = nondet_u32(); break;
	...
	nondet_bytes(pkt, tot);
	...
	hl = wg_validate_header_len(type, tot);
	...
	CHECK(hl == expect);
	...
	CHECK(enc_len >= 16);
		...
		chacha20poly1305_encrypt(pkt + MD_HDR, pt, pt_len, NULL, 0, nonce, key);
	...
	ok = chacha20poly1305_decrypt(pt_out, pkt + MD_HDR, enc_len, NULL, 0, nonce, key);
	...
	CHECK(ok == ref_ok);
		...
		CHECK(bytes_eq(pt_out, ref_pt, pt_len));   // plaintext == reference, exactly pt_len bytes
		...
		CHECK(ok);                                 // an authentic packet of this exact length decrypts
...
}

The full spec at commit 3c1fc13 ↗

Law `transport_len`: data-packet length / padding is validated before the payload is accessed; a
too-short or malformed-length data packet is rejected, not over-read.

A received packet of ANY total length `tot` (drawn around the 4-byte header and the 32-byte minimum, up to a few
hundred, and of any size; the run ends above PTRDIFF_MAX - 32, DEVIATIONS.md L13) and ANY type word, held in a
buffer of EXACTLY `tot` bytes (the quickproof convention: a one-byte overread is then caught by ASan / the
CompCert interpreter).  The harness runs the receive.c length
gate (validate_header_len, extracted in patch/data_header.c) and, when it admits a MESSAGE_DATA packet, the
payload read that decrypt_packet performs (the real chacha20poly1305_decrypt over exactly the encrypted_data
region [sizeof(message_data), tot)).
Shadow model: a MESSAGE_DATA packet is admitted exactly when tot >= MESSAGE_MINIMUM_LENGTH (= message_data_len(0)
  = sizeof(message_data) + 16); the encrypted_data region is then tot - sizeof(message_data) bytes (>= 16, room
  for the Poly1305 tag) and the plaintext is tot - sizeof(message_data) - 16 bytes.
CHECKs:
  - wg_validate_header_len == the model's header length (sizeof(message_data) for an admitted data packet, 0 for
    a short or non-data packet)  [the length gate];
  - an admitted data packet: the AEAD reads exactly [sizeof(message_data), tot) of the exact-size buffer and
    never past it (the exact buffer + ASan/interp are the overread oracle); its verdict and plaintext == the
    reference over the same region; the plaintext length is tot - sizeof(message_data) - 16;
  - a rejected packet (tot < MESSAGE_MINIMUM_LENGTH, or a non-data type): the payload is never accessed.

The code it is about#

wg_validate_header_len in patch/data_header.c, lines 24–41:

size_t wg_validate_header_len(u32 type, size_t len)
{
	if (unlikely(len < sizeof(struct message_header)))
		return 0;
	if (type == cpu_to_le32(MESSAGE_DATA) &&
	    len >= MESSAGE_MINIMUM_LENGTH)
		return sizeof(struct message_data);
	if (type == cpu_to_le32(MESSAGE_HANDSHAKE_INITIATION) &&
	    len == sizeof(struct message_handshake_initiation))
		return sizeof(struct message_handshake_initiation);
	if (type == cpu_to_le32(MESSAGE_HANDSHAKE_RESPONSE) &&
	    len == sizeof(struct message_handshake_response))
		return sizeof(struct message_handshake_response);
	if (type == cpu_to_le32(MESSAGE_HANDSHAKE_COOKIE) &&
	    len == sizeof(struct message_handshake_cookie))
		return sizeof(struct message_handshake_cookie);
	return 0;
}

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

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

• L13. The specs x_prim_blake2s, x_prim_poly1305 and x_prim_aead end the run when a drawn buffer length (message, associated data, the bytes given to decrypt) exceeds PTRDIFF_MAX (2^63 - 1), and so do x_transport_order (payload length above PTRDIFF_MAX - 32) and x_transport_len (packet length above PTRDIFF_MAX - 32). The lengths are otherwise unbounded. The ae_ specs draw their lengths up to PTRDIFF_MAX (PTRDIFF_MAX - 16 for a message that gets a 16-byte tag) Why: no C implementation creates an object larger than PTRDIFF_MAX (pointer differences inside it must fit ptrdiff_t; glibc's malloc returns NULL beyond it), but CompCert's memory model and VST's malloc_spec' allow objects of up to 2^64 - 1 bytes, which would make the specs cover buffers that cannot exist: blake2s_update's DIV_ROUND_UP(inlen, 64) wraps for inlen of 2^64 - 63 or more. This is an assumption about the environment, not about the code
• 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_len/ holds 1,540 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.