Browse zlib specs (13 of 62)

Proofs / zlib / Rejecting bad input

rj_bad_checksum

If the checksum or length at the end of the stream is changed, decompression never reports success.

spec
79 lines of C
with its headers
119 lines
status
Proved
13 of 62
On this page

The spec

The spec is the C program harness/rj_bad_checksum.c, 79 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_checksum: For any data (any length the allocator provides) compressed with deflateInit2 (any level,
// windowBits, memLevel and strategy it accepts with the zlib or gzip wrapper) and deflate (all of it, in pieces of at
// most 2^32 - 1 bytes, Z_FINISH with the last, into deflateBound_z bytes; the run ends unless it reaches Z_STREAM_END),
// with its trailer then changed in any way (zlib: the Adler-32, the last 4 bytes; gzip: the CRC-32 and ISIZE, the last
// 8), inflate() fed all of it and room for the data, in pieces of at most 2^32 - 1 bytes, with any flush, returns Z_OK
// or Z_BUF_ERROR until it returns Z_DATA_ERROR, never Z_STREAM_END (Z_MEM_ERROR ends the run).
#include "laws_common.h"

int main(void) {
	size_t data_len = upto(PTRDIFF_MAX);
	unsigned char *data = alloc_any_bytes(data_len);
	unsigned char *out = malloc(data_len);
	if (data == NULL || out == NULL)
		return 0;
	int level = (int) nondet_u32();
	int window_bits = (int) nondet_u32();
	int mem_level = (int) nondet_u32();
	int strategy = (int) nondet_u32();
	unsigned char *change = alloc_any_bytes(8);
	if (change == NULL || window_bits < 8)
		return 0;
	z_stream compressor;
	new_stream(&compressor);
	if (deflateInit2(&compressor, level, Z_DEFLATED, window_bits, mem_level, strategy) != Z_OK)
		return 0;
	size_t out_size = deflateBound_z(&compressor, data_len);
	unsigned char *compressed = malloc(out_size);
	if (compressed == NULL)
		return 0;
	compressor.next_in = data;
	compressor.next_out = compressed;
	int code;
	do {
		size_t rest = data_len - (size_t) (compressor.next_in - data);
		int flush = Z_NO_FLUSH;
		if (rest <= UINT_MAX)
			flush = Z_FINISH;
		compressor.avail_in = clip(rest);
		compressor.avail_out = clip(out_size - (size_t) (compressor.next_out - compressed));

		code = deflate(&compressor, flush);
	} while (code == Z_OK);
	if (code != Z_STREAM_END)
		return 0;
	size_t compressed_len = (size_t) (compressor.next_out - compressed);
	// RFC 1950 2.2: ADLER32 is the last 4 bytes; RFC 1952 2.3: CRC32 and ISIZE, the last 8
	size_t trailer_len = 4;
	if (window_bits > 15)
		trailer_len = 8;
	int changed = 0;
	for (size_t i = 0; i < trailer_len; i++) {
		compressed[compressed_len - trailer_len + i] ^= change[i];
		changed |= change[i];
	}
	gp_assume(changed != 0);
	z_stream decompressor;
	new_stream(&decompressor);
	// zlib.h, deflateInit2: "a request for 8 will result in 9"; "use 9 with inflateInit2()"
	if (window_bits == 8)
		window_bits = 9;
	if (inflateInit2(&decompressor, window_bits) != Z_OK)
		return 0;
	decompressor.next_in = compressed;
	decompressor.next_out = out;
	do {
		decompressor.avail_in = clip(compressed_len - (size_t) (decompressor.next_in - compressed));
		decompressor.avail_out = clip(data_len - (size_t) (decompressor.next_out - out));

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

		if (code == Z_MEM_ERROR)
			return 0;
		// 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." zlib.h, inflate: "The CRC-32 is checked against
		// the gzip trailer, as is the uncompressed length, modulo 2^32."
		gp_assert(code == Z_OK || code == Z_BUF_ERROR || code == Z_DATA_ERROR);
	} while (code != Z_DATA_ERROR);
	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_checksum.v:

Rocq
Theorem rj_bad_checksum : 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_checksum : harness_safe Zlib.contracts.rj_bad_checksum.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 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
  • deflate.c
  • trees.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.