OpenSSL's punycode decoder

We proved 19 C specs of crypto/punycode.c in OpenSSL 3.6.5: the functions ossl_punycode_decode and ossl_a2ulabel, the code of CVE-2022-3602 and CVE-2022-3786. Each spec states a property, and each has a theorem in Rocq (formerly Coq). Sixteen are short specs; most of them use no model and compare OpenSSL with itself, with the RFC's own examples, or with simple facts about the input. Three compare both functions with a reference model written from the RFCs. AI agents wrote the proof, about 36,000 lines of Rocq, and Rocq checks it. The specs, the proof and every change to the code are in genproof/openssl-punycode-auto-proofs-public.

The code#

Domain names with non-ASCII letters travel in ASCII: each such label is written as xn-- followed by its Punycode form, so "bücher.example" becomes "xn--bcher-kva.example". RFC 3492 defines Punycode.

• ossl_punycode_decode(in, len, out, &n) decodes one Punycode string into an array of n code points. It returns 1 and sets n to the number of code points, or 0.
• ossl_a2ulabel(name, out, outlen) converts a whole host name: every label that starts with xn-- is decoded and written in UTF-8, every other label is copied, and a NUL ends the output. It returns 1, 0 (the output buffer is too small) or -1. OpenSSL uses it when it checks name constraints on internationalized e-mail addresses.

In CVE-2022-3602 ossl_punycode_decode wrote one code point past the end of its array, and in CVE-2022-3786 ossl_a2ulabel overflowed its output with the . between labels.

The specs#

Each spec links to its page, which shows the spec whole, as it is in the repository, with its theorem. Thirteen short specs are 77 to 98 lines with the 52-line shared header harness/laws_common.h, and three are 124 to 143 lines: the RFC's samples, a UTF-8 writer and an RFC 3492 encoder. In a spec, nondet_*, upto(max), any_bytes(n) and any_uints(n) stand for any value. Every buffer has exactly the size the spec gives it, so a single byte read or written past its end would break the theorem. The first comment of each file states the property in full; it starts with Law, the older word for a spec.

Any input#

Safe on any input, with only the documented results. 3 specs

• rj_decode_anyC file · 25 lines

  Any bytes of any length and any capacity: ossl_punycode_decode returns 1 (with a length at most the capacity) or 0 (length unchanged), as its documentation says, and leaves the input as it was.

• rj_decode_invalidC file · 34 lines

  Input with a byte that RFC 3492 6.2 says to fail on is refused (0, length unchanged): a non-ASCII byte before the last -, or a byte after it that is neither a letter nor a digit.

• rj_a2ulabel_anyC file · 29 lines

  Any string and any output size, NULL output included: ossl_a2ulabel returns 1, 0 or -1 (as documented; -1 for a NULL or empty output), writes only inside its buffer (CVE-2022-3786 overflowed it with the . between labels), leaves the string as it was and frees what it allocates.

The standard#

Decoding is RFC 3492's, and labels are converted as IDNA asks. 6 specs

• rfc_samplesC file · 79 lines

  The 19 sample strings of RFC 3492 7.1 decode to exactly the code points the RFC lists.

• rfc_basic_firstC file · 38 lines

  If any byte before the last - is 0x80 or above, decoding fails. On success, the code points below 0x80 are exactly the bytes before the last -, in order (RFC 3492 3.1, 6.2).

• rfc_digit_caseC file · 35 lines

  Changing the case of any letters among the deltas changes nothing: the same result, length and code points (RFC 3492 5: "A decoder MUST recognize the letters in both uppercase and lowercase forms").

• rfc_uniqueC file · 36 lines

  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").

• rfc_ace_any_caseC file · 39 lines

  ossl_a2ulabel converts a name that starts with xn--, Xn--, xN-- or XN-- the same way: the same result and the same buffer (RFC 3490 5: the ACE prefix is "xn--" or any capitalization thereof), when the allocation fails in neither call or in both.

• rfc_a2ulabel_utf8C file · 72 lines

  For s without . or NUL and an output of at least one byte: xn-- + s becomes exactly the UTF-8 form (RFC 3629) of the code points ossl_punycode_decode gives for s into 512 elements, and a NUL. The result is -1 when that decoding fails, when it gives a code point above U+10FFFF, or when the allocation fails; it is 0 when the output does not fit.

The interface#

Capacities, lengths, sizes and the NUL are exactly as documented. 6 specs

• api_decode_capacityC file · 42 lines

  Nothing is written past the reported length, the reported length is exactly the capacity needed, and one element fewer is refused (CVE-2022-3602 was a write one element past the end).

• api_decode_deterministicC file · 26 lines

  The result depends only on the bytes given: the same bytes elsewhere, followed by anything, decode the same way into two arrays of the same capacity.

