Browse zlib specs (51 of 62)

Proofs / zlib / Earlier, longer properties

x_inflate_header

inflateGetHeader with buffers of any size up to 64 KiB, on a gzip member with any header fields: inflate writes the buffers only within their sizes, reports every field once the header is complete, and never accepts a reserved flag bit or a wrong header CRC.

spec
229 lines of C
with its headers
384 lines
status
Proved
51 of 62
On this page

The spec

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

C
// Law inflate_header: inflateGetHeader and the gzip header (RFC 1952 2.3).  inflateInit2 with ANY windowBits, then
// inflateGetHeader with a gz_header whose extra, name and comment buffers are each Z_NULL or an object of exactly
// extra_max, name_max, comm_max bytes, ANY maxima (<= 2^16), holding anything.  The input is a gzip member built
// here from ANY header fields: ANY FLG byte (FTEXT, FHCRC, FEXTRA, FNAME, FCOMMENT and the reserved bits), ANY MTIME,
// XFL, OS, an extra field of ANY XLEN <= 65535 bytes of ANY contents, a file name and a comment of ANY length
// <= 2^16 of ANY non-zero bytes (each ended by a zero byte), the header CRC (the low 16 bits of the CRC-32 of the
// header before it) or ANY wrong value; then an empty final stored block and the gzip trailer of the empty data.
// It is inflated by ANY number of calls with ANY flush value, ANY split of the input and ANY output space (each call:
// objects of exactly avail_in and avail_out bytes).  Properties:
//  - inflateGetHeader returns Z_STREAM_ERROR exactly when windowBits allows no gzip wrapper (< 16), else Z_OK;
//  - no undefined behaviour: in particular inflate writes the header buffers only within their maxima (each buffer is
//    an object of exactly its maximum; no slack);
//  - a header with a reserved flag bit set, or a wrong header CRC (FHCRC), is never accepted: no Z_STREAM_END, and
//    on Z_DATA_ERROR for a reserved bit done is still 0; a valid member never gives Z_DATA_ERROR;
//  - once done is 1 (the header is complete): text, time, xflags, os and hcrc are the header's FTEXT, MTIME, XFL, OS
//    and FHCRC; with FEXTRA extra_len is XLEN and the extra buffer holds the first min(XLEN, extra_max) bytes of the
//    field, without it head->extra is Z_NULL; with FNAME the name buffer holds the first min(length + 1,
//    name_max) bytes of the name and its zero byte, without it head->name is Z_NULL; the same for the comment;
//    the rest of each buffer is unchanged;
//  - on Z_STREAM_END: done is 1, the whole member was consumed and nothing was produced.
// Bounds: XLEN <= 65535, name and comment <= 2^16 bytes, buffer maxima <= 2^16, at most 2^20 bytes of output space
// per call, any number of calls.
#include "zlib_common.h"

#define GP_STR_MAX (1u << 16)
#define GP_BUF_MAX (1u << 16)
#define GP_OUT_MAX (1u << 20)

// buf[0..n-1] := any non-zero bytes
static void draw_nonzero(unsigned char *buf, unsigned n)
{
	nondet_bytes(buf, n);
	for (unsigned i = 0; i < n; ++i)
		gp_assume(buf[i] != 0);
}

// a header buffer: Z_NULL (when nul == 0) or exactly max bytes with any contents, and a snapshot
static unsigned char *head_buf(unsigned max, unsigned char nul, unsigned char **snap)
{
	if (nul == 0) {
		*snap = Z_NULL;
		return Z_NULL;
	}
	return exact_space(max, snap);
}

// field f (the header's bytes, len of them) as a header buffer of maximum max should hold it; the rest unchanged
static int field_ok(const unsigned char *buf, const unsigned char *snap, unsigned max, const unsigned char *f,
		    unsigned len)
{
	unsigned k = len < max ? len : max;
	return bytes_same(buf, f, k) && bytes_same(buf + k, snap + k, max - k);
}

