Sixteen XORs and not a single if

Verbose is a small experimental language I build — its compiler proves properties about your code (termination, declared reads, sound types) and emits tiny x86-64 machine code: no runtime, no GC, no libc. Its emitted binaries already compute the TLS 1.3 cryptography for a working handshake. This post stands on its own.

There is a sentence in the design document of Verbose's TLS layer, section 4:

No cryptography in the host.

All the crypto — AES, GHASH, key derivation, SHA-256 — was supposed to run inside binaries emitted by Verbose, carrying their proofs. The Python script that orchestrates them was meant to do plumbing only: launch, carry bytes, file results.

Three sections later, in the same document, a numbered audit finding called MAJOR-1 says that is false. Six computations were still in Python: the nonce, the authenticated header, the initial counter block, the length block, the tag, and the tag comparison. Not plumbing. Cryptography — small, but the real kind, the kind that, done wrong, lets a forged message through.

Section 4 was not quietly rewritten. Section 7 was added, with the word false in it. Then the six computations moved. That is PR #199, and it is all this post is about.

What "framing" means

We are not going to re-explain AES-GCM. We are going to look at what surrounds the encryption, because that is where the six computations lived.

The analogy: a registered letter. The message is inside the envelope, encrypted — Verbose already did that part. But around it there is:

  ┌─────────────────────────────────────────────────────────────┐
  │  tracking number     ← must NEVER repeat                    │
  │  ─────────────────                                          │
  │  visible header      ← the courier reads it, but if it is   │
  │  (type, version,       altered the seal no longer holds     │
  │   length)                                                    │
  │  ─────────────────                                          │
  │  [ encrypted body ]                                         │
  │  ─────────────────                                          │
  │  wax seal            ← 16 bytes proving that nothing,       │
  │                        header or body, was touched          │
  └─────────────────────────────────────────────────────────────┘

And on receipt: check the seal without telling the forger where the forgery failed. We will come back to that; it is the heart of the post.

The six computations, mapped onto the envelope:

  rule           what it produces                              size
  ───────────────────────────────────────────────────────────────────
  gcm_nonce      the tracking number: IV ⊕ sequence number     12 B
  gcm_j0         the counter's start block: nonce ‖ 0³¹ ‖ 1    16 B
  gcm_aad        the visible header: 23 ‖ 0303 ‖ length         5 B
  gcm_lenblock   the lengths in bits, for the seal             16 B
  gcm_tag        the seal: S ⊕ E_K(J0)                         16 B
  gcm_tag_eq     "is the received seal the right one?"         0 / 1

Each cites its reference — RFC 8446 for TLS, SP 800-38D for GCM — in its @intention. Each is an ordinary Verbose rule, with purity and termination proofs.

Why now, and why without touching the compiler

Look at the right-hand column. 12, 16, 5, 16, 16, 1. Everything is fixed-width.

That is the key. A few weeks ago, the aggregate-return arc taught Verbose rules to return a record — a multi-field structure — to another rule, without copying. A rule that returns 16 bytes as a record is exactly what TLS framing needs, and exactly what did not exist when section 4 was written.

So the six computations became six rules. The PR touches src/native.rs on 178 lines — all of them tests. Zero compiler changes. The language already had everything it needed; the only thing left was to stop doing the work somewhere else.

What stays on the host is named, and it is precisely what section 4 allowed from the start: the block-by-block CTR loop over a variable-length payload, zero-padding a variable tail, and shuttling records between binaries. Variable width, out of scope. Fixed width, in Verbose. The boundary is finally where the doc said it was.

The rule worth stopping on

Five of the six rules assemble bytes. The sixth compares them, and that is where a mistake does not show.

Here is the problem. You receive a TLS record with its 16-byte tag. You recompute the tag on your side. You have to say equal or not equal. The obvious way:

  for each byte i from 0 to 15:
      if received[i] ≠ computed[i]:
          answer "false"           ← stop at the first mismatch
  answer "true"

It is correct. It is what anyone would write without thinking. And it is a vulnerability.

The analogy: a bouncer who checks a password letter by letter and turns you away at the first wrong letter. You do not know the password. But you have a stopwatch. You try A…, B…, C… — the refusal is instant. Then S… — the refusal comes a hair later. He checked one more letter: the first one is an S. Repeat for the second. Sixteen letters, a few hundred tries, and you are in without ever having guessed the password: you measured it.

That is a timing side channel, and for an authentication tag it is fatal: an attacker who can forge a tag can get any message accepted. So the rule is absolute: the comparison's running time must not depend on any byte of either tag. No if. No early exit. The same number of operations, always.