• api_a2ulabel_copyC file · 36 lines

  With an output of at least one byte, a name with no label starting with xn-- (in any case) is copied as it is, with its NUL, when it fits ("If it does not start with xn--, it becomes U-label as is", crypto/punycode.c); else the result is 0. When the allocation fails, the result is -1.

• api_a2ulabel_nulC file · 28 lines

  On success (1) the output holds a NUL, and nothing after the first NUL was touched ("The output buffer is NUL-terminated").

• api_a2ulabel_sizeC file · 34 lines

  For a name that converts (1) into some buffer: any buffer of at least that output's size gives 1 and the same output, and any smaller buffer of at least one byte gives 0 (when the allocation fails in no call).

• api_a2ulabel_labelsC file · 46 lines

  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).

Round trip#

What an RFC 3492 encoder writes decodes back. 1 spec

• rt_roundtripC file · 91 lines

  Any number of any 32-bit code points, encoded by an RFC 3492 encoder written in the spec, when the encoder succeeds and the encoding is shorter than 2^32 - 1 bytes (OpenSSL's input limit): OpenSSL decodes them back whenever (largest code point - 127) × count ≤ 2^32. Beyond that bound it decodes them back or refuses them (0), never to other code points.

Earlier, longer properties#

These three specs, from our first proof of this code, compare both functions with a reference model written from the RFCs and OpenSSL's documentation (harness/puny_ref.h).

• x_decodeC file · 61 lines

  ossl_punycode_decode on any input and capacity gives exactly what the model's RFC 3492 decoder gives: the result, the length and the whole array.

• x_a2ulabelC file · 70 lines

  ossl_a2ulabel on any string and output size, out NULL or not, the allocation failing or not, gives exactly what the model's conversion gives: the result and the whole buffer.

• x_roundtripC file · 88 lines

  Up to 512 Unicode code points whose encoding by the model fits in 16 × count + 1 bytes: ossl_punycode_decode gives them back, and when no code point is . or NUL, ossl_a2ulabel gives their UTF-8 form.

Limits#

Each theorem says that for every value the spec draws, no run has undefined behaviour in CompCert's semantics of C and every check holds, so it also rules out any read or write outside an object. That reading rests on VST's adequacy theorem, which is not yet instantiated in Rocq for QuickProof's environment.

• Termination is not proved. A theorem says what holds if a call returns.
• The theorems are about the C code as CompCert defines it on x86_64 (LP64), in a release build (-DNDEBUG), compiled against a small header shim, in one thread. A binary built by GCC or Clang is outside them. Running out of stack is not covered.
• malloc may fail at any call. Each spec then either states the result (-1) or checks nothing more for that run.
• Only crypto/punycode.c, the ten functions of crypto/packet.c it reaches and the shim unit are verified. The certificate code that calls ossl_a2ulabel is not.
• IDNA validity is not checked: any xn-- label is decoded.
• When the output does not fit, the buffer of ossl_a2ulabel need not hold a prefix of the result and may have no NUL. Its only caller treats 0 as a failure.
• rt_roundtrip is bounded by a property of RFC 3492 itself. It states the round trip for every sequence of up to 3855 Unicode code points; beyond that, OpenSSL gives the code points back or refuses the string, never other code points.
• The theorems are about the code with the edits listed below. Nothing is proved about the unmodified file.
• Each theorem rests on 14 axioms: eight standard axioms of Rocq and six declarations of VST's malloc library. The result also trusts Rocq, VST, CompCert's semantics of C, clightgen, QuickProof's translation scripts and qp verify (What a proof means).

How to check it#

You need 64-bit x86 Linux with Coq 8.20.1, CompCert 3.15 and VST 2.15 (Install), or QuickProof's Docker image. Check the proof with a QuickProof checkout of your own at v0.1.0, the release the repository pins:

git clone --branch v0.1.0 https://github.com/genproof/quickproof-public.git quickproof
git clone --recursive https://github.com/genproof/openssl-punycode-auto-proofs-public.git
quickproof/tools/qp verify openssl-punycode-auto-proofs-public --base contract

The code under test#

The code is OpenSSL 3.6.5 (commit c8bd5a571085, tag openssl-3.6.5). crypto/punycode.c is identical in openssl-4.0.3 and in master of 2026-10-12. The repository's patch/PATCH.md lists every edit, and each changed line keeps the original in a comment. Two edits are for VST: two goto end become break, and a memmove over an unsigned int array becomes an element-by-element loop. A differential test checks that they change nothing. The third, D1, fixes a bug: ossl_a2ulabel decodes a label only when its ACE prefix is xn-- in lowercase, although RFC 3490 and RFC 5890 make the prefix case-insensitive. We reported it to the OpenSSL security team, which does not consider it a security issue; rfc_ace_any_case and x_a2ulabel need the fix. The edits are tested, not proved.

Maintained by Vladimir Kukharenko.