int main(void)
{
	const int wbits = (int) nondet_u32();
	const unsigned char flg = nondet_u8();
	const unsigned long mtime = nondet_u32();
	const unsigned char xfl = nondet_u8();
	const unsigned char os = nondet_u8();
	const unsigned xlen = nondet_u32();
	const unsigned nl = nondet_u32();
	const unsigned cl = nondet_u32();
	const unsigned delta = nondet_u32();
	const unsigned xmax = nondet_u32();
	const unsigned nmax = nondet_u32();
	const unsigned cmax = nondet_u32();
	const unsigned char xnul = nondet_u8();
	const unsigned char nnul = nondet_u8();
	const unsigned char cnul = nondet_u8();
	gp_assume(xlen <= 65535 && nl <= GP_STR_MAX && cl <= GP_STR_MAX);
	gp_assume(xmax <= GP_BUF_MAX && nmax <= GP_BUF_MAX && cmax <= GP_BUF_MAX);
	// the member: header, empty final stored block (01 00 00 ff ff), CRC-32 and ISIZE of the empty data (0, 0)
	const unsigned hlen = 10 + ((flg & 4) ? 2 + xlen : 0) + ((flg & 8) ? nl + 1 : 0) + ((flg & 16) ? cl + 1 : 0);
	const unsigned total = hlen + ((flg & 2) ? 2 : 0) + 5 + 8;
	unsigned char *src = malloc(total);
	unsigned char *xf = malloc(xlen);           // the fields, as the header buffers should hold them
	unsigned char *nf = malloc(nl + 1);
	unsigned char *cf = malloc(cl + 1);
	if (src == NULL || xf == NULL || nf == NULL || cf == NULL)
		return 0;
	nondet_bytes(xf, xlen);
	draw_nonzero(nf, nl);
	nf[nl] = 0;
	draw_nonzero(cf, cl);
	cf[cl] = 0;
	src[0] = 0x1f;
	src[1] = 0x8b;
	src[2] = 8;
	src[3] = flg;
	src[4] = (unsigned char) mtime;
	src[5] = (unsigned char) (mtime >> 8);
	src[6] = (unsigned char) (mtime >> 16);
	src[7] = (unsigned char) (mtime >> 24);
	src[8] = xfl;
	src[9] = os;
	unsigned k = 10;
	if (flg & 4) {
		src[k] = (unsigned char) xlen;
		src[k + 1] = (unsigned char) (xlen >> 8);
		bytes_copy(src + k + 2, xf, xlen);
		k += 2 + xlen;
	}
	if (flg & 8) {
		bytes_copy(src + k, nf, nl + 1);
		k += nl + 1;
	}
	if (flg & 16) {
		bytes_copy(src + k, cf, cl + 1);
		k += cl + 1;
	}
	const unsigned long hcrc = ref_crc32(0, src, hlen) & 0xffff;
	if (flg & 2) {
		const unsigned long stored = (hcrc ^ delta) & 0xffff;
		src[k] = (unsigned char) stored;
		src[k + 1] = (unsigned char) (stored >> 8);
		k += 2;
	}
	src[k] = 1;
	src[k + 1] = 0;
	src[k + 2] = 0;
	src[k + 3] = 0xff;
	src[k + 4] = 0xff;
	for (unsigned i = 0; i < 8; ++i)
		src[k + 5 + i] = 0;
	const int reserved = (flg & 0xe0) != 0;
	const int badcrc = (flg & 2) && (delta & 0xffff) != 0;

	z_stream s;
	stream_defaults(&s);
	int r = inflateInit2(&s, wbits);
	if (r != Z_OK)
		return 0;
	gz_header h;
	unsigned char *xs, *ns, *cs;
	h.extra = head_buf(xmax, xnul, &xs);
	h.name = head_buf(nmax, nnul, &ns);
	h.comment = head_buf(cmax, cnul, &cs);
	if ((xnul != 0 && h.extra == Z_NULL) || (nnul != 0 && h.name == Z_NULL) || (cnul != 0 && h.comment == Z_NULL))
		return 0;
	h.extra_max = xmax;
	h.name_max = nmax;
	h.comm_max = cmax;
	pick(h.text);
	pick(h.time);
	pick(h.xflags);
	pick(h.os);
	pick(h.extra_len);
	pick(h.hcrc);
	pick(h.done);
	r = inflateGetHeader(&s, &h);
	gp_assert((r == Z_STREAM_ERROR) == (wbits < 16));
	if (r != Z_OK) {
		gp_assert(r == Z_STREAM_ERROR);
		inflateEnd(&s);
		return 0;
	}
	gp_assert(h.done == 0);
	unsigned pos = 0;
	for (;;) {
		const unsigned nlim = nondet_u32();
		const unsigned aout = nondet_u32();
		const int flush = (int) nondet_u32();
		const unsigned char stop = nondet_u8();
		gp_assume(pos <= nlim && nlim <= total);
		gp_assume(aout <= GP_OUT_MAX);
		const unsigned ain = nlim - pos;
		unsigned char *ib = exact_copy(src + pos, ain);
		unsigned char *osnap;
		unsigned char *ob = exact_space(aout, &osnap);
		if (ib == NULL || ob == NULL)
			return 0;
		s.next_in = ib;
		s.avail_in = ain;
		s.next_out = ob;
		s.avail_out = aout;
		r = inflate(&s, flush);
		if (r == Z_MEM_ERROR)
			return 0;
		gp_assert(r == Z_OK || r == Z_BUF_ERROR || r == Z_STREAM_END || r == Z_DATA_ERROR);
		pos += ain - s.avail_in;
		if (reserved || badcrc)
			gp_assert(r != Z_STREAM_END);
		else
			gp_assert(r != Z_DATA_ERROR);
		if (reserved && r == Z_DATA_ERROR)
			gp_assert(h.done == 0);
		if (h.done != 0) {
			gp_assert(h.done == 1);
			gp_assert(h.text == (flg & 1));
			gp_assert(h.time == mtime);
			gp_assert(h.xflags == xfl);
			gp_assert(h.os == os);
			gp_assert(h.hcrc == ((flg >> 1) & 1));
			if (flg & 4) {
				gp_assert(h.extra_len == xlen);
				if (xnul != 0)
					gp_assert(field_ok(h.extra, xs, xmax, xf, xlen));
			} else {
				gp_assert(h.extra == Z_NULL);
			}
			if (flg & 8) {
				if (nnul != 0)
					gp_assert(field_ok(h.name, ns, nmax, nf, nl + 1));
			} else {
				gp_assert(h.name == Z_NULL);
			}
			if (flg & 16) {
				if (cnul != 0)
					gp_assert(field_ok(h.comment, cs, cmax, cf, cl + 1));
			} else {
				gp_assert(h.comment == Z_NULL);
			}
		}
		if (r == Z_STREAM_END) {
			gp_assert(h.done == 1);
			gp_assert(pos == total);
			gp_assert(s.total_out == 0);
		}
		free(ib);
		free(ob);
		free(osnap);
		if (stop == 0)
			break;
	}
	inflateEnd(&s);
	return 0;
}
harness/zlib_common.h, 155 lines
C
// Shared by the zlib harnesses (zlib 1.3.2 core: adler32.c, crc32.c, deflate.c, trees.c, inflate.c, inffast.c,
// inftrees.c, compress.c, uncompr.c, zutil.c).
//
// A harness draws every input from quickproof.h (nondet_*, pick), restricts it with gp_assume, and states each property
// with gp_assert (undefined behaviour when the property fails).  Buffers have exactly the size the claim allows.  Every
// call of inflate() or deflate() gets its input and its output space as objects of their own, allocated with exactly
// avail_in and avail_out bytes (exact_copy, exact_space): an access before next_in, after next_in + avail_in, before
// next_out or after next_out + avail_out is then outside an object, i.e. undefined behaviour in the semantics of the
// theorem, so "inflate reads only the input it is offered and writes only the space it is offered" is part of every
// law's "no undefined behaviour".
//
// The reference facts, written from the definitions, not from zlib:
//  - Adler-32 (RFC 1950 8.2): s1 = 1 + the sum of the bytes, s2 = the sum of the successive values of s1, both mod
//    65521; the checksum is s2 * 65536 + s1.  ref_adler32 updates a checksum byte by byte;
//  - CRC-32 (RFC 1952 8, ISO 3309): the reflected polynomial 0xedb88320, register preset to all ones and inverted at
//    the end.  ref_crc32 updates a checksum bit by bit;
//  - the zlib wrapper (RFC 1950): 2 header bytes, an optional 4-byte dictionary id (big-endian Adler-32 of the
//    dictionary), the deflate data, then the big-endian Adler-32 of the uncompressed data;
//  - the gzip wrapper (RFC 1952): a header of at least 10 bytes (1f 8b 08 FLG MTIME(4) XFL OS, then the optional
//    fields), the deflate data, then the little-endian CRC-32 and the little-endian length mod 2^32 of the data;
//  - the inflate windowBits of zlib.h: 8..15 (zlib wrapper, 2^windowBits window), 0 (zlib wrapper, the window size of
//    the header), -8..-15 (raw deflate), + 16 (gzip wrapper only; 16 itself: the window size of the header), + 32
//    (zlib or gzip, detected); everything else is rejected with Z_STREAM_ERROR.
#ifndef ZLIB_HARNESS_COMMON_H
#define ZLIB_HARNESS_COMMON_H
#include <stddef.h>
#include <stdint.h>
#include <stdlib.h>
#include "quickproof.h"
#include "zlib.h"

