TLS ClientHello parser and printer, with a proved round trip

.github/workflows/bar.yml

@@ -0,0 +1,21 @@
+name: verified bar
+
+on:
+  push:
+  pull_request:
+  # Rerun when the spec reviewer approves, or an approval is dismissed.
+  pull_request_review:
+    types: [submitted, dismissed]
+
+jobs:
+  bar:
+    # pull-requests: read lets the check confirm the spec approval on GitHub.
+    permissions:
+      contents: read
+      pull-requests: read
+    # Both lines pin the same commit of Proven-Commons/mission: bar v2, as
+    # proposed in its pull request #2. Move both to a release tag once
+    # mission publishes one.
+    uses: Proven-Commons/mission/.github/workflows/verified-bar.yml@6ba85c27abaaf07905c9316aa96dc29f7b5847a2
+    with:
+      bar-ref: 6ba85c27abaaf07905c9316aa96dc29f7b5847a2

.gitignore

@@ -1 +1,4 @@
 .lake/
+__pycache__/
+venv/
+scratch/

ClientHello.lean

@@ -0,0 +1,2 @@
+import ClientHello.Value
+import ClientHello.Parse

ClientHello/Parse.lean

@@ -0,0 +1,270 @@
+/-
+  The TLS ClientHello parser. It reads one record holding
+  one ClientHello and returns the message, or `none` when the
+  bytes break any of the rules in SPEC.md. Every read is
+  length checked before it happens, so the parser never
+  reads past the end of its input:
+
+  - The record header is five bytes: content type 22, a
+    legacy record version carried unchecked, and a two byte
+    length. The body is exactly that many bytes, and no bytes
+    may follow the record. A body of length 0 cannot hold a
+    handshake header, so it is turned away by the body read.
+  - The handshake header is a type byte, which must be 1,
+    and a three byte length that must cover the rest of the
+    record body exactly.
+  - The body fields follow their length rules: session id at
+    most 32 bytes; cipher suites an even byte count of at
+    least 2; compression methods at least one byte and the
+    null method 0 among them. A body that ends before the
+    extensions length is turned away: the extensions block
+    must be present, though it may be empty.
+  - The extensions block is consumed exactly. Each extension
+    is a type, a length, and that many value bytes; a length
+    running past the block turns the message away, and a
+    type standing twice turns it away.
+  - Four extension values are decoded. In each, the inner
+    length must cover the rest of the value exactly. Server
+    name entries may not repeat a name type, and a host_name
+    entry must be nonempty. ALPN names must be nonempty.
+    supported_versions in a hello is a list of two byte
+    versions of even, nonzero byte length. Key share entries
+    may not repeat a group, and key exchange bytes must be
+    nonempty. Every other type is carried opaque.
+
+  The variable length lists are read with a fuel count, one
+  more than the length of the input at the top level, which
+  is always enough, since every step takes bytes. A hostile
+  input is rejected, never looped on.
+-/
+
+import ClientHello.Value
+
+namespace ClientHello
+
+/-- Read one byte as a value, with the rest of the input. -/
+def getU8 : List UInt8 → Option (Nat × List UInt8)
+  | b :: rest => some (b.toNat, rest)
+  | [] => none
+
+/-- Read two bytes as a big endian value, with the rest of
+    the input. Fewer than two bytes gives `none`. -/
+def getU16 : List UInt8 → Option (Nat × List UInt8)
+  | a :: b :: rest => some (u16 a b, rest)
+  | _ => none
+
+/-- Read three bytes as a big endian value, with the rest of
+    the input. Fewer than three bytes gives `none`. -/
+def getU24 : List UInt8 → Option (Nat × List UInt8)
+  | a :: b :: c :: rest => some (u24 a b c, rest)
+  | _ => none
+
+/-- Read `n` bytes as a block, with the rest of the input.
+    Fewer than `n` bytes gives `none`. -/
+def getBytes (n : Nat) (bs : List UInt8) :
+    Option (List UInt8 × List UInt8) :=
+  if (bs.take n).length = n then some (bs.take n, bs.drop n)
+  else none
+
+/-- Read a list of two byte values from bytes that must be
+    consumed exactly. An odd trailing byte gives `none`. -/
+def parsePairs : List UInt8 → Option (List Nat)
+  | [] => some []
+  | a :: b :: rest =>
+    (parsePairs rest).map (fun vs => u16 a b :: vs)
+  | _ => none
+
+/-- Read server name entries with a fuel count. A name type
+    standing twice in the list gives `none`; the repeat
+    check is made against the entries that follow. -/
+def parseNameEntriesGo :
+    Nat → List UInt8 → Option (List (Nat × List UInt8))
+  | 0, _ => none
+  | _ + 1, [] => some []
+  | f + 1, t :: rest =>
+    getU16 rest >>= fun (n, r1) =>
+    if (r1.take n).length = n then
+      parseNameEntriesGo f (r1.drop n) >>= fun es =>
+      if t.toNat ∈ es.map Prod.fst then none
+      else some ((t.toNat, r1.take n) :: es)
+    else none
+
+/-- Read server name entries, with enough fuel for the whole
+    input. -/
+def parseNameEntries (bs : List UInt8) :
+    Option (List (Nat × List UInt8)) :=
+  parseNameEntriesGo (bs.length + 1) bs
+
+/-- The server name value check that stands outside the
+    entry grammar: the list is nonempty, and every host_name
+    entry (type 0) carries at least one byte. -/
+def validNames (es : List (Nat × List UInt8)) : Bool :=
+  !es.isEmpty &&
+  es.all (fun e => decide (e.1 ≠ 0 ∨ e.2 ≠ []))
+
+/-- Read the server_name value: a two byte list length that
+    covers the rest of the value, then the entries, then
+    the value check. -/
+def parseSNI (v : List UInt8) : Option Extension :=
+  getU16 v >>= fun (n, rest) =>
+  if rest.length = n then
+    parseNameEntries rest >>= fun es =>
+    if validNames es then some (.serverName es) else none
+  else none
+
+/-- Read ALPN protocol names with a fuel count. An empty
+    name gives `none`. -/
+def parseAlpnGo : Nat → List UInt8 → Option (List (List UInt8))
+  | 0, _ => none
+  | _ + 1, [] => some []
+  | f + 1, len :: rest =>
+    if len.toNat = 0 then none
+    else if (rest.take len.toNat).length = len.toNat then
+      (parseAlpnGo f (rest.drop len.toNat)).map
+        (fun ns => (rest.take len.toNat) :: ns)
+    else none
+
+/-- Read ALPN protocol names, with enough fuel for the whole
+    input. -/
+def parseAlpnNames (bs : List UInt8) :
+    Option (List (List UInt8)) :=
+  parseAlpnGo (bs.length + 1) bs
+
+/-- Read the ALPN value: a two byte list length that covers
+    the rest of the value, then at least one name. -/
+def parseALPN (v : List UInt8) : Option Extension :=
+  getU16 v >>= fun (n, rest) =>
+  if rest.length = n then
+    parseAlpnNames rest >>= fun ns =>
+    if ns.isEmpty then none else some (.alpn ns)
+  else none
+
+/-- Read the supported_versions value, in the ClientHello
+    form: a one byte length, even and at least 2, then that
+    many bytes as two byte versions. -/
+def parseSV (v : List UInt8) : Option Extension :=
+  match v with
+  | n :: rest =>
+    if rest.length = n.toNat ∧ n.toNat % 2 = 0 ∧ 2 ≤ n.toNat
+      then parsePairs rest >>= fun vs =>
+        some (.supportedVersions vs)
+    else none
+  | [] => none
+
+/-- Read key share entries with a fuel count. Empty key
+    exchange bytes give `none`, and a group standing twice
+    in the list gives `none`. -/
+def parseSharesGo :
+    Nat → List UInt8 → Option (List (Nat × List UInt8))
+  | 0, _ => none
+  | _ + 1, [] => some []
+  | f + 1, bs =>
+    getU16 bs >>= fun (g, r1) =>
+    getU16 r1 >>= fun (n, r2) =>
+    if n = 0 then none
+    else if (r2.take n).length = n then
+      parseSharesGo f (r2.drop n) >>= fun ss =>
+      if g ∈ ss.map Prod.fst then none
+      else some ((g, r2.take n) :: ss)
+    else none
+
+/-- Read key share entries, with enough fuel for the whole
+    input. -/
+def parseShares (bs : List UInt8) :
+    Option (List (Nat × List UInt8)) :=
+  parseSharesGo (bs.length + 1) bs
+
+/-- Read the key_share value, in the client form: a two
+    byte list length that covers the rest of the value, then
+    at least one entry. -/
+def parseKS (v : List UInt8) : Option Extension :=
+  getU16 v >>= fun (n, rest) =>
+  if rest.length = n then
+    parseShares rest >>= fun ss =>
+    if ss.isEmpty then none else some (.keyShare ss)
+  else none
+
+/-- Read one extension value, by its type. The four decoded
+    types go to their readers; every other type is carried
+    opaque, as the type and the value bytes as they stood. -/
+def parseExtValue (t : Nat) (v : List UInt8) :
+    Option Extension :=
+  if t = 0 then parseSNI v
+  else if t = 16 then parseALPN v
+  else if t = 43 then parseSV v
+  else if t = 51 then parseKS v
+  else some (.opaque t v)
+
+/-- Read the extensions of a block that must be consumed
+    exactly, with a fuel count. An extension length running
+    past the block gives `none`, and a type standing twice
+    gives `none`. -/
+def parseExtsGo : Nat → List UInt8 → Option (List Extension)
+  | 0, _ => none
+  | _ + 1, [] => some []
+  | f + 1, bs =>
+    getU16 bs >>= fun (t, r1) =>
+    getU16 r1 >>= fun (n, r2) =>
+    if (r2.take n).length = n then
+      parseExtValue t (r2.take n) >>= fun e =>
+      parseExtsGo f (r2.drop n) >>= fun es =>
+      if extType e ∈ es.map extType then none
+      else some (e :: es)
+    else none
+
+/-- Read an extensions block, with enough fuel for the
+    whole block. -/
+def parseExts (bs : List UInt8) : Option (List Extension) :=
+  parseExtsGo (bs.length + 1) bs
+
+/-- Read the body fields from bytes that are exactly the
+    fields: legacy version, random, session id, cipher
+    suites, compression methods, and the extensions block,
+    which must be present and must run to the end. -/
+def parseBodyFields (bs : List UInt8) : Option Hello :=
+  getU16 bs >>= fun (ver, r1) =>
+  getBytes 32 r1 >>= fun (rand, r2) =>
+  getU8 r2 >>= fun (slen, r3) =>
+  (if slen ≤ 32 then getBytes slen r3 else none) >>=
+    fun (sess, r4) =>
+  getU16 r4 >>= fun (clen, r5) =>
+  (if clen % 2 = 0 ∧ 2 ≤ clen then getBytes clen r5
+   else none) >>= fun (cbytes, r6) =>
+  parsePairs cbytes >>= fun suites =>
+  getU8 r6 >>= fun (mlen, r7) =>
+  (if 1 ≤ mlen then getBytes mlen r7 else none) >>=
+    fun (comps, r8) =>
+  if (0 : UInt8) ∈ comps then
+    getU16 r8 >>= fun (elen, r9) =>
+    getBytes elen r9 >>= fun (ebytes, r10) =>
+    if r10 = [] then
+      parseExts ebytes >>= fun exts =>
+      some ⟨ver, rand, sess, suites, comps, exts⟩
+    else none
+  else none
+
+/-- Read the handshake message from a record body: the type
+    byte must be 1, and the three byte length must cover the
+    rest of the body exactly. -/
+def parseBody (body : List UInt8) : Option Hello :=
+  getU8 body >>= fun (htype, r1) =>
+  if htype = 1 then
+    getU24 r1 >>= fun (hlen, r2) =>
+    getBytes hlen r2 >>= fun (fbs, r3) =>
+    if r3 = [] then parseBodyFields fbs else none
+  else none
+
+/-- Parse a whole message: one record, holding one
+    ClientHello, with no bytes after the record. -/
+def parse (bs : List UInt8) : Option Message :=
+  getU8 bs >>= fun (ct, r1) =>
+  if ct = 22 then
+    getU16 r1 >>= fun (rv, r2) =>
+    getU16 r2 >>= fun (rlen, r3) =>
+    getBytes rlen r3 >>= fun (body, r4) =>
+    if r4 = [] then
+      (parseBody body).map (fun h => ⟨rv, h⟩)
+    else none
+  else none
+
+end ClientHello