Browse OpenSSL punycode specs (7 of 19)

Proofs / OpenSSL punycode / The standard

rfc_unique

Two inputs that both decode (1) to the same code points, into arrays of the same capacity, are the same bytes up to the case of the delta letters (RFC 3492 6.2: "only one encoded string ... can represent a given sequence of integers").

spec
36 lines of C
with its headers
88 lines
status
Proved
7 of 19
On this page

The spec

The spec is the C program harness/rfc_unique.c, 36 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 rfc_unique: One sequence of code points has one Punycode form, up to the case of its digits. RFC 3492 6.2:
// "there is only one encoded string that can represent a given sequence of integers. ... If the decoder fails on
// these errors as shown above, then it cannot produce the same output for two distinct inputs." For any two inputs
// (any octets, any lengths the allocator provides) and any capacity (any unsigned int), each decoded into an array of
// exactly that many elements holding any values: when ossl_punycode_decode returns 1 for both, with the same code
// points, the inputs are the same octets, except that a letter of the deltas (after the last '-'; all octets when
// there is no '-') may be in the other case (rfc_digit_case).
#include "laws_common.h"

int main(void) {
	// Choose the inputs: any two octet strings, any capacity, any initial contents of the arrays
	size_t len1 = upto(PTRDIFF_MAX);
	unsigned char *input1 = any_bytes(len1);
	size_t len2 = upto(PTRDIFF_MAX);
	unsigned char *input2 = any_bytes(len2);
	unsigned int cap = nondet_u32();
	unsigned int *out1 = any_uints(cap);
	unsigned int *out2 = any_uints(cap);
	if (input1 == NULL || input2 == NULL || out1 == NULL || out2 == NULL)
		return 0;
	unsigned int count1 = cap, count2 = cap;
	int r1 = ossl_punycode_decode((const char *) input1, len1, out1, &count1);
	int r2 = ossl_punycode_decode((const char *) input2, len2, out2, &count2);
	if (r1 != 1 || r2 != 1 || count1 != count2 || !uints_eq(out1, out2, count1))
		return 0;
	// Check: the same octets, but for the case of letters among the deltas
	gp_assert(len1 == len2);
	size_t literal = last_delimiter(input1, len1);
	for (size_t i = 0; i < len1; i++)
		if (input1[i] != input2[i]) {
			unsigned char lower = input1[i] | 32;   // the letter in lowercase, if input1[i] is a letter
			gp_assert(i > literal || literal == 0);
			gp_assert(lower >= 'a' && lower <= 'z' && (input2[i] | 32) == lower);
		}
	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/rfc_unique.v:

Rocq
Theorem rfc_unique : 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 rfc_unique : harness_safe OpensslPunycode.contracts.rfc_unique.whole_prog.
Proof. exact (proj1 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (proj2 (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.