#define GP_BASE 65521ul             // the Adler-32 modulus (RFC 1950)
#define GP_POLY 0xedb88320ul        // the CRC-32 polynomial, reflected (RFC 1952)

// Adler-32 of buf[0..n-1] continued from the checksum a (both halves < 65521 for a checksum).
static unsigned long ref_adler32(unsigned long a, const unsigned char *buf, unsigned long n)
{
	unsigned long s1 = a & 0xffff;
	unsigned long s2 = (a >> 16) & 0xffff;
	for (unsigned long i = 0; i < n; ++i) {
		s1 = (s1 + buf[i]) % GP_BASE;
		s2 = (s2 + s1) % GP_BASE;
	}
	return (s2 << 16) | s1;
}

// The CRC-32 register update by one byte, without pre- or post-conditioning (the register is the 32 low bits).
static unsigned long ref_crc_byte(unsigned long c, unsigned char b)
{
	c ^= b;
	for (int k = 0; k < 8; ++k) {
		if (c & 1)
			c = (c >> 1) ^ GP_POLY;
		else
			c = c >> 1;
	}
	return c;
}

// CRC-32 of buf[0..n-1] continued from the checksum c (its 32 low bits).
static unsigned long ref_crc32(unsigned long c, const unsigned char *buf, unsigned long n)
{
	c = (~c) & 0xffffffff;
	for (unsigned long i = 0; i < n; ++i)
		c = ref_crc_byte(c, buf[i]);
	return (~c) & 0xffffffff;
}

