Browse OpenSSL punycode specs (15 of 19)

Proofs / OpenSSL punycode / The interface

api_a2ulabel_labels

Labels are converted one by one. When s1 and s2 each convert (1), the name s1.s2 converts, into a buffer as large as their two buffers together, to the output of s1, a ., and the output of s2. When either gives -1, so does the name (when the allocation fails in no call).

spec
46 lines of C
with its headers
98 lines
status
Proved
15 of 19
On this page

The spec

The spec is the C program harness/api_a2ulabel_labels.c, 46 lines, shown whole as it is in the repository at 7556530. It includes harness/laws_common.h (52 lines). Its first comment states the property in full, with every bound.

C
// Law api_a2ulabel_labels: The labels of a name are converted one by one. For any two strings s1 and s2 (any octets
// up to their NUL, any lengths the allocator provides) and any outlen1, outlen2 >= 1, with objects of exactly those
// sizes holding any values: if ossl_a2ulabel returns 1 for s1 into outlen1 octets and 1 for s2 into outlen2 octets, it
// returns 1 for s1 '.' s2 into outlen1 + outlen2 octets and writes the output of s1, a '.', and the output of s2 with
// its NUL; if it returns -1 for s1 or for s2, it returns -1 for s1 '.' s2 (when the allocation of its WPACKET record
// fails in none of the three calls).
#include "laws_common.h"

int main(void) {
	// Choose the inputs: any two strings, the name s1 '.' s2, any outlen1 and outlen2 >= 1 and as many octets
	size_t len1 = upto(PTRDIFF_MAX - 2), len2 = upto(PTRDIFF_MAX - 2 - len1);
	unsigned char *s1 = any_bytes(len1 + 1), *s2 = any_bytes(len2 + 1), *name = malloc(len1 + len2 + 2);
	size_t outlen1 = upto(PTRDIFF_MAX), outlen2 = upto(PTRDIFF_MAX - outlen1);
	unsigned char *out1 = any_bytes(outlen1), *out2 = any_bytes(outlen2), *out = any_bytes(outlen1 + outlen2);
	if (s1 == NULL || s2 == NULL || name == NULL || out1 == NULL || out2 == NULL || out == NULL)
		return 0;
	if (outlen1 == 0 || outlen2 == 0)
		return 0;
	s1[len1] = 0;
	s2[len2] = 0;
	size_t n1 = 0, n2 = 0;                              // the strings' lengths
	for (; s1[n1] != 0; n1++)
		name[n1] = s1[n1];
	name[n1] = '.';
	for (; s2[n2] != 0; n2++)
		name[n1 + 1 + n2] = s2[n2];
	name[n1 + 1 + n2] = 0;
	ossl_shim_zalloc_failed = 0;
	int r1 = ossl_a2ulabel((const char *) s1, (char *) out1, outlen1);
	int r2 = ossl_a2ulabel((const char *) s2, (char *) out2, outlen2);
	int r = ossl_a2ulabel((const char *) name, (char *) out, outlen1 + outlen2);
	if (ossl_shim_zalloc_failed)
		return 0;
	// Check. crypto/punycode.c: "Domain name has some parts consisting of ASCII chars joined with dot."
	if (r1 == -1 || r2 == -1)
		gp_assert(r == -1);
	if (r1 == 1 && r2 == 1) {
		size_t u1 = 0, u2 = 0;                          // the lengths of the two outputs
		while (u1 < outlen1 && out1[u1] != 0)
			u1++;
		while (u2 < outlen2 && out2[u2] != 0)
			u2++;
		gp_assert(r == 1 && bytes_eq(out, out1, u1) && out[u1] == '.' && bytes_eq(out + u1 + 1, out2, u2 + 1));
	}
	return 0;
}
harness/laws_common.h, 52 lines
C
// laws_common.h: trivial helpers shared by the short laws (each law includes it once). No models, no algorithms.
#include <stdint.h>
#include <stdlib.h>
#include "quickproof.h"
#include "crypto/punycode.h"                         // ossl_punycode_decode, ossl_a2ulabel
// OpenSSL's allocator in this build (patch/shim/ossl_shim.c): set to 1 when CRYPTO_zalloc fails (malloc may fail at
// any call in the theorems), and the number of its blocks not freed yet.
extern int ossl_shim_zalloc_failed;
extern long ossl_shim_live;
static size_t upto(size_t max) {                     // any value from 0 to max
	size_t value = nondet_size();
	return value < max ? value : max;
}
static unsigned char *any_bytes(size_t n) {          // a new object of n arbitrary bytes (NULL if malloc fails)
	unsigned char *bytes = malloc(n);
	if (bytes != NULL)
		nondet_bytes(bytes, n);
	return bytes;
}
static unsigned int *any_uints(size_t n) {           // a new array of n arbitrary unsigned ints (NULL if malloc fails)
	unsigned int *values = malloc(n * sizeof(unsigned int));
	for (size_t i = 0; values != NULL && i < n; i++)
		values[i] = nondet_u32();
	return values;
}
static unsigned char *copy_of(const unsigned char *source, size_t n) {   // a new object holding source[0..n-1]
	if (source == NULL)                                                   // (NULL if source is or malloc fails)
		return NULL;
	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) {   // 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 int uints_eq(const unsigned int *a, const unsigned int *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 size_t last_delimiter(const unsigned char *s, size_t n) {   // the position of the last '-', 0 if none
	size_t last = 0;
	for (size_t i = 0; i < n; i++)
		if (s[i] == '-')
			last = i;
	return last;
}

The theorem

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

Rocq
Theorem api_a2ulabel_labels : 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 api_a2ulabel_labels : harness_safe OpensslPunycode.contracts.api_a2ulabel_labels.whole_prog.
Proof. exact (proj1 (proj2 OpensslPunycode.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
  • crypto/punycode.c
  • patch/units/packet_ext.c
  • patch/shim/ossl_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: termination (a run that never returns is not a counterexample), one thread, and binaries built by a compiler (the theorem is about the code as CompCert defines C for x86-64, in a release build, compiled against a small header shim instead of OpenSSL's generated headers).
  • The rest of OpenSSL: only crypto/punycode.c and the parts of crypto/packet.c it reaches are code under test.

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.