TLS 1.3 without a library — a real browser does the handshake against Verbose machine code

#compilers #cryptography #programming #rust

This is an English version of an article first published, in French, on my blog: arcker.org. It's part of an educational series about Verbose — an experimental language whose compiler verifies proofs declared in source and emits small, readable x86-64 machine code.

When your browser shows a little padlock next to a URL, it has just held a cryptographic conversation with the server — the TLS handshake. That conversation is usually handled by enormous C libraries: OpenSSL, BoringSSL, hundreds of thousands of lines nobody ever reads in full.

This article is the capstone of the crypto arc of the series. It shows the payoff: a real browser opens an HTTPS page served by a binary whose every cryptographic transform — the key exchange, the identity signature, the bulk encryption, the hash — is machine code emitted by Verbose. Not one line of OpenSSL. And the browser, the most demanding TLS client there is, can't tell the difference: it completes the handshake and renders the page.

We build on SHA-256 (chapter 1 of the arc) — it shows up everywhere in TLS. The details of each brick (AES, Ed25519) get their own chapters; here we pull up and watch the whole thing work.

A handshake, in three ideas

Before any encrypted exchange, the browser and the server have to settle three things. That's all of TLS, one sentence each:

Agree on a secret that no eavesdropper can guess, even after hearing the entire conversation (the key exchange).
Prove identity — the server shows a certificate and signs, so you know you're talking to the right party (the signature).
Talk encrypted — once the shared secret exists, everything else is encrypted with a fast symmetric algorithm (the bulk encryption).

On the wire, it looks like this:

  BROWSER                                 SERVER (Verbose binary)
      │                                          │
      │ ─── ClientHello ───────────────────────► │  "here are my algos + my key"
      │ ◄── ServerHello ───────────────────────- │  "here's mine"
      │            (encrypted from here on)      │
      │ ◄── Certificate + signature ──────────── │  "here's who I am, signed"
      │ ─── Finished ──────────────────────────► │
      │ ◄══ HTML page (AES-GCM encrypted) ══════ │  "Hello from Verbose TLS"
      │                                          │

Each of the three ideas needs a cryptographic ingredient. And that's where Verbose comes in.

The ingredients — and where the boundary runs

Here's the part that matters for Verbose's thesis. All the cryptography is Verbose machine code. The host (in Python) only does plumbing: open the socket, frame the TLS messages, and draw the one random secret (os.urandom).

  ┌────────────────────────────────────────────────────────────┐
  │  HOST (Python)  : socket, TLS record framing,              │
  │                   os.urandom (the only secret input)       │
  ├────────────────────────────────────────────────────────────┤
  │  VERBOSE (x86-64 machine code) :                           │
  │     X25519          the key exchange                       │
  │     Ed25519 / P-256 the identity signature                 │
  │     AES-128-GCM     the bulk encryption                    │
  │     SHA-256 + HKDF  the hash and key derivation            │
  └────────────────────────────────────────────────────────────┘

Every line of the Verbose block was validated byte-for-byte against a reference before being assembled:

AES-128-GCM against the NIST GCM Test Case 2 vector;
X25519 against RFC 7748;
Ed25519 against the three RFC 8032 §7.1 vectors;
HKDF against RFC 5869;
SHA-256, as we saw in chapter 1, against sha256sum.

Nothing is taken on faith because "it worked once." Each brick is checked against the official spec, in isolation, before it's stacked into the next.

The only loop in all of TLS: the X25519 ladder

Almost all the cryptography here is unrolled: each operation finishes in a fixed number of steps the verifier can follow statically. There's exactly one real loop — the X25519 key exchange, which climbs a "ladder" (the Montgomery ladder) over 255 rungs.

In Verbose, a loop is written as recursion, and — like in chapter 3 — it has to prove it terminates:

rule ladder
  logic:
    ...
    out = if s.i == 0 then <the ladder result>
          else ladder(LadderState { ..., i: s.i - 1, ... })
  proofs:
    termination:
      decreasing : i

(The real state carries ~50 fields — the field elements over 10 limbs — elided here.) The key point: decreasing : i is a compile-time-verified promise. The rung i strictly decreases on every call, so the compiler proves the ladder stops. The 255 iterations run at runtime; the guarantee that they finish is established before the binary even exists. No general loop construct was added to do TLS — the proof tools from chapter 3 are enough.

The catch: a real browser doesn't compromise

The first server signed its identity with Ed25519. Against openssl s_client — the usual test client — everything passed: Verify return code: 0 (ok), signature ed25519. We could have declared victory there.

Except a real browser refused. Flat: illegal_parameter.

Why? In its ClientHello, the browser announces the signature schemes it accepts (the signature_algorithms extension). And browsers offer ecdsa_secp256r1_sha256 (P-256), not Ed25519. RFC 8446 requires the server to sign with an offered scheme. Ed25519 wasn't offered → immediate rejection.

That's exactly the value of a real browser as a target: it imposes constraints a test client lets slide. So we had to build the whole ECDSA P-256 stack — GF(p256) field arithmetic, point add/double, scalar multiplication, the modular inverse, and ECDSA-P256-SHA256 signing (RFC 6979 deterministic nonce, DER encoding, low-s) — validated against the RFC 6979 §A.2.5 vectors and openssl dgst -verify.

With a P-256 certificate, the browser stops saying illegal_parameter. It completes the handshake. It renders the page: "Hello from Verbose TLS". The only remaining warning is the expected self-signed-certificate one. Not a crypto failure. The page renders.

The detail that's fun: smaller, for free

Two recursive rewrites, the same week, at zero compute cost:

p256_ninv: 11.2 MB → 84 KB of native code (131× smaller), 8/8 byte-for-byte vs the unrolled version.
x25519_finish: 1.3 MB → 42 KB (31× smaller), 266 field multiplications identical to the unrolled version. openssl handshake re-validated after the cure.

Same algorithm, same exact output, zero CPU overhead. The recursive path introduced for self-hosting (Phase A) turned out to be the right tool for collapsing huge unrolled cryptographic chains into compact machine code.

Why it matters

TLS 1.3 is not a toy: it's a stack of cryptographic primitives, inside a state machine, inside a wire format, with a public client — your browser — that won't compromise on any of it. Making it work end-to-end is empirical proof that the language and its compiler can express, verify, and run a real protocol, not a demo.

And the method is the message. The cryptography here isn't credible because a tool produced it — it's credible because it's confronted, brick by brick, with the RFC vectors, then with OpenSSL, then with a browser that forgives nothing. You don't trust, you verify. That's the whole difference, and that's all of Verbose: a binary small enough to read, proofs declared in source, and output checked against reality at every step.

The arc began with a 12 KB hash in chapter 1. It ends with a browser rendering a page encrypted by a binary you can read line by line. In between, each brick still needs telling in detail — AES, Ed25519, the Montgomery ladder. Those are the next chapters.

Originally published on arcker.org, where the full series lives.