Here is gcm_tag_eq, as it sits in the repo:

rule gcm_tag_eq
  @intention: "constant-time equality of two 16-byte tags: 1 when every
               byte matches, 0 otherwise, with no data-dependent branch
               in the accumulation"
  input:
    p : TagPair            -- a0..a15: the computed tag, r0..r15: the received one
  output:
    eq : number
  logic:
    let d0  = bxor(p.a0, p.r0)
    let d1  = bor(d0,  bxor(p.a1,  p.r1))
    let d2  = bor(d1,  bxor(p.a2,  p.r2))
    ...
    let d15 = bor(d14, bxor(p.a15, p.r15))
    eq = 1 - min(d15, 1)
  proofs:
    purity:
      reads : [p.a0, …, p.a15, p.r0, …, p.r15]
      calls : []
    termination:
      bound : 2

Walk it through. bxor — exclusive OR — is 0 if and only if the two bytes are identical. bor — OR — accumulates: once a difference has appeared, it never goes away.

  Case 1 — the two tags are identical:

    bxor(a0,r0)=0   bxor(a1,r1)=0   …   bxor(a15,r15)=0
    d0 = 0
    d1 = 0 | 0 = 0
    …
    d15 = 0
    eq  = 1 - min(0, 1) = 1 - 0 = 1          → equal

  Case 2 — exactly one byte differs, the third:

    bxor(a0,r0)=0   bxor(a1,r1)=0   bxor(a2,r2)=0   bxor(a3,r3)=0x5A   …
    d0 = 0
    d1 = 0
    d2 = 0
    d3 = 0 | 0x5A = 0x5A         ← the difference enters
    d4 = 0x5A | 0 = 0x5A            and stays, whatever follows
    …
    d15 = 0x5A
    eq  = 1 - min(0x5A, 1) = 1 - 1 = 0        → not equal

Look at what the two cases do: sixteen XORs, fifteen ORs, one min, one subtraction. Thirty-three operations in both cases. Whether the difference is in the third byte, the sixteenth, or nowhere, the path is the same. The stopwatch measures nothing anymore.

The min(d15, 1) deserves a word: d15 is 0 or anything non-zero — 0x5A, 0xFF, 3. We want a clean boolean. min(x, 1) clamps every non-zero to 1 without branching. Then 1 - … inverts. Two arithmetic operations where one would be tempted to write if d15 == 0.

And the proofs: block tells the compiler: this rule reads exactly these 32 fields, calls nothing, terminates in two steps. Not a comment; if the logic read an undeclared field, it would not compile. The language's standing promise — the author declares, the binary doesn't drift — applies here to a rule whose shape is a security property.

The oracle that does not lie

How do we know the six rules are right? Not by rereading them — we saw this summer what rereading is worth for this class of bug.

Three levels, from most local to most unforgiving:

1. Each rule against an independent reference. gcm_nonce is compared byte for byte with a third-party RFC 8446 implementation. gcm_tag_eq is run on: two equal tags → 1; one bit flipped at each of the sixteen positions → 0 every time; two entirely different tags → 0.
2. The crypto harness — VCRYPTO_OK, with a new framing leg at 2 ms, and a full AEAD round trip.
3. A real TLS 1.3 handshake, against a real openssl s_client 3.6.2, PSK-DHE: Protocol: TLSv1.3, Verify return code: 0, and a hello world delivered through the tunnel.

The third level is the one that counts. A nonce off by one bit, a length block in bytes instead of bits, a tag computed over the wrong header — and openssl refuses the session. It does not know Verbose, does not read the docs, does not extend trust. That is exactly what you want from an oracle.

And the usual obsession: the corpus's 128 binaries, recompiled before and after, byte-identical. Six rules added, nothing else moved.

What it teaches

A doc that says "no cryptography in the host" while six pieces of it are there is not a lie — it is an intention written before the language could keep it. What matters is what you do the day the gap is measured. Here: it was written down in the same document, then the sentence was made true. Section 4 is now restated honestly — that is the PR's own phrase.

And the limit, named as in previous posts: v0.11.0 is not tagged, ~25 commits past v0.10.0, plus eight draft PRs stacked this week on a bounded-HTTP arc. The rhythm has changed shape — fewer merges, more parallel work in progress. We will see what comes of it.

Sixteen XORs, not a single if. The seal is checked in thirty-three operations, always the same ones, and the only thing a stopwatch will learn there is that there is nothing to learn.

French original on arcker.org.