Browse WireGuard specs (16 of 38)

Proofs / WireGuard / Encryption and the primitives

ae_fail_untouched

A decryption that fails (either AEAD, any bytes as ciphertext) leaves every byte of its output buffer as it was.

spec
51 lines of C
with its headers
91 lines
status
Proved
16 of 38
On this page

The spec

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

C
// Law ae_fail_untouched: For any bytes as ciphertext (any length up to PTRDIFF_MAX), any associated data (up to
// PTRDIFF_MAX bytes), any nonce and any 32-byte key, a chacha20poly1305_decrypt or xchacha20poly1305_decrypt that
// returns false leaves every byte of its output buffer (an object of max(length - 16, 0) bytes) as it was.  The
// ciphertext is built as the encryption of any message under that associated data, nonce and key, then any bytes
// changed and any prefix kept: this reaches every byte string, and lets runs reach the tag check (a failed malloc
// ends the run).
#include "wg_laws.h"

int main(void) {
	// Choose the inputs: either AEAD, any message, associated data, nonce, key
	int extended = nondet_u8() & 1;
	size_t len = upto(PTRDIFF_MAX - CHACHA20POLY1305_AUTHTAG_SIZE);
	size_t ad_len = upto(PTRDIFF_MAX);
	u8 *message = any_bytes(len);
	u8 *ad = any_bytes(ad_len);
	u8 *sealed = malloc(len + CHACHA20POLY1305_AUTHTAG_SIZE);
	if (message == NULL || ad == NULL || sealed == NULL)
		return 0;
	u8 key[CHACHA20POLY1305_KEY_SIZE], xnonce[XCHACHA20POLY1305_NONCE_SIZE];
	nondet_bytes(key, sizeof key);
	nondet_bytes(xnonce, sizeof xnonce);
	u64 nonce = any_u64();
	if (extended)
		xchacha20poly1305_encrypt(sealed, message, len, ad, ad_len, xnonce, key);
	else
		chacha20poly1305_encrypt(sealed, message, len, ad, ad_len, nonce, key);
	// Any bytes changed to any values, then any prefix of it, as an object of its own
	while (nondet_u8() != 0)
		sealed[upto(len + CHACHA20POLY1305_AUTHTAG_SIZE - 1)] = nondet_u8();
	size_t given = upto(len + CHACHA20POLY1305_AUTHTAG_SIZE);
	size_t out_len = given < CHACHA20POLY1305_AUTHTAG_SIZE ? 0 : given - CHACHA20POLY1305_AUTHTAG_SIZE;
	u8 *ciphertext = copy_of(sealed, given);
	u8 *out = any_bytes(out_len);
	if (ciphertext == NULL || out == NULL)
		return 0;
	u8 *before = copy_of(out, out_len);
	if (before == NULL)
		return 0;
	// Decrypt. RFC 8439, 2.8: "The message is authenticated if and only if the tags match."; lib/crypto/
	// chacha20poly1305.c: "ret = crypto_memneq(b.block0, src + dst_len, POLY1305_DIGEST_SIZE); if (likely(!ret))
	// chacha20_crypt(chacha_state, dst, src, dst_len);"
	bool ok;
	if (extended)
		ok = xchacha20poly1305_decrypt(out, ciphertext, given, ad, ad_len, xnonce, key);
	else
		ok = chacha20poly1305_decrypt(out, ciphertext, given, ad, ad_len, nonce, key);
	// Check
	if (ok == 0)
		gp_assert(bytes_eq(out, before, out_len));
	return 0;
}
harness/wg_laws.h, 40 lines
C
// wg_laws.h: trivial helpers shared by the WireGuard laws (each law includes it once). No models, no algorithms.
#include "quickproof.h"
#include "noise.h"
#include <crypto/blake2s.h>
#include <crypto/chacha.h>
#include <crypto/poly1305.h>
#include <crypto/chacha20poly1305.h>
bool wg_counter_validate(struct noise_replay_counter *counter, u64 nonce);   // receive.c's counter_validate (S19)
#define REJECT_AFTER (U64_MAX - COUNTER_WINDOW_SIZE - 1)   // messages.h: REJECT_AFTER_MESSAGES, 2^64 - 8130
static size_t upto(size_t max) {                      // any value from 0 to max
	size_t value = nondet_size();
	return value < max ? value : max;
}
static u64 any_u64(void) {                            // any 64-bit value
	u64 high = nondet_u32();
	return high << 32 | nondet_u32();
}
static u8 *any_bytes(size_t n) {                      // a new object of n arbitrary bytes (NULL if malloc fails)
	u8 *bytes = malloc(n);
	if (bytes != NULL && n != 0)
		nondet_bytes(bytes, n);
	return bytes;
}
static u8 *copy_of(const u8 *source, size_t n) {      // a new object holding source[0..n-1]
	u8 *copy = malloc(n);
	for (size_t i = 0; copy != NULL && i < n; i++)
		copy[i] = source[i];
	return copy;
}
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 new_counter(struct noise_replay_counter *c) {    // a new key's replay counter: zero (keypair_create)
	c->counter = 0;
	for (size_t i = 0; i < COUNTER_BITS_TOTAL / BITS_PER_LONG; i++)
		c->backtrack[i] = 0;
}

The theorem

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

Rocq
Theorem ae_fail_untouched : 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 ae_fail_untouched : harness_safe WgNoise.contracts.ae_fail_untouched.whole_prog.
Proof. exact (proj1 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
  • lib/crypto/chacha.c
  • lib/crypto/chacha-block-generic.c
  • lib/crypto/poly1305.c
  • lib/crypto/poly1305-donna32.c
  • lib/crypto/chacha20poly1305.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.