Browse zlib specs (11 of 62)

Proofs / zlib / Rejecting bad input

rj_bad_header

A zlib header that breaks RFC 1950 (check bits, method, window size) is refused before any output.

spec
45 lines of C
with its headers
85 lines
status
Proved
11 of 62
On this page

The spec

The spec is the C program harness/rj_bad_header.c, 45 lines, shown whole as it is in the repository at 37189f4. It includes harness/laws_common.h (40 lines). Its first comment states the property in full, with every bound.

C
// Law rj_bad_header: For any windowBits that selects the zlib wrapper (0, 8..15, or those plus 32, when the input does
// not start with the gzip magic 1f 8b) and any input (2 bytes to 2^32 - 1) whose first two bytes CMF and FLG break RFC
// 1950 2.2 (CMF*256 + FLG not a multiple of 31, or CM not 8, or CINFO above 7, or CINFO + 8 above windowBits when that
// is not 0 or 32), one inflate() call with any output space and any flush refuses it before any output: it returns
// Z_DATA_ERROR with total_out 0 and the output space unchanged.
#include "laws_common.h"

int main(void) {
	int window_bits = (int) upto(47);
	int low = window_bits & 15;
	gp_assume((window_bits & 16) == 0 && (low == 0 || low >= 8));
	size_t input_len = 2 + upto(UINT_MAX - 2);
	size_t room = nondet_u32();
	unsigned char *input = alloc_any_bytes(input_len);
	unsigned char *out = alloc_any_bytes(room);
	if (input == NULL || out == NULL)
		return 0;
	unsigned char *before = copy_of(out, room);
	if (before == NULL)
		return 0;
	// RFC 1950 2.2: "The FCHECK value must be such that CMF and FLG, when viewed as a 16-bit unsigned integer
	// stored in MSB order (CMF*256 + FLG), is a multiple of 31"; "CM = 8 denotes the "deflate" compression method";
	// "Values of CINFO above 7 are not allowed". zlib.h, inflateInit2: "If a compressed stream with a larger window
	// size is given as input, inflate() will return with the error code Z_DATA_ERROR"
	unsigned cmf = input[0];
	unsigned flg = input[1];
	unsigned cinfo = cmf >> 4;
	int bad_check = (cmf * 256 + flg) % 31 != 0;
	int bad_method = (cmf & 15) != 8;
	int bad_window = cinfo > 7 || (low != 0 && cinfo + 8 > (unsigned) low);
	gp_assume(bad_check || bad_method || bad_window);
	gp_assume(window_bits < 32 || cmf != 0x1f || flg != 0x8b);
	z_stream strm;
	new_stream(&strm);
	if (inflateInit2(&strm, window_bits) != Z_OK)
		return 0;
	set_buffer(&strm, input, input_len, out, room);

	int code = inflate(&strm, (int) nondet_u32());

	// RFC 1950 2.3: "A compliant decompressor must check CMF, FLG, and ADLER32, and provide an error indication if
	// any of these have incorrect values."
	gp_assert(code == Z_DATA_ERROR && strm.total_out == 0 && bytes_eq(out, before, room));
	return 0;
}
harness/laws_common.h, 40 lines
C
// laws_common.h: trivial helpers shared by the zlib laws (each law includes it once). No models, no algorithms.
#include <limits.h>
#include <stdlib.h>
#include "quickproof.h"
#include "zlib.h"
static size_t upto(size_t max) {
	size_t value = nondet_size();
	return value < max ? value : max;
}
static uInt clip(size_t n) { return n < UINT_MAX ? (uInt) n : UINT_MAX; }
static unsigned char *alloc_any_bytes(size_t n) {
	unsigned char *bytes = malloc(n);
	if (bytes != NULL)
		nondet_bytes(bytes, n);
	return bytes;
}
static unsigned char *copy_of(const unsigned char *source, size_t n) {
	unsigned char *copy = malloc(n);
	for (size_t i = 0; copy != NULL && i < n; i++)
		copy[i] = source[i];
	return copy;
}
static int bytes_eq(const unsigned char *a, const unsigned char *b, size_t n) {
	for (size_t i = 0; i < n; i++)
		if (a[i] != b[i])
			return 0;
	return 1;
}
static void set_buffer(z_stream *strm, unsigned char *in, size_t in_len, unsigned char *out, size_t out_len) {
	strm->next_in = in;
	strm->avail_in = (uInt) in_len;
	strm->next_out = out;
	strm->avail_out = (uInt) out_len;
}
static void new_stream(z_stream *strm) {
	strm->zalloc = Z_NULL;
	strm->zfree = Z_NULL;
	strm->opaque = Z_NULL;
	set_buffer(strm, Z_NULL, 0, Z_NULL, 0);
}

The theorem

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

Rocq
Theorem rj_bad_header : 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 rj_bad_header : harness_safe Zlib.contracts.rj_bad_header.whole_prog.
Proof. exact (proj1 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 Zlib.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
  • adler32.c
  • crc32.c
  • inflate.c
  • inffast.c
  • inftrees.c
  • zutil.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: 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 x86_64, LP64), one thread.
  • Where zlib reports Z_MEM_ERROR, most specs end the run and claim nothing about it; the first comment of the spec says so.
  • The edits to zlib's code, listed in the repository, are tested, 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.