static unsigned long be32(const unsigned char *p)
{
	return ((unsigned long) p[0] << 24) | ((unsigned long) p[1] << 16) | ((unsigned long) p[2] << 8) | p[3];
}

static unsigned long le32(const unsigned char *p)
{
	return ((unsigned long) p[3] << 24) | ((unsigned long) p[2] << 16) | ((unsigned long) p[1] << 8) | p[0];
}

static int bytes_same(const unsigned char *a, const unsigned char *b, unsigned long n)
{
	for (unsigned long i = 0; i < n; ++i)
		if (a[i] != b[i])
			return 0;
	return 1;
}

static void bytes_copy(unsigned char *d, const unsigned char *s, unsigned long n)
{
	for (unsigned long i = 0; i < n; ++i)
		d[i] = s[i];
}

// A new object of exactly n bytes holding src[0..n-1] (NULL when the allocation fails).
static unsigned char *exact_copy(const unsigned char *src, unsigned n)
{
	unsigned char *p = malloc(n);
	if (p != NULL)
		bytes_copy(p, src, n);
	return p;
}

// A new object of exactly n bytes with any contents, and a snapshot of them in *snap (NULL when an allocation fails).
static unsigned char *exact_space(unsigned n, unsigned char **snap)
{
	unsigned char *p = malloc(n);
	unsigned char *q = malloc(n);
	if (p == NULL || q == NULL) {
		free(p);
		free(q);
		*snap = NULL;
		return NULL;
	}
	nondet_bytes(p, n);
	bytes_copy(q, p, n);
	*snap = q;
	return p;
}

// inflateInit2's windowBits check (zlib.h): accepted values.
static int inflate_wbits_ok(int w)
{
	if (w < 0)
		return w >= -15 && w <= -8;
	if (w >= 48)
		return 0;
	w &= 15;
	return w == 0 || (w >= 8 && w <= 15);
}

// Is a value one of inflate()'s documented return codes (zlib.h)?
static int inflate_code_ok(int r)
{
	return r == Z_OK || r == Z_STREAM_END || r == Z_NEED_DICT || r == Z_DATA_ERROR || r == Z_STREAM_ERROR ||
	       r == Z_MEM_ERROR || r == Z_BUF_ERROR;
}

// A z_stream with the default allocator (zalloc, zfree, opaque all Z_NULL: zlib uses zcalloc/zcfree, i.e. malloc and
// free) and any values in the fields the caller does not have to set.
static void stream_defaults(z_stream *s)
{
	s->zalloc = Z_NULL;
	s->zfree = Z_NULL;
	s->opaque = Z_NULL;
	s->next_in = Z_NULL;
	s->avail_in = 0;
	s->next_out = Z_NULL;
	s->avail_out = 0;
	pick(s->total_in);
	pick(s->total_out);
	pick(s->adler);
	pick(s->data_type);
	pick(s->reserved);
}

#endif

The theorem

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

Rocq
Theorem x_inflate_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 x_inflate_header : harness_safe Zlib.contracts.x_inflate_header.whole_prog.
Proof. exact (proj1 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 Zlib.contracts.suite.suite_x))))))))))))))). 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.