diff --git a/.github/workflows/bar.yml b/.github/workflows/bar.yml new file mode 100644 index 0000000..32457ed --- /dev/null +++ b/.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 diff --git a/.gitignore b/.gitignore index 01f8cdb..a2759c4 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1,4 @@ .lake/ +__pycache__/ +venv/ +scratch/ diff --git a/ClientHello.lean b/ClientHello.lean new file mode 100644 index 0000000..cd42942 --- /dev/null +++ b/ClientHello.lean @@ -0,0 +1,2 @@ +import ClientHello.Value +import ClientHello.Parse diff --git a/ClientHello/Parse.lean b/ClientHello/Parse.lean new file mode 100644 index 0000000..275fe5b --- /dev/null +++ b/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 diff --git a/ClientHello/Value.lean b/ClientHello/Value.lean new file mode 100644 index 0000000..425a582 --- /dev/null +++ b/ClientHello/Value.lean @@ -0,0 +1,224 @@ +/- + The TLS ClientHello data model and the canonical printer. + + A message is one TLS record holding one ClientHello, in the + shape of RFC 8446 section 4.1.2 with the legacy fields of + RFC 5246. The record header carries a content type, which + must be 22 (handshake), a legacy record version, which is + carried unchecked, and a length. Inside it, a handshake + header carries the message type, which must be 1 + (client_hello), and a three byte length. The body holds the + legacy version, the 32 byte random, the legacy session id, + the cipher suites, the legacy compression methods, and the + extensions. + + Four extensions are decoded: server_name (0, RFC 6066 + section 3), ALPN (16, RFC 7301), supported_versions (43), + and key_share (51). Every other extension is carried as its + type and its raw value bytes, length checked and not read. + + Numbers are held as plain natural numbers. Byte blocks are + held as byte lists. Printing recomputes every length from + the value it prints, so a printed message is the canonical + form of the value. +-/ + +namespace ClientHello + +/-- A value as two bytes, big endian. The value is taken + modulo 2^16; callers only pass values below that. -/ +def be16 (n : Nat) : List UInt8 := + [ (n / 256).toUInt8, n.toUInt8 ] + +/-- The value of two bytes read big endian. -/ +def u16 (a b : UInt8) : Nat := + a.toNat * 256 + b.toNat + +/-- A value as three bytes, big endian. The value is taken + modulo 2^24; callers only pass values below that. -/ +def be24 (n : Nat) : List UInt8 := + [ (n / 65536).toUInt8, (n / 256).toUInt8, n.toUInt8 ] + +/-- The value of three bytes read big endian. -/ +def u24 (a b c : UInt8) : Nat := + a.toNat * 65536 + b.toNat * 256 + c.toNat + +/-- One extension. The four decoded forms are distinct from + the opaque form, which carries a type the slice does not + decode and the value bytes as they stood. A server name + entry is a name type and its bytes; a key share entry is + a group and its key exchange bytes. -/ +inductive Extension where + | serverName (entries : List (Nat × List UInt8)) : Extension + | alpn (names : List (List UInt8)) : Extension + | supportedVersions (versions : List Nat) : Extension + | keyShare (shares : List (Nat × List UInt8)) : Extension + | opaque (extType : Nat) (value : List UInt8) : Extension + deriving DecidableEq, Repr + +/-- The wire type of an extension. -/ +def extType : Extension → Nat + | .serverName _ => 0 + | .alpn _ => 16 + | .supportedVersions _ => 43 + | .keyShare _ => 51 + | .opaque t _ => t + +/-- Two byte values in printed form, one after another. -/ +def printPairs : List Nat → List UInt8 + | [] => [] + | v :: vs => be16 v ++ printPairs vs + +/-- Server name entries in printed form: a name type byte, a + two byte length, and the name bytes. -/ +def printNameEntries : List (Nat × List UInt8) → List UInt8 + | [] => [] + | (t, bs) :: es => + (t.toUInt8 :: (be16 bs.length ++ bs)) ++ printNameEntries es + +/-- ALPN protocol names in printed form: a one byte length + and the name bytes. -/ +def printAlpnNames : List (List UInt8) → List UInt8 + | [] => [] + | n :: ns => (n.length.toUInt8 :: n) ++ printAlpnNames ns + +/-- Key share entries in printed form: a two byte group, a + two byte length, and the key exchange bytes. -/ +def printShares : List (Nat × List UInt8) → List UInt8 + | [] => [] + | (g, k) :: ss => + (be16 g ++ (be16 k.length ++ k)) ++ printShares ss + +/-- The value bytes of an extension, as the printer writes + them. Three of the decoded forms open with a length that + covers the rest of the value: two bytes for server_name + and key_share, one byte for supported_versions in a + ClientHello. -/ +def printExtValue : Extension → List UInt8 + | .serverName es => + be16 (printNameEntries es).length ++ printNameEntries es + | .alpn ns => + be16 (printAlpnNames ns).length ++ printAlpnNames ns + | .supportedVersions vs => + (printPairs vs).length.toUInt8 :: printPairs vs + | .keyShare ss => + be16 (printShares ss).length ++ printShares ss + | .opaque _ v => v + +/-- One extension in printed form: type, length, value. -/ +def printExt (e : Extension) : List UInt8 := + be16 (extType e) ++ be16 (printExtValue e).length ++ + printExtValue e + +/-- The extension list in printed form. -/ +def printExts : List Extension → List UInt8 + | [] => [] + | e :: es => printExt e ++ printExts es + +/-- The ClientHello body fields, in wire order. -/ +structure Hello where + /-- The legacy version, two bytes. Carried unchecked. -/ + legacyVersion : Nat + /-- The random: 32 bytes in a well formed message. -/ + random : List UInt8 + /-- The legacy session id: at most 32 bytes in a well + formed message. -/ + sessionId : List UInt8 + /-- The cipher suites, as two byte codes. A well formed + message holds at least one. -/ + cipherSuites : List Nat + /-- The legacy compression methods. A well formed message + holds at least one, and the null method 0 is among + them. -/ + compressionMethods : List UInt8 + /-- The extensions, in wire order. No type stands twice in + a well formed message. -/ + extensions : List Extension + deriving DecidableEq, Repr + +/-- One record holding one ClientHello. -/ +structure Message where + /-- The legacy record version, two bytes. Carried + unchecked. -/ + recordVersion : Nat + /-- The ClientHello the record holds. -/ + hello : Hello + deriving DecidableEq, Repr + +/-- The body fields in printed form, without the handshake + header: legacy version, random, session id with its one + byte length, cipher suites with their two byte length, + compression methods with their one byte length, and the + extensions with their two byte length. -/ +def printBodyFields (h : Hello) : List UInt8 := + be16 h.legacyVersion ++ h.random ++ + (h.sessionId.length.toUInt8 :: h.sessionId) ++ + (be16 (printPairs h.cipherSuites).length ++ + printPairs h.cipherSuites) ++ + (h.compressionMethods.length.toUInt8 :: + h.compressionMethods) ++ + (be16 (printExts h.extensions).length ++ + printExts h.extensions) + +/-- The handshake message in printed form: type 1, a three + byte length, and the body fields. -/ +def printBody (h : Hello) : List UInt8 := + (1 : UInt8) :: (be24 (printBodyFields h).length ++ + printBodyFields h) + +/-- The whole message in printed form: content type 22, the + legacy record version, a two byte length, and the + handshake message. -/ +def print (m : Message) : List UInt8 := + (22 : UInt8) :: (be16 m.recordVersion ++ + (be16 (printBody m.hello).length ++ printBody m.hello)) + +/-- Well formedness of one extension, at the level the + printer needs: every length it writes fits the field that + holds it, and the checks the parser makes on the value + hold. -/ +def ExtWF : Extension → Prop + | .serverName es => + es ≠ [] ∧ + (∀ e ∈ es, e.1 < 256 ∧ e.2.length ≤ 65535 ∧ + (e.1 = 0 → e.2 ≠ [])) ∧ + List.Nodup (es.map Prod.fst) ∧ + (printNameEntries es).length ≤ 65533 + | .alpn ns => + ns ≠ [] ∧ + (∀ n ∈ ns, n ≠ [] ∧ n.length ≤ 255) ∧ + (printAlpnNames ns).length ≤ 65533 + | .supportedVersions vs => + vs ≠ [] ∧ (∀ v ∈ vs, v < 65536) ∧ vs.length ≤ 127 + | .keyShare ss => + ss ≠ [] ∧ + (∀ s ∈ ss, s.1 < 65536 ∧ s.2 ≠ [] ∧ + s.2.length ≤ 65535) ∧ + List.Nodup (ss.map Prod.fst) ∧ + (printShares ss).length ≤ 65533 + | .opaque t v => + ¬ (t = 0 ∨ t = 16 ∨ t = 43 ∨ t = 51) ∧ + t < 65536 ∧ v.length ≤ 65535 + +/-- A well formed message: every number fits the field that + holds it, every byte block holds the length its field + demands, the cipher suites and compression methods meet + their rules, every extension is well formed, and no + extension type stands twice. -/ +def WF (m : Message) : Prop := + m.recordVersion < 65536 ∧ + m.hello.legacyVersion < 65536 ∧ + m.hello.random.length = 32 ∧ + m.hello.sessionId.length ≤ 32 ∧ + m.hello.cipherSuites ≠ [] ∧ + (∀ v ∈ m.hello.cipherSuites, v < 65536) ∧ + m.hello.cipherSuites.length ≤ 32767 ∧ + m.hello.compressionMethods ≠ [] ∧ + (0 : UInt8) ∈ m.hello.compressionMethods ∧ + m.hello.compressionMethods.length ≤ 255 ∧ + (∀ e ∈ m.hello.extensions, ExtWF e) ∧ + List.Nodup (m.hello.extensions.map extType) ∧ + (printExts m.hello.extensions).length ≤ 65535 ∧ + (printBodyFields m.hello).length ≤ 65531 + +end ClientHello diff --git a/Main.lean b/Main.lean new file mode 100644 index 0000000..642c584 --- /dev/null +++ b/Main.lean @@ -0,0 +1,87 @@ +/- + Command line front end, used by the tests. + + Reads one request per line and prints one answer per line. A + request is an operation and its input as comma-separated + decimal byte codes. + + parse 22,3,3,... prints ok:22,3,3,... or none + + The one operation is `parse`. Its input is the byte codes of + a TLS record holding a ClientHello. Its answer is `ok:` and + the byte codes of the canonical reprint of the parsed + message, or `none` when the message is rejected. + + A request is an operation, then optionally one space and its + numbers; with no numbers after the space, the input is empty. + A malformed request prints `error`: any other line, an unknown + operation, a number that is not plain decimal digits, or a + code above 255, which no byte holds. A line may end in LF or + CR LF; nothing else around a request is ignored. + + The parsing and printing here call `ClientHello.parse` and + `ClientHello.print` directly. The line handling is covered by + the tests, not by a proof. +-/ + +import ClientHello + +open ClientHello + +/-- A number in plain decimal digits. Longer numbers than any + byte code are refused before they are converted, since + that takes time quadratic in their length. -/ +def number (t : String) : Option Nat := + let ds := t.toList + if ds.isEmpty || !ds.all Char.isDigit || (ds.dropWhile (· = '0')).length > 7 then none + else t.toNat? + +/-- The comma-separated numbers in `s`. -/ +def numbers (s : String) : Option (List Nat) := + if s.isEmpty then some [] else (s.splitOn ",").mapM number + +/-- The numbers as bytes. A number above 255 is not a byte, and + makes the request malformed. -/ +def toBytes (ns : List Nat) : Option (List UInt8) := + ns.mapM fun n => if n < 256 then some n.toUInt8 else none + +def showCodes (bs : List UInt8) : String := + ",".intercalate (bs.map fun b => toString b.toNat) + +/-- The answer to one request, or `none` when the request is + malformed. -/ +def answer (op : String) (ns : List Nat) : Option String := + match op with + | "parse" => + match toBytes ns with + | none => none + | some bs => + match parse bs with + | some v => some ("ok:" ++ showCodes (print v)) + | none => some "none" + | _ => none + +/-- The answer to one line: an operation, then optionally one + space and its numbers. -/ +def request (line : String) : Option String := + match line.splitOn " " with + | [op] => answer op [] + | [op, arg] => numbers arg >>= answer op + | _ => none + +/-- The line without its line ending: LF, or CR LF. -/ +def chomp (line : String) : String := + let cs := line.toList + if cs.getLast? = some '\n' then + let cs := cs.dropLast + String.ofList (if cs.getLast? = some '\r' then cs.dropLast else cs) + else line + +def main : IO Unit := do + let stdin ← IO.getStdin + let stdout ← IO.getStdout + repeat + let line ← stdin.getLine + if line.isEmpty then break + let line := chomp line + stdout.putStrLn ((request line).getD "error") diff --git a/Proofs.lean b/Proofs.lean new file mode 100644 index 0000000..36165f5 --- /dev/null +++ b/Proofs.lean @@ -0,0 +1,3 @@ +import Proofs.RoundTrip +import Proofs.SpecProofs +import Proofs.Verify diff --git a/Proofs/RoundTrip.lean b/Proofs/RoundTrip.lean new file mode 100644 index 0000000..6a4b0ab --- /dev/null +++ b/Proofs/RoundTrip.lean @@ -0,0 +1,2036 @@ +/- + The round trip proofs. + + Two claims are proved here, matching the plan's main claim + and its mirror: + + - `parse_print`: for every well formed message, parsing its + printed form gives the message back. + - `print_parse`: for every byte list the parser takes, + printing the parsed message gives the same bytes back. + The printer is canonical and the parser takes exactly the + canonical forms: every length is recomputed from the + value, and the value holds every byte the message + carried, so nothing is lost or added. + + The parser's safety, that it never reads past the end of + its input, is in the shape of the readers: every read is a + `take` whose length is checked first, or a match on bytes + that must be present. SPEC.md states it. +-/ + +import ClientHello + +namespace ClientHello.Proofs + +open ClientHello + +/-! ## Byte and number basics -/ + +/-- A byte printed from a number reads back as the number + modulo 256. -/ +theorem toUInt8_toNat (n : Nat) : (n.toUInt8).toNat = n % 256 := rfl + +/-- A byte's value fits in 256. -/ +theorem toNat_lt (b : UInt8) : b.toNat < 256 := UInt8.toNat_lt_size b + +/-- A byte rebuilt from its value is the byte. -/ +theorem toNat_toUInt8 (b : UInt8) : b.toNat.toUInt8 = b := by + apply UInt8.toNat_inj.mp + show (b.toNat.toUInt8).toNat = b.toNat + rw [toUInt8_toNat] + exact Nat.mod_eq_of_lt (toNat_lt b) + +/-- Two bytes printed from a value below 2^16 read back as + the value. -/ +theorem u16_be16 (n : Nat) (h : n < 65536) : + u16 (n / 256).toUInt8 n.toUInt8 = n := by + simp only [u16, toUInt8_toNat] + omega + +/-- The bytes read as a two byte value print back to those + bytes. -/ +theorem be16_u16 (a b : UInt8) : be16 (u16 a b) = [a, b] := by + have ha := toNat_lt a + have hb := toNat_lt b + have e1 : u16 a b / 256 = a.toNat := by + simp only [u16]; omega + have e2 : (u16 a b).toUInt8 = b := by + apply UInt8.toNat_inj.mp + show ((u16 a b).toUInt8).toNat = b.toNat + rw [toUInt8_toNat]; simp only [u16]; omega + simp only [be16, e1, e2, toNat_toUInt8] + +/-- Three bytes printed from a value below 2^24 read back as + the value. -/ +theorem u24_be24 (n : Nat) (h : n < 16777216) : + u24 (n / 65536).toUInt8 (n / 256).toUInt8 n.toUInt8 = n := by + simp only [u24, toUInt8_toNat] + omega + +/-- The bytes read as a three byte value print back to those + bytes. -/ +theorem be24_u24 (a b c : UInt8) : + be24 (u24 a b c) = [a, b, c] := by + have ha := toNat_lt a + have hb := toNat_lt b + have hc := toNat_lt c + have e1 : u24 a b c / 65536 = a.toNat := by + simp only [u24]; omega + have e2 : (u24 a b c / 256).toUInt8 = b := by + apply UInt8.toNat_inj.mp + show ((u24 a b c / 256).toUInt8).toNat = b.toNat + rw [toUInt8_toNat]; simp only [u24]; omega + have e3 : (u24 a b c).toUInt8 = c := by + apply UInt8.toNat_inj.mp + show ((u24 a b c).toUInt8).toNat = c.toNat + rw [toUInt8_toNat]; simp only [u24]; omega + simp only [be24, e1, e2, e3, toNat_toUInt8] + +/-! ## The readers, on printed forms and on read forms -/ + +/-- One step of the one byte reader, stated for rewriting. -/ +theorem getU8_cons (b : UInt8) (r : List UInt8) : + getU8 (b :: r) = some (b.toNat, r) := rfl + +/-- Reading two bytes off the front of a printed value and + what follows it. -/ +theorem getU16_be16 (n : Nat) (h : n < 65536) (r : List UInt8) : + getU16 (be16 n ++ r) = some (n, r) := by + show getU16 ((n / 256).toUInt8 :: n.toUInt8 :: r) = some (n, r) + show some (u16 (n / 256).toUInt8 n.toUInt8, r) = some (n, r) + rw [u16_be16 n h] + +/-- Reading three bytes off the front of a printed value and + what follows it. -/ +theorem getU24_be24 (n : Nat) (h : n < 16777216) + (r : List UInt8) : + getU24 (be24 n ++ r) = some (n, r) := by + show getU24 ((n / 65536).toUInt8 :: (n / 256).toUInt8 :: + n.toUInt8 :: r) = some (n, r) + show some (u24 (n / 65536).toUInt8 (n / 256).toUInt8 + n.toUInt8, r) = some (n, r) + rw [u24_be24 n h] + +/-- Reading a byte block off the front of a printed block and + what follows it. -/ +theorem getBytes_app {n : Nat} {v : List UInt8} (hv : v.length = n) + (r : List UInt8) : getBytes n (v ++ r) = some (v, r) := by + unfold getBytes + have ht : (v ++ r).take n = v := by + rw [← hv]; exact List.take_left + have hd : (v ++ r).drop n = r := by + rw [← hv]; exact List.drop_left + rw [ht, hd, if_pos hv] + +/-- A byte read by the one byte reader prints back as that + byte: the input was the byte and the rest. -/ +theorem getU8_inv {bs : List UInt8} {n : Nat} {r : List UInt8} + (h : getU8 bs = some (n, r)) : bs = n.toUInt8 :: r := by + cases bs with + | nil => simp [getU8] at h + | cons b r' => + have hstep : getU8 (b :: r') = some (b.toNat, r') := rfl + rw [hstep] at h + simp only [Option.some.injEq, Prod.mk.injEq] at h + obtain ⟨rfl, rfl⟩ := h + rw [toNat_toUInt8] + +/-- Bytes read by the two byte reader print back as those + bytes, and the value fits two bytes. -/ +theorem getU16_inv {bs : List UInt8} {n : Nat} {r : List UInt8} + (h : getU16 bs = some (n, r)) : + bs = be16 n ++ r ∧ n < 65536 := by + cases bs with + | nil => simp [getU16] at h + | cons a bs' => + cases bs' with + | nil => simp [getU16] at h + | cons b r' => + have hstep : getU16 (a :: b :: r') = some (u16 a b, r') := rfl + rw [hstep] at h + simp only [Option.some.injEq, Prod.mk.injEq] at h + obtain ⟨rfl, rfl⟩ := h + refine ⟨?_, ?_⟩ + · simp only [be16_u16, List.cons_append, List.nil_append] + · have ha := toNat_lt a + have hb := toNat_lt b + simp only [u16]; omega + +/-- Bytes read by the three byte reader print back as those + bytes, and the value fits three bytes. -/ +theorem getU24_inv {bs : List UInt8} {n : Nat} {r : List UInt8} + (h : getU24 bs = some (n, r)) : + bs = be24 n ++ r ∧ n < 16777216 := by + cases bs with + | nil => simp [getU24] at h + | cons a bs' => + cases bs' with + | nil => simp [getU24] at h + | cons b bs'' => + cases bs'' with + | nil => simp [getU24] at h + | cons c r' => + have hstep : getU24 (a :: b :: c :: r') + = some (u24 a b c, r') := rfl + rw [hstep] at h + simp only [Option.some.injEq, Prod.mk.injEq] at h + obtain ⟨rfl, rfl⟩ := h + refine ⟨?_, ?_⟩ + · simp only [be24_u24, List.cons_append, List.nil_append] + · have ha := toNat_lt a + have hb := toNat_lt b + have hc := toNat_lt c + simp only [u24]; omega + +/-- A block read by the block reader is its first `n` bytes, + and the rest is the rest: the input was the block and the + rest, and the block holds `n` bytes. -/ +theorem getBytes_inv {n : Nat} {bs v : List UInt8} + {r : List UInt8} (h : getBytes n bs = some (v, r)) : + v.length = n ∧ bs = v ++ r := by + unfold getBytes at h + by_cases hc : (bs.take n).length = n + · rw [if_pos hc] at h + simp only [Option.some.injEq, Prod.mk.injEq] at h + obtain ⟨rfl, rfl⟩ := h + exact ⟨hc, (List.take_append_drop n bs).symm⟩ + · rw [if_neg hc] at h + simp at h + +/-! ## Two byte value lists: the cipher suites and the + supported versions -/ + +/-- The printed length of a two byte value list. -/ +theorem printPairs_length (vs : List Nat) : + (printPairs vs).length = 2 * vs.length := by + induction vs with + | nil => rfl + | cons v vs ih => + simp only [printPairs, be16, List.length_append, + List.length_cons, List.length_nil, ih] + omega + +/-- Printed two byte values read back as the values. -/ +theorem parsePairs_printPairs : + ∀ {vs : List Nat}, (∀ v ∈ vs, v < 65536) → + parsePairs (printPairs vs) = some vs := by + intro vs + induction vs with + | nil => intro _; rfl + | cons v vs ih => + intro hw + have hv : v < 65536 := hw v (by simp) + have htail : ∀ x ∈ vs, x < 65536 := + fun x hx => hw x (List.mem_cons_of_mem v hx) + show parsePairs (be16 v ++ printPairs vs) = some (v :: vs) + show parsePairs ((v / 256).toUInt8 :: v.toUInt8 :: + printPairs vs) = some (v :: vs) + show (parsePairs (printPairs vs)).map + (fun vs' => u16 (v / 256).toUInt8 v.toUInt8 :: vs') + = some (v :: vs) + rw [ih htail, u16_be16 v hv] + rfl + +/-- Two byte values a successful read gives print back to + the bytes they were read from, and each fits two bytes. + The induction is on the byte count, two at a time, since + the reader takes two bytes per value. -/ +theorem parsePairs_inv_aux : ∀ (n : Nat) (bs : List UInt8) + (vs : List Nat), bs.length = n → parsePairs bs = some vs → + printPairs vs = bs ∧ ∀ v ∈ vs, v < 65536 + | 0, bs, vs, hlen, h => by + cases bs with + | nil => + have h1 : parsePairs ([] : List UInt8) = some [] := rfl + rw [h1] at h + simp only [Option.some.injEq] at h + subst h + exact ⟨rfl, by simp⟩ + | cons a bs' => simp at hlen + | 1, bs, vs, hlen, h => by + cases bs with + | nil => simp at hlen + | cons a bs' => + cases bs' with + | nil => simp [parsePairs] at h + | cons b rest => simp at hlen + | n + 2, bs, vs, hlen, h => by + cases bs with + | nil => simp at hlen + | cons a bs' => + cases bs' with + | nil => simp at hlen + | cons b rest => + have hrest : rest.length = n := by + simp only [List.length_cons] at hlen + omega + have hstep : parsePairs (a :: b :: rest) + = (parsePairs rest).map + (fun vs' => u16 a b :: vs') := rfl + rw [hstep] at h + obtain ⟨vs', hrec, hvs⟩ := Option.map_eq_some_iff.mp h + obtain ⟨hprint, hlt⟩ := + parsePairs_inv_aux n rest vs' hrest hrec + refine ⟨?_, ?_⟩ + · show printPairs vs = a :: b :: rest + rw [← hvs] + show printPairs (u16 a b :: vs') = a :: b :: rest + simp only [printPairs, be16_u16, List.cons_append, + List.nil_append, hprint] + · rw [← hvs] + intro x hx + simp only [List.mem_cons] at hx + rcases hx with rfl | hx + · have ha := toNat_lt a + have hb := toNat_lt b + simp only [u16]; omega + · exact hlt x hx + +/-- Two byte values a successful read gives print back to + the bytes they were read from, and each fits two + bytes. -/ +theorem parsePairs_inv {bs : List UInt8} {vs : List Nat} + (h : parsePairs bs = some vs) : + printPairs vs = bs ∧ ∀ v ∈ vs, v < 65536 := + parsePairs_inv_aux bs.length bs vs rfl h + +/-- The count of values a successful two byte read gives, + from the byte count it read. -/ +theorem parsePairs_length {bs : List UInt8} {vs : List Nat} + (h : parsePairs bs = some vs) : + bs.length = 2 * vs.length := by + have h1 := (parsePairs_inv h).1 + rw [← h1, printPairs_length] + +/-! ## Server name entries -/ + +/-- The printed length of a server name entry list, one entry + at a time. -/ +theorem printNameEntries_length_cons (t : Nat) + (bs : List UInt8) (es : List (Nat × List UInt8)) : + (printNameEntries ((t, bs) :: es)).length + = bs.length + 3 + (printNameEntries es).length := by + simp only [printNameEntries, be16, List.length_append, + List.length_cons, List.length_nil] + omega + +/-- One step of the server name entry reader, stated for + rewriting. -/ +theorem parseNameEntriesGo_step (f : Nat) (t : UInt8) + (rest : List UInt8) : + parseNameEntriesGo (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 := rfl + +/-- Printed server name entries read back as the entries. -/ +theorem parseNameEntriesGo_print : + ∀ (es : List (Nat × List UInt8)) (fuel : Nat), + (∀ e ∈ es, e.1 < 256 ∧ e.2.length ≤ 65535) → + List.Nodup (es.map Prod.fst) → + (printNameEntries es).length < fuel → + parseNameEntriesGo fuel (printNameEntries es) = some es := by + intro es + induction es with + | nil => + intro fuel _ _ hf + obtain ⟨f, rfl⟩ : ∃ f, fuel = f + 1 := ⟨fuel - 1, by omega⟩ + rfl + | cons e es ih => + intro fuel hw hnodup hf + obtain ⟨t, bs⟩ := e + have hhead : t < 256 ∧ bs.length ≤ 65535 := + hw (t, bs) (by simp) + have htail : ∀ x ∈ es, x.1 < 256 ∧ x.2.length ≤ 65535 := + fun x hx => hw x (List.mem_cons_of_mem (t, bs) hx) + have hnodup' : List.Nodup (es.map Prod.fst) := by + have h2 : ((t, bs) :: es).map Prod.fst + = t :: es.map Prod.fst := rfl + rw [h2] at hnodup + exact (List.nodup_cons.mp hnodup).2 + have hnotin : t ∉ es.map Prod.fst := by + have h2 : ((t, bs) :: es).map Prod.fst + = t :: es.map Prod.fst := rfl + rw [h2] at hnodup + exact (List.nodup_cons.mp hnodup).1 + obtain ⟨f, rfl⟩ : ∃ f, fuel = f + 1 := ⟨fuel - 1, by omega⟩ + have hf' : (printNameEntries es).length < f := by + have hflen : (printNameEntries ((t, bs) :: es)).length + = bs.length + 3 + (printNameEntries es).length := + printNameEntries_length_cons t bs es + omega + have ht : (t.toUInt8).toNat = t := by + rw [toUInt8_toNat] + exact Nat.mod_eq_of_lt hhead.1 + show parseNameEntriesGo (f + 1) + ((t.toUInt8 :: (be16 bs.length ++ bs)) ++ + printNameEntries es) + = some ((t, bs) :: es) + have hform : (t.toUInt8 :: (be16 bs.length ++ bs)) ++ + printNameEntries es + = t.toUInt8 :: (bs.length / 256).toUInt8 :: + bs.length.toUInt8 :: (bs ++ printNameEntries es) := by + simp only [be16, List.cons_append, List.nil_append] + rw [hform, parseNameEntriesGo_step] + show (getU16 ((bs.length / 256).toUInt8 :: + bs.length.toUInt8 :: (bs ++ printNameEntries es)) >>= + fun (n, r1) => + if (r1.take n).length = n then + parseNameEntriesGo f (r1.drop n) >>= fun es' => + if (t.toUInt8).toNat ∈ es'.map Prod.fst then none + else some (((t.toUInt8).toNat, r1.take n) :: es') + else none) = some ((t, bs) :: es) + have hg : getU16 ((bs.length / 256).toUInt8 :: + bs.length.toUInt8 :: (bs ++ printNameEntries es)) + = some (bs.length, bs ++ printNameEntries es) := by + show some (u16 (bs.length / 256).toUInt8 + bs.length.toUInt8, bs ++ printNameEntries es) = _ + rw [u16_be16 bs.length (by omega)] + rw [hg] + simp only [Option.bind_some] + show (if ((bs ++ printNameEntries es).take bs.length).length + = bs.length then + parseNameEntriesGo f ((bs ++ printNameEntries es).drop + bs.length) >>= fun es' => + if (t.toUInt8).toNat ∈ es'.map Prod.fst then none + else some (((t.toUInt8).toNat, + (bs ++ printNameEntries es).take bs.length) :: es') + else none) = some ((t, bs) :: es) + rw [List.take_left, List.drop_left, if_pos rfl, + ih f htail hnodup' hf'] + show (if (t.toUInt8).toNat ∈ es.map Prod.fst then none + else some (((t.toUInt8).toNat, bs) :: es)) + = some ((t, bs) :: es) + rw [if_neg (by rw [ht]; exact hnotin), ht] + +/-- Printed server name entries read back, at the top + level. -/ +theorem parseNameEntries_print {es : List (Nat × List UInt8)} + (hw : ∀ e ∈ es, e.1 < 256 ∧ e.2.length ≤ 65535) + (hn : List.Nodup (es.map Prod.fst)) : + parseNameEntries (printNameEntries es) = some es := by + show parseNameEntriesGo ((printNameEntries es).length + 1) + (printNameEntries es) = some es + exact parseNameEntriesGo_print es _ hw hn (Nat.lt_succ_self _) + +/-- Server name entries a successful read gives print back + to the bytes they were read from, each name type fits + one byte, each name fits two length bytes, and no name + type stands twice. -/ +theorem parseNameEntriesGo_inv : + ∀ (f : Nat) (bs : List UInt8) + (es : List (Nat × List UInt8)), + parseNameEntriesGo f bs = some es → + printNameEntries es = bs ∧ + (∀ e ∈ es, e.1 < 256 ∧ e.2.length ≤ 65535) ∧ + List.Nodup (es.map Prod.fst) := by + intro f + induction f with + | zero => + intro bs es h + simp [parseNameEntriesGo] at h + | succ f ih => + intro bs es h + cases bs with + | nil => + have h1 : parseNameEntriesGo (f + 1) ([] : List UInt8) + = some [] := rfl + rw [h1] at h + simp only [Option.some.injEq] at h + subst h + exact ⟨rfl, by simp, by simp⟩ + | cons t rest => + rw [parseNameEntriesGo_step] at h + obtain ⟨⟨n, r1⟩, hn, h⟩ := Option.bind_eq_some_iff.mp h + change (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) = some es at h + obtain ⟨hrest, hnlt⟩ := getU16_inv hn + by_cases hc : (r1.take n).length = n + · rw [if_pos hc] at h + obtain ⟨es', hrec, h⟩ := + Option.bind_eq_some_iff.mp h + obtain ⟨hprint, hprops, hnodup⟩ := ih _ _ hrec + by_cases hd : t.toNat ∈ es'.map Prod.fst + · rw [if_pos hd] at h + simp at h + · rw [if_neg hd] at h + simp only [Option.some.injEq, Prod.mk.injEq] at h + obtain ⟨rfl, rfl⟩ := h + refine ⟨?_, ?_, ?_⟩ + · show printNameEntries ((t.toNat, r1.take n) :: es') + = t :: rest + have htake : (r1.take n).length = n := hc + show ((t.toNat.toUInt8 :: + (be16 (r1.take n).length ++ r1.take n)) ++ + printNameEntries es') = t :: rest + rw [htake, hprint, toNat_toUInt8, hrest] + show (t :: ((be16 n ++ r1.take n) ++ r1.drop n)) + = t :: (be16 n ++ r1) + rw [List.append_assoc, List.take_append_drop] + · intro x hx + simp only [List.mem_cons] at hx + rcases hx with rfl | hx + · exact ⟨toNat_lt t, by rw [hc]; omega⟩ + · exact hprops x hx + · have h2 : ((t.toNat, r1.take n) :: es').map Prod.fst + = t.toNat :: es'.map Prod.fst := rfl + rw [h2] + exact List.nodup_cons.mpr ⟨hd, hnodup⟩ + · rw [if_neg hc] at h + simp at h + +/-- Server name entries a successful read gives print back, + at the top level. -/ +theorem parseNameEntries_inv {bs : List UInt8} + {es : List (Nat × List UInt8)} + (h : parseNameEntries bs = some es) : + printNameEntries es = bs ∧ + (∀ e ∈ es, e.1 < 256 ∧ e.2.length ≤ 65535) ∧ + List.Nodup (es.map Prod.fst) := + parseNameEntriesGo_inv _ _ _ h + +/-- The server name value check holds for a list the printer + can write: nonempty, and every host_name entry + nonempty. -/ +theorem validNames_of {es : List (Nat × List UInt8)} + (hne : es ≠ []) + (hhost : ∀ e ∈ es, e.1 = 0 → e.2 ≠ []) : + validNames es = true := by + unfold validNames + rw [Bool.and_eq_true] + constructor + · cases es with + | nil => exact absurd rfl hne + | cons e es' => rfl + · rw [List.all_eq_true] + intro e he + simp only [decide_eq_true_eq] + by_cases h0 : e.1 = 0 + · exact Or.inr (hhost e he h0) + · exact Or.inl h0 + +/-- A server name list that passes the value check is + nonempty, and its host_name entries are nonempty. -/ +theorem validNames_true {es : List (Nat × List UInt8)} + (h : validNames es = true) : + es ≠ [] ∧ ∀ e ∈ es, e.1 = 0 → e.2 ≠ [] := by + have hne : es ≠ [] := by + cases es with + | nil => simp [validNames] at h + | cons e es' => simp + have hall : ∀ e ∈ es, e.1 ≠ 0 ∨ e.2 ≠ [] := by + have h2 : es.all + (fun e => decide (e.1 ≠ 0 ∨ e.2 ≠ [])) = true := by + have h' : (!es.isEmpty && + es.all (fun e => decide (e.1 ≠ 0 ∨ e.2 ≠ []))) + = true := h + rw [Bool.and_eq_true] at h' + exact h'.2 + rw [List.all_eq_true] at h2 + intro e he + have h3 := h2 e he + simpa only [decide_eq_true_eq] using h3 + exact ⟨hne, fun e he h0 => + (hall e he).elim (fun hn => absurd h0 hn) id⟩ + +/-! ## The server_name value -/ + +/-- A printed server_name value reads back as the + extension. -/ +theorem parseSNI_print {es : List (Nat × List UInt8)} + (hne : es ≠ []) + (hw : ∀ e ∈ es, e.1 < 256 ∧ e.2.length ≤ 65535 ∧ + (e.1 = 0 → e.2 ≠ [])) + (hnodup : List.Nodup (es.map Prod.fst)) + (hlen : (printNameEntries es).length ≤ 65533) : + parseSNI (printExtValue (.serverName es)) + = some (.serverName es) := by + have hw' : ∀ e ∈ es, e.1 < 256 ∧ e.2.length ≤ 65535 := + fun e he => ⟨(hw e he).1, (hw e he).2.1⟩ + show parseSNI (be16 (printNameEntries es).length ++ + printNameEntries es) = some (Extension.serverName es) + unfold parseSNI + rw [getU16_be16 _ (by omega)] + simp only [Option.bind_some] + show (if (printNameEntries es).length + = (printNameEntries es).length then + parseNameEntries (printNameEntries es) >>= fun es' => + if validNames es' then some (Extension.serverName es') else none + else none) = some (Extension.serverName es) + rw [if_pos rfl, parseNameEntries_print hw' hnodup] + show (if validNames es then some (Extension.serverName es) + else none) = some (Extension.serverName es) + rw [if_pos (validNames_of hne (fun e he => (hw e he).2.2))] + +/-- A server_name value a successful read gives is the + printed form of the extension it gives, and the + extension is well formed. The value length bound comes + from the caller: an extension value fits two length + bytes. -/ +theorem parseSNI_inv {v : List UInt8} {e : Extension} + (hv : v.length ≤ 65535) (h : parseSNI v = some e) : + ∃ es, e = .serverName es ∧ + printExtValue (.serverName es) = v ∧ + ExtWF (.serverName es) := by + unfold parseSNI at h + obtain ⟨⟨n, rest⟩, hn, h⟩ := Option.bind_eq_some_iff.mp h + change (if rest.length = n then + parseNameEntries rest >>= fun es => + if validNames es then some (.serverName es) else none + else none) = some e at h + obtain ⟨hrest, hnlt⟩ := getU16_inv hn + by_cases hc : rest.length = n + · rw [if_pos hc] at h + obtain ⟨es, hrec, h⟩ := Option.bind_eq_some_iff.mp h + by_cases hval : validNames es = true + · rw [if_pos hval] at h + simp only [Option.some.injEq] at h + subst h + obtain ⟨hprint, hprops, hnodup⟩ := parseNameEntries_inv hrec + obtain ⟨hne, hhost⟩ := validNames_true hval + refine ⟨es, rfl, ?_, ?_⟩ + · show be16 (printNameEntries es).length ++ + printNameEntries es = v + rw [hprint, hc, hrest] + · exact ⟨hne, fun x hx => + ⟨(hprops x hx).1, (hprops x hx).2, hhost x hx⟩, + hnodup, by + have h2 : (printNameEntries es).length = rest.length := by + rw [hprint] + have hvlen : v.length = rest.length + 2 := by + rw [hrest]; simp [be16] + omega⟩ + · rw [if_neg hval] at h + simp at h + · rw [if_neg hc] at h + simp at h + +/-! ## ALPN protocol names -/ + +/-- The printed length of an ALPN name list, one name at a + time. -/ +theorem printAlpnNames_length_cons (n : List UInt8) + (ns : List (List UInt8)) : + (printAlpnNames (n :: ns)).length + = n.length + 1 + (printAlpnNames ns).length := by + simp only [printAlpnNames, List.length_append, + List.length_cons] + +/-- One step of the ALPN name reader, stated for + rewriting. -/ +theorem parseAlpnGo_step (f : Nat) (len : UInt8) + (rest : List UInt8) : + parseAlpnGo (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 := rfl + +/-- Printed ALPN names read back as the names. -/ +theorem parseAlpnGo_print : + ∀ (ns : List (List UInt8)) (fuel : Nat), + (∀ n ∈ ns, n ≠ [] ∧ n.length ≤ 255) → + (printAlpnNames ns).length < fuel → + parseAlpnGo fuel (printAlpnNames ns) = some ns := by + intro ns + induction ns with + | nil => + intro fuel _ hf + obtain ⟨f, rfl⟩ : ∃ f, fuel = f + 1 := ⟨fuel - 1, by omega⟩ + rfl + | cons n ns ih => + intro fuel hw hf + have hhead : n ≠ [] ∧ n.length ≤ 255 := hw n (by simp) + have htail : ∀ x ∈ ns, x ≠ [] ∧ x.length ≤ 255 := + fun x hx => hw x (List.mem_cons_of_mem n hx) + obtain ⟨f, rfl⟩ : ∃ f, fuel = f + 1 := ⟨fuel - 1, by omega⟩ + have hf' : (printAlpnNames ns).length < f := by + have hflen : (printAlpnNames (n :: ns)).length + = n.length + 1 + (printAlpnNames ns).length := + printAlpnNames_length_cons n ns + omega + have hlen : (n.length.toUInt8).toNat = n.length := by + rw [toUInt8_toNat] + exact Nat.mod_eq_of_lt (by omega) + show parseAlpnGo (f + 1) + ((n.length.toUInt8 :: n) ++ printAlpnNames ns) + = some (n :: ns) + have hform : (n.length.toUInt8 :: n) ++ printAlpnNames ns + = n.length.toUInt8 :: (n ++ printAlpnNames ns) := by + simp only [List.cons_append, List.nil_append] + rw [hform, parseAlpnGo_step, hlen, + if_neg (by + intro hcon + cases n with + | nil => exact hhead.1 rfl + | cons b bs => simp at hcon), + List.take_left, List.drop_left, if_pos rfl, ih f htail hf'] + rfl + +/-- Printed ALPN names read back, at the top level. -/ +theorem parseAlpnNames_print {ns : List (List UInt8)} + (hw : ∀ n ∈ ns, n ≠ [] ∧ n.length ≤ 255) : + parseAlpnNames (printAlpnNames ns) = some ns := by + show parseAlpnGo ((printAlpnNames ns).length + 1) + (printAlpnNames ns) = some ns + exact parseAlpnGo_print ns _ hw (Nat.lt_succ_self _) + +/-- ALPN names a successful read gives print back to the + bytes they were read from, and each name is nonempty + and fits one length byte. -/ +theorem parseAlpnGo_inv : + ∀ (f : Nat) (bs : List UInt8) (ns : List (List UInt8)), + parseAlpnGo f bs = some ns → + printAlpnNames ns = bs ∧ + ∀ n ∈ ns, n ≠ [] ∧ n.length ≤ 255 := by + intro f + induction f with + | zero => + intro bs ns h + simp [parseAlpnGo] at h + | succ f ih => + intro bs ns h + cases bs with + | nil => + have h1 : parseAlpnGo (f + 1) ([] : List UInt8) + = some [] := rfl + rw [h1] at h + simp only [Option.some.injEq] at h + subst h + exact ⟨rfl, by simp⟩ + | cons len rest => + rw [parseAlpnGo_step] at h + by_cases h0 : len.toNat = 0 + · rw [if_pos h0] at h + simp at h + · rw [if_neg h0] at h + by_cases hc : (rest.take len.toNat).length = len.toNat + · rw [if_pos hc] at h + obtain ⟨ns', hrec, hns⟩ := Option.map_eq_some_iff.mp h + obtain ⟨hprint, hprops⟩ := ih _ _ hrec + refine ⟨?_, ?_⟩ + · show printAlpnNames ns = len :: rest + rw [← hns] + show printAlpnNames ((rest.take len.toNat) :: ns') + = len :: rest + have htake : (rest.take len.toNat).length + = len.toNat := hc + show ((rest.take len.toNat).length.toUInt8 :: + rest.take len.toNat) ++ printAlpnNames ns' + = len :: rest + rw [htake, toNat_toUInt8, hprint] + show len :: (rest.take len.toNat ++ rest.drop len.toNat) + = len :: rest + rw [List.take_append_drop] + · intro x hx + rw [← hns] at hx + simp only [List.mem_cons] at hx + rcases hx with rfl | hx + · refine ⟨?_, by rw [hc]; have h := toNat_lt len; omega⟩ + intro hcon + rw [hcon] at hc + simp at hc + omega + · exact hprops x hx + · rw [if_neg hc] at h + simp at h + +/-- ALPN names a successful read gives print back, at the + top level. -/ +theorem parseAlpnNames_inv {bs : List UInt8} + {ns : List (List UInt8)} + (h : parseAlpnNames bs = some ns) : + printAlpnNames ns = bs ∧ + ∀ n ∈ ns, n ≠ [] ∧ n.length ≤ 255 := + parseAlpnGo_inv _ _ _ h + +/-- A printed ALPN value reads back as the extension. -/ +theorem parseALPN_print {ns : List (List UInt8)} + (hne : ns ≠ []) + (hw : ∀ n ∈ ns, n ≠ [] ∧ n.length ≤ 255) + (hlen : (printAlpnNames ns).length ≤ 65533) : + parseALPN (printExtValue (.alpn ns)) = some (.alpn ns) := by + show parseALPN (be16 (printAlpnNames ns).length ++ + printAlpnNames ns) = some (Extension.alpn ns) + unfold parseALPN + rw [getU16_be16 _ (by omega)] + simp only [Option.bind_some] + show (if (printAlpnNames ns).length + = (printAlpnNames ns).length then + parseAlpnNames (printAlpnNames ns) >>= fun ns' => + if ns'.isEmpty then none else some (Extension.alpn ns') + else none) = some (Extension.alpn ns) + rw [if_pos rfl, parseAlpnNames_print hw] + show (if ns.isEmpty then none else some (Extension.alpn ns)) + = some (Extension.alpn ns) + rw [if_neg (by + cases ns with + | nil => exact absurd rfl hne + | cons n ns' => simp)] + +/-- An ALPN value a successful read gives is the printed + form of the extension it gives, and the extension is + well formed. -/ +theorem parseALPN_inv {v : List UInt8} {e : Extension} + (hv : v.length ≤ 65535) (h : parseALPN v = some e) : + ∃ ns, e = .alpn ns ∧ + printExtValue (.alpn ns) = v ∧ ExtWF (.alpn ns) := by + unfold parseALPN at h + obtain ⟨⟨n, rest⟩, hn, h⟩ := Option.bind_eq_some_iff.mp h + change (if rest.length = n then + parseAlpnNames rest >>= fun ns => + if ns.isEmpty then none else some (.alpn ns) + else none) = some e at h + obtain ⟨hrest, hnlt⟩ := getU16_inv hn + by_cases hc : rest.length = n + · rw [if_pos hc] at h + obtain ⟨ns, hrec, h⟩ := Option.bind_eq_some_iff.mp h + by_cases hemp : ns.isEmpty = false + · rw [if_neg (by + intro hcon + rw [hcon] at hemp + simp at hemp)] at h + simp only [Option.some.injEq] at h + subst h + obtain ⟨hprint, hprops⟩ := parseAlpnNames_inv hrec + have hne : ns ≠ [] := by + cases ns with + | nil => simp at hemp + | cons n' ns' => simp + refine ⟨ns, rfl, ?_, ?_⟩ + · show be16 (printAlpnNames ns).length ++ + printAlpnNames ns = v + rw [hprint, hc, hrest] + · exact ⟨hne, hprops, by + have h2 : (printAlpnNames ns).length = rest.length := by + rw [hprint] + have hvlen : v.length = rest.length + 2 := by + rw [hrest]; simp [be16] + omega⟩ + · have hemp2 : ns.isEmpty = true := by + cases h' : ns.isEmpty with + | true => rfl + | false => exact absurd h' hemp + rw [if_pos hemp2] at h + simp at h + · rw [if_neg hc] at h + simp at h + +/-! ## The supported_versions value -/ + +/-- A printed supported_versions value reads back as the + extension. -/ +theorem parseSV_print {vs : List Nat} + (hne : vs ≠ []) (hw : ∀ v ∈ vs, v < 65536) + (hlen : vs.length ≤ 127) : + parseSV (printExtValue (.supportedVersions vs)) + = some (.supportedVersions vs) := by + show parseSV ((printPairs vs).length.toUInt8 :: + printPairs vs) = some (.supportedVersions vs) + have hlen2 : ((printPairs vs).length.toUInt8).toNat + = (printPairs vs).length := by + rw [toUInt8_toNat, printPairs_length] + have : 2 * vs.length < 256 := by omega + exact Nat.mod_eq_of_lt this + have hcond : (printPairs vs).length + = ((printPairs vs).length.toUInt8).toNat ∧ + ((printPairs vs).length.toUInt8).toNat % 2 = 0 ∧ + 2 ≤ ((printPairs vs).length.toUInt8).toNat := by + rw [hlen2, printPairs_length] + refine ⟨rfl, by omega, by + cases vs with + | nil => exact absurd rfl hne + | cons v vs' => simp; omega⟩ + show (if (printPairs vs).length + = ((printPairs vs).length.toUInt8).toNat ∧ + ((printPairs vs).length.toUInt8).toNat % 2 = 0 ∧ + 2 ≤ ((printPairs vs).length.toUInt8).toNat then + parsePairs (printPairs vs) >>= fun vs' => + some (Extension.supportedVersions vs') + else none) = some (Extension.supportedVersions vs) + rw [if_pos hcond, parsePairs_printPairs hw] + rfl + +/-- A supported_versions value a successful read gives is + the printed form of the extension it gives, and the + extension is well formed. -/ +theorem parseSV_inv {v : List UInt8} {e : Extension} + (h : parseSV v = some e) : + ∃ vs, e = .supportedVersions vs ∧ + printExtValue (.supportedVersions vs) = v ∧ + ExtWF (.supportedVersions vs) := by + cases v with + | nil => simp [parseSV] at h + | cons n rest => + have hstep : parseSV (n :: rest) = + if rest.length = n.toNat ∧ n.toNat % 2 = 0 ∧ + 2 ≤ n.toNat then + parsePairs rest >>= fun vs => + some (.supportedVersions vs) + else none := rfl + rw [hstep] at h + by_cases hc : rest.length = n.toNat ∧ n.toNat % 2 = 0 ∧ + 2 ≤ n.toNat + · rw [if_pos hc] at h + obtain ⟨vs, hrec, h⟩ := Option.bind_eq_some_iff.mp h + simp only [Option.some.injEq] at h + subst h + obtain ⟨hprint, hlt⟩ := parsePairs_inv hrec + have hlen := parsePairs_length hrec + refine ⟨vs, rfl, ?_, ?_⟩ + · show (printPairs vs).length.toUInt8 :: printPairs vs + = n :: rest + rw [hprint] + have hbyte : (rest.length).toUInt8 = n := by + apply UInt8.toNat_inj.mp + show ((rest.length).toUInt8).toNat = n.toNat + rw [toUInt8_toNat, hc.1] + exact Nat.mod_eq_of_lt (toNat_lt n) + rw [hbyte] + · refine ⟨?_, hlt, by + have h1 := hc.1 + have h2 := toNat_lt n + omega⟩ + cases vs with + | nil => + intro hcon + have h5 := (parsePairs_inv hrec).1 + simp only [printPairs] at h5 + have hz : rest.length = 0 := by + rw [← h5] + simp [printPairs] + have h1 := hc.1 + have h3 := hc.2.2 + omega + | cons v' vs' => intro hcon; cases hcon + · rw [if_neg hc] at h + simp at h + +/-! ## Key share entries -/ + +/-- The printed length of a key share entry list, one entry + at a time. -/ +theorem printShares_length_cons (g : Nat) (k : List UInt8) + (ss : List (Nat × List UInt8)) : + (printShares ((g, k) :: ss)).length + = k.length + 4 + (printShares ss).length := by + show ((be16 g ++ (be16 k.length ++ k)) ++ + printShares ss).length = _ + rw [List.length_append, List.length_append, + List.length_append] + simp only [be16, List.length_cons, List.length_nil] + omega + +/-- One step of the key share entry reader, stated for + rewriting. -/ +theorem parseSharesGo_step (f : Nat) (x y : UInt8) + (rest : List UInt8) : + parseSharesGo (f + 1) (x :: y :: rest) = + getU16 (x :: y :: rest) >>= 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 := rfl + +/-- Printed key share entries read back as the entries. -/ +theorem parseSharesGo_print : + ∀ (ss : List (Nat × List UInt8)) (fuel : Nat), + (∀ s ∈ ss, s.1 < 65536 ∧ s.2 ≠ [] ∧ s.2.length ≤ 65535) → + List.Nodup (ss.map Prod.fst) → + (printShares ss).length < fuel → + parseSharesGo fuel (printShares ss) = some ss := by + intro ss + induction ss with + | nil => + intro fuel _ _ hf + obtain ⟨f, rfl⟩ : ∃ f, fuel = f + 1 := ⟨fuel - 1, by omega⟩ + rfl + | cons s ss ih => + intro fuel hw hnodup hf + obtain ⟨g, k⟩ := s + have hhead : g < 65536 ∧ k ≠ [] ∧ k.length ≤ 65535 := + hw (g, k) (by simp) + have htail : ∀ x ∈ ss, x.1 < 65536 ∧ x.2 ≠ [] ∧ + x.2.length ≤ 65535 := + fun x hx => hw x (List.mem_cons_of_mem (g, k) hx) + have hnodup' : List.Nodup (ss.map Prod.fst) := by + have h2 : ((g, k) :: ss).map Prod.fst + = g :: ss.map Prod.fst := rfl + rw [h2] at hnodup + exact (List.nodup_cons.mp hnodup).2 + have hnotin : g ∉ ss.map Prod.fst := by + have h2 : ((g, k) :: ss).map Prod.fst + = g :: ss.map Prod.fst := rfl + rw [h2] at hnodup + exact (List.nodup_cons.mp hnodup).1 + obtain ⟨f, rfl⟩ : ∃ f, fuel = f + 1 := ⟨fuel - 1, by omega⟩ + have hf' : (printShares ss).length < f := by + have hflen : (printShares ((g, k) :: ss)).length + = k.length + 4 + (printShares ss).length := + printShares_length_cons g k ss + omega + show parseSharesGo (f + 1) + ((be16 g ++ (be16 k.length ++ k)) ++ printShares ss) + = some ((g, k) :: ss) + have hform : (be16 g ++ (be16 k.length ++ k)) ++ + printShares ss + = be16 g ++ (be16 k.length ++ (k ++ printShares ss)) := by + simp only [← List.append_assoc] + rw [hform] + show parseSharesGo (f + 1) ((g / 256).toUInt8 :: + g.toUInt8 :: ((k.length / 256).toUInt8 :: + k.length.toUInt8 :: (k ++ printShares ss))) + = some ((g, k) :: ss) + rw [parseSharesGo_step] + have hg : getU16 ((g / 256).toUInt8 :: g.toUInt8 :: + ((k.length / 256).toUInt8 :: k.length.toUInt8 :: + (k ++ printShares ss))) + = some (g, (k.length / 256).toUInt8 :: + k.length.toUInt8 :: (k ++ printShares ss)) := by + show some (u16 (g / 256).toUInt8 g.toUInt8, _) = _ + rw [u16_be16 g hhead.1] + rw [hg] + simp only [Option.bind_some] + show (getU16 ((k.length / 256).toUInt8 :: + k.length.toUInt8 :: (k ++ printShares ss)) >>= + 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) = some ((g, k) :: ss) + have hk : getU16 ((k.length / 256).toUInt8 :: + k.length.toUInt8 :: (k ++ printShares ss)) + = some (k.length, k ++ printShares ss) := by + show some (u16 (k.length / 256).toUInt8 + k.length.toUInt8, _) = _ + rw [u16_be16 _ (by omega)] + rw [hk] + simp only [Option.bind_some] + show (if k.length = 0 then none + else if ((k ++ printShares ss).take k.length).length + = k.length then + parseSharesGo f ((k ++ printShares ss).drop + k.length) >>= fun ss' => + if g ∈ ss'.map Prod.fst then none + else some ((g, (k ++ printShares ss).take + k.length) :: ss') + else none) = some ((g, k) :: ss) + rw [if_neg (by + intro hcon + cases k with + | nil => exact hhead.2.1 rfl + | cons b bs => simp at hcon), + List.take_left, List.drop_left, if_pos rfl, + ih f htail hnodup' hf'] + show (if g ∈ ss.map Prod.fst then none + else some ((g, k) :: ss)) = some ((g, k) :: ss) + rw [if_neg hnotin] + +/-- Printed key share entries read back, at the top + level. -/ +theorem parseShares_print {ss : List (Nat × List UInt8)} + (hw : ∀ s ∈ ss, s.1 < 65536 ∧ s.2 ≠ [] ∧ + s.2.length ≤ 65535) + (hn : List.Nodup (ss.map Prod.fst)) : + parseShares (printShares ss) = some ss := by + show parseSharesGo ((printShares ss).length + 1) + (printShares ss) = some ss + exact parseSharesGo_print ss _ hw hn (Nat.lt_succ_self _) + +/-- Key share entries a successful read gives print back to + the bytes they were read from, each group fits two + bytes, each key is nonempty and fits two length bytes, + and no group stands twice. -/ +theorem parseSharesGo_inv : + ∀ (f : Nat) (bs : List UInt8) + (ss : List (Nat × List UInt8)), + parseSharesGo f bs = some ss → + printShares ss = bs ∧ + (∀ s ∈ ss, s.1 < 65536 ∧ s.2 ≠ [] ∧ + s.2.length ≤ 65535) ∧ + List.Nodup (ss.map Prod.fst) := by + intro f + induction f with + | zero => + intro bs ss h + simp [parseSharesGo] at h + | succ f ih => + intro bs ss h + cases bs with + | nil => + have h1 : parseSharesGo (f + 1) ([] : List UInt8) + = some [] := rfl + rw [h1] at h + simp only [Option.some.injEq] at h + subst h + exact ⟨rfl, by simp, by simp⟩ + | cons b1 rest => + cases rest with + | nil => simp [parseSharesGo, getU16] at h + | cons b2 rest => + rw [parseSharesGo_step] at h + obtain ⟨⟨g, r1⟩, hg, h⟩ := Option.bind_eq_some_iff.mp h + change (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) = some ss at h + obtain ⟨⟨n, r2⟩, hn, h⟩ := Option.bind_eq_some_iff.mp h + change (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) = some ss at h + obtain ⟨hbs, hglt⟩ := getU16_inv hg + obtain ⟨hr1, hnlt⟩ := getU16_inv hn + by_cases h0 : n = 0 + · rw [if_pos h0] at h + simp at h + · rw [if_neg h0] at h + by_cases hc : (r2.take n).length = n + · rw [if_pos hc] at h + obtain ⟨ss', hrec, h⟩ := Option.bind_eq_some_iff.mp h + obtain ⟨hprint, hprops, hnodup⟩ := ih _ _ hrec + by_cases hd : g ∈ ss'.map Prod.fst + · rw [if_pos hd] at h + simp at h + · rw [if_neg hd] at h + simp only [Option.some.injEq, Prod.mk.injEq] at h + obtain ⟨rfl, rfl⟩ := h + refine ⟨?_, ?_, ?_⟩ + · have htake : (r2.take n).length = n := hc + show ((be16 g ++ (be16 (r2.take n).length ++ + r2.take n)) ++ printShares ss') + = b1 :: b2 :: rest + rw [htake, hprint, hbs, hr1] + simp only [List.append_assoc] + rw [List.take_append_drop] + · intro x hx + simp only [List.mem_cons] at hx + rcases hx with rfl | hx + · exact ⟨hglt, by + intro hcon + change r2.take n = [] at hcon + rw [hcon] at hc + exact h0 hc.symm, by + change (r2.take n).length ≤ 65535 + rw [hc]; omega⟩ + · exact hprops x hx + · have h2 : ((g, r2.take n) :: ss').map Prod.fst + = g :: ss'.map Prod.fst := rfl + rw [h2] + exact List.nodup_cons.mpr ⟨hd, hnodup⟩ + · rw [if_neg hc] at h + simp at h + +/-- Key share entries a successful read gives print back, + at the top level. -/ +theorem parseShares_inv {bs : List UInt8} + {ss : List (Nat × List UInt8)} + (h : parseShares bs = some ss) : + printShares ss = bs ∧ + (∀ s ∈ ss, s.1 < 65536 ∧ s.2 ≠ [] ∧ + s.2.length ≤ 65535) ∧ + List.Nodup (ss.map Prod.fst) := + parseSharesGo_inv _ _ _ h + +/-- A printed key_share value reads back as the + extension. -/ +theorem parseKS_print {ss : List (Nat × List UInt8)} + (hne : ss ≠ []) + (hw : ∀ s ∈ ss, s.1 < 65536 ∧ s.2 ≠ [] ∧ + s.2.length ≤ 65535) + (hnodup : List.Nodup (ss.map Prod.fst)) + (hlen : (printShares ss).length ≤ 65533) : + parseKS (printExtValue (.keyShare ss)) + = some (.keyShare ss) := by + show parseKS (be16 (printShares ss).length ++ + printShares ss) = some (Extension.keyShare ss) + unfold parseKS + rw [getU16_be16 _ (by omega)] + simp only [Option.bind_some] + show (if (printShares ss).length + = (printShares ss).length then + parseShares (printShares ss) >>= fun ss' => + if ss'.isEmpty then none else some (Extension.keyShare ss') + else none) = some (Extension.keyShare ss) + rw [if_pos rfl, parseShares_print hw hnodup] + show (if ss.isEmpty then none else some (Extension.keyShare ss)) + = some (Extension.keyShare ss) + rw [if_neg (by + cases ss with + | nil => exact absurd rfl hne + | cons s ss' => simp)] + +/-- A key_share value a successful read gives is the + printed form of the extension it gives, and the + extension is well formed. -/ +theorem parseKS_inv {v : List UInt8} {e : Extension} + (hv : v.length ≤ 65535) (h : parseKS v = some e) : + ∃ ss, e = .keyShare ss ∧ + printExtValue (.keyShare ss) = v ∧ + ExtWF (.keyShare ss) := by + unfold parseKS at h + obtain ⟨⟨n, rest⟩, hn, h⟩ := Option.bind_eq_some_iff.mp h + change (if rest.length = n then + parseShares rest >>= fun ss => + if ss.isEmpty then none else some (.keyShare ss) + else none) = some e at h + obtain ⟨hrest, hnlt⟩ := getU16_inv hn + by_cases hc : rest.length = n + · rw [if_pos hc] at h + obtain ⟨ss, hrec, h⟩ := Option.bind_eq_some_iff.mp h + by_cases hemp : ss.isEmpty = false + · rw [if_neg (by + intro hcon + rw [hcon] at hemp + simp at hemp)] at h + simp only [Option.some.injEq] at h + subst h + obtain ⟨hprint, hprops, hnodup⟩ := parseShares_inv hrec + have hne : ss ≠ [] := by + cases ss with + | nil => simp at hemp + | cons s' ss' => intro hcon; cases hcon + refine ⟨ss, rfl, ?_, ?_⟩ + · show be16 (printShares ss).length ++ + printShares ss = v + rw [hprint, hc, hrest] + · exact ⟨hne, hprops, hnodup, by + have h2 : (printShares ss).length = rest.length := by + rw [hprint] + have hvlen : v.length = rest.length + 2 := by + rw [hrest]; simp [be16] + omega⟩ + · have hemp2 : ss.isEmpty = true := by + cases h' : ss.isEmpty with + | true => rfl + | false => exact absurd h' hemp + rw [if_pos hemp2] at h + simp at h + · rw [if_neg hc] at h + simp at h + +/-! ## Extension values, dispatched by type -/ + +/-- The type of a well formed extension fits two bytes. -/ +theorem extType_lt {e : Extension} (h : ExtWF e) : + extType e < 65536 := by + rcases e with ⟨es⟩ | ⟨ns⟩ | ⟨vs⟩ | ⟨ss⟩ | ⟨t, v⟩ + · show (0 : Nat) < 65536; omega + · show (16 : Nat) < 65536; omega + · show (43 : Nat) < 65536; omega + · show (51 : Nat) < 65536; omega + · have h' : ¬ (t = 0 ∨ t = 16 ∨ t = 43 ∨ t = 51) ∧ + t < 65536 ∧ v.length ≤ 65535 := h + exact h'.2.1 + +/-- The printed value of a well formed extension fits two + length bytes. -/ +theorem printExtValue_length_le {e : Extension} + (h : ExtWF e) : (printExtValue e).length ≤ 65535 := by + rcases e with ⟨es⟩ | ⟨ns⟩ | ⟨vs⟩ | ⟨ss⟩ | ⟨t, v⟩ + · + have h' : es ≠ [] ∧ + (∀ e ∈ es, e.1 < 256 ∧ e.2.length ≤ 65535 ∧ + (e.1 = 0 → e.2 ≠ [])) ∧ + List.Nodup (es.map Prod.fst) ∧ + (printNameEntries es).length ≤ 65533 := h + show (be16 (printNameEntries es).length ++ + printNameEntries es).length ≤ 65535 + rw [List.length_append] + simp [be16] + omega + · have h' : ns ≠ [] ∧ + (∀ n ∈ ns, n ≠ [] ∧ n.length ≤ 255) ∧ + (printAlpnNames ns).length ≤ 65533 := h + show (be16 (printAlpnNames ns).length ++ + printAlpnNames ns).length ≤ 65535 + rw [List.length_append] + simp [be16] + omega + · have h' : vs ≠ [] ∧ (∀ v ∈ vs, v < 65536) ∧ + vs.length ≤ 127 := h + show ((printPairs vs).length.toUInt8 :: + printPairs vs).length ≤ 65535 + rw [List.length_cons, printPairs_length] + omega + · have h' : ss ≠ [] ∧ + (∀ s ∈ ss, s.1 < 65536 ∧ s.2 ≠ [] ∧ + s.2.length ≤ 65535) ∧ + List.Nodup (ss.map Prod.fst) ∧ + (printShares ss).length ≤ 65533 := h + show (be16 (printShares ss).length ++ + printShares ss).length ≤ 65535 + rw [List.length_append] + simp [be16] + omega + · have h' : ¬ (t = 0 ∨ t = 16 ∨ t = 43 ∨ t = 51) ∧ + t < 65536 ∧ v.length ≤ 65535 := h + exact h'.2.2 + +/-- A printed extension value reads back as the extension, + at its own type. -/ +theorem parseExtValue_printExtValue (e : Extension) + (h : ExtWF e) : + parseExtValue (extType e) (printExtValue e) = some e := by + rcases e with ⟨es⟩ | ⟨ns⟩ | ⟨vs⟩ | ⟨ss⟩ | ⟨t, v⟩ + · + have h' : es ≠ [] ∧ + (∀ e ∈ es, e.1 < 256 ∧ e.2.length ≤ 65535 ∧ + (e.1 = 0 → e.2 ≠ [])) ∧ + List.Nodup (es.map Prod.fst) ∧ + (printNameEntries es).length ≤ 65533 := h + show parseExtValue 0 (printExtValue + (Extension.serverName es)) = some (Extension.serverName es) + unfold parseExtValue + rw [if_pos rfl] + exact parseSNI_print h'.1 h'.2.1 h'.2.2.1 h'.2.2.2 + · have h' : ns ≠ [] ∧ + (∀ n ∈ ns, n ≠ [] ∧ n.length ≤ 255) ∧ + (printAlpnNames ns).length ≤ 65533 := h + show parseExtValue 16 (printExtValue + (Extension.alpn ns)) = some (Extension.alpn ns) + unfold parseExtValue + rw [if_neg (by decide), if_pos rfl] + exact parseALPN_print h'.1 h'.2.1 h'.2.2 + · have h' : vs ≠ [] ∧ (∀ v ∈ vs, v < 65536) ∧ + vs.length ≤ 127 := h + show parseExtValue 43 (printExtValue + (Extension.supportedVersions vs)) + = some (Extension.supportedVersions vs) + unfold parseExtValue + rw [if_neg (by decide), if_neg (by decide), if_pos rfl] + exact parseSV_print h'.1 h'.2.1 h'.2.2 + · have h' : ss ≠ [] ∧ + (∀ s ∈ ss, s.1 < 65536 ∧ s.2 ≠ [] ∧ + s.2.length ≤ 65535) ∧ + List.Nodup (ss.map Prod.fst) ∧ + (printShares ss).length ≤ 65533 := h + show parseExtValue 51 (printExtValue + (Extension.keyShare ss)) = some (Extension.keyShare ss) + unfold parseExtValue + rw [if_neg (by decide), if_neg (by decide), + if_neg (by decide), if_pos rfl] + exact parseKS_print h'.1 h'.2.1 h'.2.2.1 h'.2.2.2 + · have h' : ¬ (t = 0 ∨ t = 16 ∨ t = 43 ∨ t = 51) ∧ + t < 65536 ∧ v.length ≤ 65535 := h + have hn := not_or.mp h'.1 + have hn2 := not_or.mp hn.2 + have hn3 := not_or.mp hn2.2 + show parseExtValue t (printExtValue + (Extension.opaque t v)) = some (Extension.opaque t v) + unfold parseExtValue + rw [if_neg hn.1, if_neg hn2.1, if_neg hn3.1, + if_neg hn3.2] + rfl + +/-- An extension value a successful read gives is the + printed form of the extension it gives, the extension + carries the type it was read under, and the extension + is well formed. -/ +theorem parseExtValue_inv {t : Nat} {v : List UInt8} + {e : Extension} + (ht : t < 65536) (hv : v.length ≤ 65535) + (h : parseExtValue t v = some e) : + extType e = t ∧ printExtValue e = v ∧ ExtWF e := by + unfold parseExtValue at h + by_cases h0 : t = 0 + · rw [if_pos h0] at h + obtain ⟨es, he, hprint, hwf⟩ := parseSNI_inv hv h + refine ⟨?_, ?_, ?_⟩ + · rw [he]; exact h0.symm + · rw [he]; exact hprint + · rw [he]; exact hwf + · rw [if_neg h0] at h + by_cases h16 : t = 16 + · rw [if_pos h16] at h + obtain ⟨ns, he, hprint, hwf⟩ := parseALPN_inv hv h + refine ⟨?_, ?_, ?_⟩ + · rw [he]; exact h16.symm + · rw [he]; exact hprint + · rw [he]; exact hwf + · rw [if_neg h16] at h + by_cases h43 : t = 43 + · rw [if_pos h43] at h + obtain ⟨vs, he, hprint, hwf⟩ := parseSV_inv h + refine ⟨?_, ?_, ?_⟩ + · rw [he]; exact h43.symm + · rw [he]; exact hprint + · rw [he]; exact hwf + · rw [if_neg h43] at h + by_cases h51 : t = 51 + · rw [if_pos h51] at h + obtain ⟨ss, he, hprint, hwf⟩ := parseKS_inv hv h + refine ⟨?_, ?_, ?_⟩ + · rw [he]; exact h51.symm + · rw [he]; exact hprint + · rw [he]; exact hwf + · rw [if_neg h51] at h + simp only [Option.some.injEq] at h + subst h + refine ⟨rfl, rfl, ?_⟩ + exact ⟨fun hc => by + rcases hc with rfl | rfl | rfl | rfl + · exact h0 rfl + · exact h16 rfl + · exact h43 rfl + · exact h51 rfl, ht, hv⟩ + +/-! ## The extensions block -/ + +/-- The printed length of one extension: four bytes of type + and length, then the value. -/ +theorem printExt_length (e : Extension) : + (printExt e).length = (printExtValue e).length + 4 := by + show (be16 (extType e) ++ be16 (printExtValue e).length ++ + printExtValue e).length = _ + rw [List.length_append, List.length_append] + have h1 : (be16 (extType e)).length = 2 := rfl + have h2 : (be16 (printExtValue e).length).length = 2 := rfl + omega + +/-- One step of the extension reader, stated for + rewriting. -/ +theorem parseExtsGo_step (f : Nat) (x y : UInt8) + (rest : List UInt8) : + parseExtsGo (f + 1) (x :: y :: rest) = + getU16 (x :: y :: rest) >>= 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 := rfl + +/-- Printed extensions read back as the extensions. -/ +theorem parseExtsGo_print : + ∀ (es : List Extension) (fuel : Nat), + (∀ e ∈ es, ExtWF e) → + List.Nodup (es.map extType) → + (printExts es).length < fuel → + parseExtsGo fuel (printExts es) = some es := by + intro es + induction es with + | nil => + intro fuel _ _ hf + obtain ⟨f, rfl⟩ : ∃ f, fuel = f + 1 := ⟨fuel - 1, by omega⟩ + rfl + | cons e es ih => + intro fuel hw hnodup hf + have hwe : ExtWF e := hw e (by simp) + have htail : ∀ x ∈ es, ExtWF x := + fun x hx => hw x (List.mem_cons_of_mem e hx) + have hnodup' : List.Nodup (es.map extType) := by + have h2 : (e :: es).map extType + = extType e :: es.map extType := rfl + rw [h2] at hnodup + exact (List.nodup_cons.mp hnodup).2 + have hnotin : extType e ∉ es.map extType := by + have h2 : (e :: es).map extType + = extType e :: es.map extType := rfl + rw [h2] at hnodup + exact (List.nodup_cons.mp hnodup).1 + obtain ⟨f, rfl⟩ : ∃ f, fuel = f + 1 := ⟨fuel - 1, by omega⟩ + have hf' : (printExts es).length < f := by + have hflen : (printExts (e :: es)).length + = (printExt e).length + (printExts es).length := by + show ((printExt e) ++ printExts es).length = _ + rw [List.length_append] + have h2 := printExt_length e + omega + show parseExtsGo (f + 1) + ((be16 (extType e) ++ + (be16 (printExtValue e).length ++ + printExtValue e)) ++ printExts es) + = some (e :: es) + have hform : (be16 (extType e) ++ + (be16 (printExtValue e).length ++ + printExtValue e)) ++ printExts es + = (extType e / 256).toUInt8 :: (extType e).toUInt8 :: + ((printExtValue e).length / 256).toUInt8 :: + (printExtValue e).length.toUInt8 :: + (printExtValue e ++ printExts es) := by + simp only [be16, ← List.append_assoc, List.cons_append, + List.nil_append] + rw [hform, parseExtsGo_step] + have hg : getU16 ((extType e / 256).toUInt8 :: + (extType e).toUInt8 :: + ((printExtValue e).length / 256).toUInt8 :: + (printExtValue e).length.toUInt8 :: + (printExtValue e ++ printExts es)) + = some (extType e, + ((printExtValue e).length / 256).toUInt8 :: + (printExtValue e).length.toUInt8 :: + (printExtValue e ++ printExts es)) := by + show some (u16 (extType e / 256).toUInt8 + (extType e).toUInt8, _) = _ + rw [u16_be16 _ (extType_lt hwe)] + rw [hg] + simp only [Option.bind_some] + show (getU16 (((printExtValue e).length / 256).toUInt8 :: + (printExtValue e).length.toUInt8 :: + (printExtValue e ++ printExts es)) >>= + fun (n, r2) => + if (r2.take n).length = n then + parseExtValue (extType e) (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) = some (e :: es) + have hk : getU16 (((printExtValue e).length / 256).toUInt8 :: + (printExtValue e).length.toUInt8 :: + (printExtValue e ++ printExts es)) + = some ((printExtValue e).length, + printExtValue e ++ printExts es) := by + show some (u16 ((printExtValue e).length / 256).toUInt8 + (printExtValue e).length.toUInt8, _) = _ + rw [u16_be16 _ (by + have h2 := printExtValue_length_le hwe + omega)] + rw [hk] + simp only [Option.bind_some] + show (if ((printExtValue e ++ printExts es).take + (printExtValue e).length).length + = (printExtValue e).length then + parseExtValue (extType e) + ((printExtValue e ++ printExts es).take + (printExtValue e).length) >>= fun e' => + parseExtsGo f ((printExtValue e ++ printExts es).drop + (printExtValue e).length) >>= fun es' => + if extType e' ∈ es'.map extType then none + else some (e' :: es') + else none) = some (e :: es) + rw [List.take_left, List.drop_left, if_pos rfl, + parseExtValue_printExtValue e hwe] + show (parseExtsGo f (printExts es) >>= fun es' => + if extType e ∈ es'.map extType then none + else some (e :: es')) = some (e :: es) + rw [ih f htail hnodup' hf'] + show (if extType e ∈ es.map extType then none + else some (e :: es)) = some (e :: es) + rw [if_neg hnotin] + +/-- Printed extensions read back, at the top level. -/ +theorem parseExts_print {es : List Extension} + (hw : ∀ e ∈ es, ExtWF e) + (hn : List.Nodup (es.map extType)) : + parseExts (printExts es) = some es := by + show parseExtsGo ((printExts es).length + 1) + (printExts es) = some es + exact parseExtsGo_print es _ hw hn (Nat.lt_succ_self _) + +/-- Extensions a successful read gives print back to the + bytes they were read from, each extension is well + formed, and no type stands twice. -/ +theorem parseExtsGo_inv : + ∀ (f : Nat) (bs : List UInt8) (es : List Extension), + parseExtsGo f bs = some es → + printExts es = bs ∧ + (∀ e ∈ es, ExtWF e) ∧ + List.Nodup (es.map extType) := by + intro f + induction f with + | zero => + intro bs es h + simp [parseExtsGo] at h + | succ f ih => + intro bs es h + cases bs with + | nil => + have h1 : parseExtsGo (f + 1) ([] : List UInt8) + = some [] := rfl + rw [h1] at h + simp only [Option.some.injEq] at h + subst h + exact ⟨rfl, by simp, by simp⟩ + | cons b1 rest => + cases rest with + | nil => + have h1 : parseExtsGo (f + 1) [b1] = none := rfl + rw [h1] at h + simp at h + | cons b2 rest => + rw [parseExtsGo_step] at h + obtain ⟨⟨t, r1⟩, ht, h⟩ := Option.bind_eq_some_iff.mp h + change (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) = some es at h + obtain ⟨⟨n, r2⟩, hn, h⟩ := Option.bind_eq_some_iff.mp h + change (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) = some es at h + obtain ⟨hbs, htlt⟩ := getU16_inv ht + obtain ⟨hr1, hnlt⟩ := getU16_inv hn + by_cases hc : (r2.take n).length = n + · rw [if_pos hc] at h + obtain ⟨e, hev, h⟩ := Option.bind_eq_some_iff.mp h + obtain ⟨es', hrec, h⟩ := Option.bind_eq_some_iff.mp h + obtain ⟨hprint, hprops, hnodup⟩ := ih _ _ hrec + obtain ⟨htype, hvalue, hwe⟩ := parseExtValue_inv htlt + (by rw [hc]; omega) hev + by_cases hd : extType e ∈ es'.map extType + · rw [if_pos hd] at h + simp at h + · rw [if_neg hd] at h + simp only [Option.some.injEq] at h + subst h + refine ⟨?_, ?_, ?_⟩ + · show printExts (e :: es') = b1 :: b2 :: rest + have htake : (r2.take n).length = n := hc + show (printExt e ++ printExts es') + = b1 :: b2 :: rest + show ((be16 (extType e) ++ + be16 (printExtValue e).length ++ + printExtValue e) ++ printExts es') + = b1 :: b2 :: rest + rw [htype, hvalue, htake, hprint, hbs, hr1] + simp only [List.append_assoc] + rw [List.take_append_drop] + · intro x hx + simp only [List.mem_cons] at hx + rcases hx with rfl | hx + · exact hwe + · exact hprops x hx + · have h2 : (e :: es').map extType + = extType e :: es'.map extType := rfl + rw [h2] + exact List.nodup_cons.mpr ⟨hd, hnodup⟩ + · rw [if_neg hc] at h + simp at h + +/-- Extensions a successful read gives print back, at the + top level. -/ +theorem parseExts_inv {bs : List UInt8} + {es : List Extension} + (h : parseExts bs = some es) : + printExts es = bs ∧ + (∀ e ∈ es, ExtWF e) ∧ + List.Nodup (es.map extType) := + parseExtsGo_inv _ _ _ h + +/-- The value a successful one byte read gives fits in a + byte. -/ +theorem getU8_lt {bs : List UInt8} {n : Nat} {r : List UInt8} + (h : getU8 bs = some (n, r)) : n < 256 := by + cases bs with + | nil => simp [getU8] at h + | cons b r' => + have hstep : getU8 (b :: r') = some (b.toNat, r') := rfl + rw [hstep] at h + simp only [Option.some.injEq, Prod.mk.injEq] at h + obtain ⟨rfl, rfl⟩ := h + exact toNat_lt b + +/-- A block read at exactly its own length gives the block + and nothing after it. -/ +theorem getBytes_self (bs : List UInt8) : + getBytes bs.length bs = some (bs, []) := by + unfold getBytes + have ht : bs.take bs.length = bs := List.take_length + have hd : bs.drop bs.length = [] := List.drop_length + rw [ht, hd, if_pos rfl] + +/-! ## The body fields -/ + +/-- The printed body fields read back as the hello. -/ +theorem parseBodyFields_print (m : Message) (hw : WF m) : + parseBodyFields (printBodyFields m.hello) = some m.hello := by + obtain ⟨_, hver, hrand, hsess, hsuites_ne, hsuites_lt, + hsuites_len, hcomp_ne, hcomp0, hcomp_len, hext_wf, + hnodup, hext_len, _⟩ := hw + have hsuites_len1 : 1 ≤ m.hello.cipherSuites.length := by + cases hcs : m.hello.cipherSuites with + | nil => exact absurd hcs hsuites_ne + | cons v vs' => simp + have hcomp_len1 : 1 ≤ m.hello.compressionMethods.length := by + cases hcc : m.hello.compressionMethods with + | nil => exact absurd hcc hcomp_ne + | cons c cs' => simp + have hsb : (m.hello.sessionId.length.toUInt8).toNat + = m.hello.sessionId.length := by + rw [toUInt8_toNat] + exact Nat.mod_eq_of_lt (by omega) + have hcb : (m.hello.compressionMethods.length.toUInt8).toNat + = m.hello.compressionMethods.length := by + rw [toUInt8_toNat] + exact Nat.mod_eq_of_lt (by omega) + have hguard : (printPairs m.hello.cipherSuites).length % 2 = 0 ∧ + 2 ≤ (printPairs m.hello.cipherSuites).length := by + have h2 := printPairs_length m.hello.cipherSuites + exact ⟨by omega, by omega⟩ + unfold parseBodyFields printBodyFields + simp only [List.append_assoc] + rw [getU16_be16 _ hver] + simp only [Option.bind_eq_bind, Option.bind_some] + rw [getBytes_app hrand] + simp only [Option.bind_eq_bind, Option.bind_some] + rw [List.cons_append, getU8_cons] + simp only [Option.bind_eq_bind, Option.bind_some] + rw [hsb, if_pos hsess, getBytes_app rfl] + simp only [Option.bind_eq_bind, Option.bind_some] + rw [getU16_be16 _ (by + have h2 := printPairs_length m.hello.cipherSuites + omega)] + simp only [Option.bind_eq_bind, Option.bind_some] + rw [if_pos hguard, getBytes_app rfl] + simp only [Option.bind_eq_bind, Option.bind_some] + rw [parsePairs_printPairs hsuites_lt] + simp only [Option.bind_eq_bind, Option.bind_some] + rw [List.cons_append, getU8_cons] + simp only [Option.bind_eq_bind, Option.bind_some] + rw [hcb, if_pos hcomp_len1, getBytes_app rfl] + simp only [Option.bind_eq_bind, Option.bind_some] + rw [if_pos hcomp0, + getU16_be16 _ (by omega)] + simp only [Option.bind_eq_bind, Option.bind_some] + rw [getBytes_self] + simp only [Option.bind_eq_bind, Option.bind_some] + show (parseExts (printExts m.hello.extensions) >>= fun exts => + some ⟨m.hello.legacyVersion, m.hello.random, + m.hello.sessionId, m.hello.cipherSuites, + m.hello.compressionMethods, exts⟩) = some m.hello + rw [parseExts_print hext_wf hnodup] + simp only [Option.bind_eq_bind, Option.bind_some] + + + +/-- A parsed hello prints back to the input bytes, and every + field satisfies the well formedness bounds. -/ +theorem parseBodyFields_inv {bs : List UInt8} {h : Hello} + (hparse : parseBodyFields bs = some h) : + printBodyFields h = bs ∧ + h.legacyVersion < 65536 ∧ h.random.length = 32 ∧ + h.sessionId.length ≤ 32 ∧ + h.cipherSuites ≠ [] ∧ + (∀ v ∈ h.cipherSuites, v < 65536) ∧ + h.cipherSuites.length ≤ 32767 ∧ + h.compressionMethods ≠ [] ∧ + (0 : UInt8) ∈ h.compressionMethods ∧ + h.compressionMethods.length ≤ 255 ∧ + (∀ e ∈ h.extensions, ExtWF e) ∧ + List.Nodup (h.extensions.map extType) ∧ + (printExts h.extensions).length ≤ 65535 := by + unfold parseBodyFields at hparse + simp only [Option.bind_eq_bind] at hparse + obtain ⟨⟨ver, r1⟩, s1, hparse⟩ := + Option.bind_eq_some_iff.mp hparse + obtain ⟨⟨rand, r2⟩, s2, hparse⟩ := + Option.bind_eq_some_iff.mp hparse + obtain ⟨⟨slen, r3⟩, s3, hparse⟩ := + Option.bind_eq_some_iff.mp hparse + by_cases hs : slen ≤ 32 + · rw [if_pos hs] at hparse + obtain ⟨⟨sess, r4⟩, s4, hparse⟩ := + Option.bind_eq_some_iff.mp hparse + obtain ⟨⟨clen, r5⟩, s5, hparse⟩ := + Option.bind_eq_some_iff.mp hparse + by_cases hg : clen % 2 = 0 ∧ 2 ≤ clen + · rw [if_pos hg] at hparse + obtain ⟨⟨cbytes, r6⟩, s6, hparse⟩ := + Option.bind_eq_some_iff.mp hparse + obtain ⟨suites, s7, hparse⟩ := + Option.bind_eq_some_iff.mp hparse + obtain ⟨⟨mlen, r7⟩, s8, hparse⟩ := + Option.bind_eq_some_iff.mp hparse + by_cases hm : 1 ≤ mlen + · rw [if_pos hm] at hparse + obtain ⟨⟨comps, r8⟩, s9, hparse⟩ := + Option.bind_eq_some_iff.mp hparse + by_cases h0 : (0 : UInt8) ∈ comps + · rw [if_pos h0] at hparse + obtain ⟨⟨elen, r9⟩, s10, hparse⟩ := + Option.bind_eq_some_iff.mp hparse + obtain ⟨⟨ebytes, r10⟩, s11, hparse⟩ := + Option.bind_eq_some_iff.mp hparse + by_cases hr : r10 = [] + · rw [if_pos hr] at hparse + obtain ⟨exts, s12, hparse⟩ := + Option.bind_eq_some_iff.mp hparse + rw [Option.some.injEq] at hparse + subst hparse + have hbs : bs = be16 ver ++ r1 := + (getU16_inv s1).1 + have hver : ver < 65536 := (getU16_inv s1).2 + have hrand : rand.length = 32 := + (getBytes_inv s2).1 + have hr1 : r1 = rand ++ r2 := + (getBytes_inv s2).2 + have hr2 : r2 = slen.toUInt8 :: r3 := + getU8_inv s3 + have hsesslen : sess.length = slen := + (getBytes_inv s4).1 + have hr3 : r3 = sess ++ r4 := + (getBytes_inv s4).2 + have hr4 : r4 = be16 clen ++ r5 := + (getU16_inv s5).1 + have hclen_lt : clen < 65536 := + (getU16_inv s5).2 + have hcbyteslen : cbytes.length = clen := + (getBytes_inv s6).1 + have hr5 : r5 = cbytes ++ r6 := + (getBytes_inv s6).2 + have hpp : printPairs suites = cbytes := + (parsePairs_inv s7).1 + have hsuites_lt : ∀ v ∈ suites, v < 65536 := + (parsePairs_inv s7).2 + have hplen : cbytes.length + = 2 * suites.length := + parsePairs_length s7 + have hr6 : r6 = mlen.toUInt8 :: r7 := + getU8_inv s8 + have hmlen_lt : mlen < 256 := getU8_lt s8 + have hcomplen : comps.length = mlen := + (getBytes_inv s9).1 + have hr7 : r7 = comps ++ r8 := + (getBytes_inv s9).2 + have hr8 : r8 = be16 elen ++ r9 := + (getU16_inv s10).1 + have helen_lt : elen < 65536 := + (getU16_inv s10).2 + have hebyteslen : ebytes.length = elen := + (getBytes_inv s11).1 + have hr9 : r9 = ebytes ++ r10 := + (getBytes_inv s11).2 + have hpe : printExts exts = ebytes := + (parseExts_inv s12).1 + have hext_wf : ∀ e ∈ exts, ExtWF e := + (parseExts_inv s12).2.1 + have hnodup : (exts.map extType).Nodup := + (parseExts_inv s12).2.2 + have hsess_le : sess.length ≤ 32 := by omega + have hsuites_ne : suites ≠ [] := by + intro hcon + rw [hcon] at hplen + simp at hplen + have hz : cbytes.length = 0 := by + simp [hplen] + omega + have hsuites_len : suites.length ≤ 32767 := by + omega + have hcomp_ne : comps ≠ [] := by + intro hcon + rw [hcon] at hcomplen + simp at hcomplen + omega + have hcomp_len : comps.length ≤ 255 := by + omega + have hext_len : (printExts exts).length + ≤ 65535 := by + rw [hpe, hebyteslen] + omega + have hprint : printBodyFields + ⟨ver, rand, sess, suites, comps, exts⟩ + = bs := by + show (be16 ver ++ rand ++ + (sess.length.toUInt8 :: sess) ++ + (be16 (printPairs suites).length ++ + printPairs suites) ++ + (comps.length.toUInt8 :: comps) ++ + (be16 (printExts exts).length ++ + printExts exts)) = bs + rw [hsesslen, hcomplen, hpp, hcbyteslen, + hpe, hebyteslen, hbs, hr1, hr2, hr3, hr4, + hr5, hr6, hr7, hr8, hr9, hr] + simp only [List.append_assoc, List.cons_append, + List.append_nil] + exact ⟨hprint, hver, hrand, hsess_le, + hsuites_ne, hsuites_lt, hsuites_len, hcomp_ne, + h0, hcomp_len, hext_wf, hnodup, hext_len⟩ + · rw [if_neg hr] at hparse + simp at hparse + · rw [if_neg h0] at hparse + simp at hparse + · rw [if_neg hm] at hparse + simp at hparse + · rw [if_neg hg] at hparse + simp at hparse + · rw [if_neg hs] at hparse + simp at hparse + +/-! ## The handshake message and the record -/ + +/-- The printed handshake message is four bytes longer than + the printed body fields. -/ +theorem printBody_length (h : Hello) : + (printBody h).length = (printBodyFields h).length + 4 := by + simp [printBody, be24] + +/-- The printed handshake message reads back as the hello. -/ +theorem parseBody_print (m : Message) (hw : WF m) : + parseBody (printBody m.hello) = some m.hello := by + have hwf : WF m := hw + obtain ⟨_, _, _, _, _, _, _, _, _, _, _, _, _, + hflen⟩ := hw + unfold parseBody printBody + rw [getU8_cons] + simp only [Option.bind_eq_bind, Option.bind_some] + rw [if_pos (by decide : ((1 : UInt8).toNat = 1)), + getU24_be24 _ (by omega)] + simp only [Option.bind_eq_bind, Option.bind_some] + rw [getBytes_self] + simp only [Option.bind_eq_bind, Option.bind_some] + exact parseBodyFields_print m hwf + +/-- A parsed handshake message prints back to the input + bytes, and every field satisfies the bounds. -/ +theorem parseBody_inv {body : List UInt8} {h : Hello} + (hparse : parseBody body = some h) : + printBody h = body ∧ + h.legacyVersion < 65536 ∧ h.random.length = 32 ∧ + h.sessionId.length ≤ 32 ∧ + h.cipherSuites ≠ [] ∧ + (∀ v ∈ h.cipherSuites, v < 65536) ∧ + h.cipherSuites.length ≤ 32767 ∧ + h.compressionMethods ≠ [] ∧ + (0 : UInt8) ∈ h.compressionMethods ∧ + h.compressionMethods.length ≤ 255 ∧ + (∀ e ∈ h.extensions, ExtWF e) ∧ + List.Nodup (h.extensions.map extType) ∧ + (printExts h.extensions).length ≤ 65535 := by + unfold parseBody at hparse + simp only [Option.bind_eq_bind] at hparse + obtain ⟨⟨htype, r1⟩, s1, hparse⟩ := + Option.bind_eq_some_iff.mp hparse + by_cases ht : htype = 1 + · rw [if_pos ht] at hparse + obtain ⟨⟨hlen, r2⟩, s2, hparse⟩ := + Option.bind_eq_some_iff.mp hparse + obtain ⟨⟨fbs, r3⟩, s3, hparse⟩ := + Option.bind_eq_some_iff.mp hparse + by_cases hr : r3 = [] + · rw [if_pos hr] at hparse + have hfi := parseBodyFields_inv hparse + have hbody1 : body = htype.toUInt8 :: r1 := + getU8_inv s1 + have hbyte : htype.toUInt8 = (1 : UInt8) := by + rw [ht] + decide + have hr1 : r1 = be24 hlen ++ r2 := + (getU24_inv s2).1 + have hfbs : fbs.length = hlen := + (getBytes_inv s3).1 + have hr2 : r2 = fbs ++ r3 := (getBytes_inv s3).2 + have hprint : printBody h = body := by + show ((1 : UInt8) :: (be24 (printBodyFields h).length + ++ printBodyFields h)) = body + rw [hfi.1, hfbs, hbody1, hbyte, hr1, hr2, hr] + simp only [List.append_nil] + exact ⟨hprint, hfi.2⟩ + · rw [if_neg hr] at hparse + simp at hparse + · rw [if_neg ht] at hparse + simp at hparse + +/-- The whole printed message reads back as the message. -/ +theorem parse_print (m : Message) (hw : WF m) : + parse (print m) = some m := by + have hwf : WF m := hw + obtain ⟨hrv, _, _, _, _, _, _, _, _, _, _, _, _, + hflen⟩ := hw + have hblt : (printBody m.hello).length < 65536 := by + rw [printBody_length] + omega + unfold parse print + rw [getU8_cons] + simp only [Option.bind_eq_bind, Option.bind_some] + rw [if_pos (by decide : ((22 : UInt8).toNat = 22)), + getU16_be16 _ hrv] + simp only [Option.bind_eq_bind, Option.bind_some] + rw [getU16_be16 _ hblt] + simp only [Option.bind_eq_bind, Option.bind_some] + rw [getBytes_self] + simp only [Option.bind_eq_bind, Option.bind_some] + show (Option.map (fun h => ⟨m.recordVersion, h⟩) + (parseBody (printBody m.hello))) = some m + rw [parseBody_print m hwf] + simp only [Option.map_some] + +/-- A parsed message prints back to the input bytes, and the + message is well formed. -/ +theorem print_parse {bs : List UInt8} {m : Message} + (hparse : parse bs = some m) : + print m = bs ∧ WF m := by + unfold parse at hparse + simp only [Option.bind_eq_bind] at hparse + obtain ⟨⟨ct, r1⟩, s1, hparse⟩ := + Option.bind_eq_some_iff.mp hparse + by_cases hct : ct = 22 + · rw [if_pos hct] at hparse + obtain ⟨⟨rv, r2⟩, s2, hparse⟩ := + Option.bind_eq_some_iff.mp hparse + obtain ⟨⟨rlen, r3⟩, s3, hparse⟩ := + Option.bind_eq_some_iff.mp hparse + obtain ⟨⟨body, r4⟩, s4, hparse⟩ := + Option.bind_eq_some_iff.mp hparse + by_cases hr : r4 = [] + · rw [if_pos hr] at hparse + cases hpb : parseBody body with + | none => + rw [hpb] at hparse + simp at hparse + | some hh => + rw [hpb] at hparse + simp only [Option.map_some, Option.some.injEq] + at hparse + subst hparse + obtain ⟨hbody_eq, hver, hrand, hsess, hsne, hslt, + hslen, hcne, hc0, hclen, hewf, hnod, helen⟩ := + parseBody_inv hpb + have hbs1 : bs = ct.toUInt8 :: r1 := getU8_inv s1 + have hctb : ct.toUInt8 = (22 : UInt8) := by + rw [hct] + decide + have hr1 : r1 = be16 rv ++ r2 := + (getU16_inv s2).1 + have hrv : rv < 65536 := (getU16_inv s2).2 + have hr2 : r2 = be16 rlen ++ r3 := + (getU16_inv s3).1 + have hrlen : rlen < 65536 := (getU16_inv s3).2 + have hbodylen : body.length = rlen := + (getBytes_inv s4).1 + have hr3 : r3 = body ++ r4 := + (getBytes_inv s4).2 + have hflen : (printBodyFields hh).length + ≤ 65531 := by + have h1 := printBody_length hh + rw [hbody_eq] at h1 + omega + have hprint : print ⟨rv, hh⟩ = bs := by + show ((22 : UInt8) :: (be16 rv ++ + (be16 (printBody hh).length ++ printBody hh))) + = bs + rw [hbody_eq, hbodylen, hbs1, hctb, hr1, hr2, + hr3, hr] + simp only [List.append_nil] + exact ⟨hprint, hrv, hver, hrand, hsess, hsne, + hslt, hslen, hcne, hc0, hclen, hewf, hnod, helen, + hflen⟩ + · rw [if_neg hr] at hparse + simp at hparse + · rw [if_neg hct] at hparse + simp at hparse diff --git a/Proofs/SpecProofs.lean b/Proofs/SpecProofs.lean new file mode 100644 index 0000000..bbaf935 --- /dev/null +++ b/Proofs/SpecProofs.lean @@ -0,0 +1,154 @@ +/- + Proofs of the statements in `Spec.lean`, under the same names. + + The two round trips are the theorems proved in + `Proofs/RoundTrip.lean`. The examples are single inputs, checked + in the kernel with `decide +kernel`: no native evaluation, which + the bar forbids. +-/ + +import ClientHello +import Proofs.RoundTrip + +open ClientHello + +theorem Spec.parse_print (m : Message) (hw : WF m) : + parse (print m) = some m := + ClientHello.Proofs.parse_print m hw + +theorem Spec.print_parse {bs : List UInt8} {m : Message} + (hparse : parse bs = some m) : + print m = bs ∧ WF m := + ClientHello.Proofs.print_parse hparse + + +theorem Spec.accepts_empty_extensions : + (parse ([22, 3, 1, 0, 47, 1, 0, 0, 43, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 0] : List UInt8)).map print = + some ([22, 3, 1, 0, 47, 1, 0, 0, 43, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 0] : List UInt8) := by + decide +kernel + + +theorem Spec.accepts_supported_versions : + (parse ([22, 3, 1, 0, 56, 1, 0, 0, 52, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 9, 0, 43, 0, 5, 4, 3, 4, 3, 3] : List UInt8)).map print = + some ([22, 3, 1, 0, 56, 1, 0, 0, 52, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 9, 0, 43, 0, 5, 4, 3, 4, 3, 3] : List UInt8) := by + decide +kernel + + +theorem Spec.rejects_empty : + (parse ([] : List UInt8)).isSome = false := by + decide +kernel + + +theorem Spec.rejects_short_header : + (parse ([22, 3] : List UInt8)).isSome = false := by + decide +kernel + + +theorem Spec.rejects_record_length_zero : + (parse ([22, 3, 1, 0, 0] : List UInt8)).isSome = false := by + decide +kernel + + +theorem Spec.rejects_content_type : + (parse ([23, 3, 1, 0, 0] : List UInt8)).isSome = false := by + decide +kernel + + +theorem Spec.rejects_record_length_longer : + (parse ([22, 3, 1, 0, 10, 1, 0, 0, 0] : List UInt8)).isSome = false := by + decide +kernel + + +theorem Spec.rejects_trailing_bytes : + (parse ([22, 3, 1, 0, 47, 1, 0, 0, 43, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 0, 0] : List UInt8)).isSome = false := by + decide +kernel + + +theorem Spec.rejects_handshake_type : + (parse ([22, 3, 1, 0, 4, 2, 0, 0, 0] : List UInt8)).isSome = false := by + decide +kernel + + +theorem Spec.rejects_handshake_length : + (parse ([22, 3, 1, 0, 47, 1, 0, 0, 44, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 0] : List UInt8)).isSome = false := by + decide +kernel + + +theorem Spec.rejects_missing_extensions : + (parse ([22, 3, 1, 0, 45, 1, 0, 0, 41, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0] : List UInt8)).isSome = false := by + decide +kernel + + +theorem Spec.rejects_session_id_33 : + (parse ([22, 3, 1, 0, 39, 1, 0, 0, 35, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 33] : List UInt8)).isSome = false := by + decide +kernel + + +theorem Spec.rejects_odd_cipher_suites : + (parse ([22, 3, 1, 0, 41, 1, 0, 0, 37, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 3] : List UInt8)).isSome = false := by + decide +kernel + + +theorem Spec.rejects_empty_cipher_suites : + (parse ([22, 3, 1, 0, 41, 1, 0, 0, 37, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 0] : List UInt8)).isSome = false := by + decide +kernel + + +theorem Spec.rejects_compression_without_null : + (parse ([22, 3, 1, 0, 45, 1, 0, 0, 41, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 1] : List UInt8)).isSome = false := by + decide +kernel + + +theorem Spec.rejects_empty_compression : + (parse ([22, 3, 1, 0, 44, 1, 0, 0, 40, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 0] : List UInt8)).isSome = false := by + decide +kernel + + +theorem Spec.rejects_duplicate_extension : + (parse ([22, 3, 1, 0, 61, 1, 0, 0, 57, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 14, 0, 43, 0, 3, 2, 3, 4, 0, 43, 0, 3, 2, 3, 3] : List UInt8)).isSome = false := by + decide +kernel + + +theorem Spec.rejects_extension_overrun : + (parse ([22, 3, 1, 0, 54, 1, 0, 0, 50, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 7, 0, 0, 0, 10, 2, 3, 4] : List UInt8)).isSome = false := by + decide +kernel + + +theorem Spec.rejects_duplicate_key_share_group : + (parse ([22, 3, 1, 0, 63, 1, 0, 0, 59, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 16, 0, 51, 0, 12, 0, 10, 0, 29, 0, 1, 1, 0, 29, 0, 1, 2] : List UInt8)).isSome = false := by + decide +kernel + + +theorem Spec.rejects_key_share_empty_key : + (parse ([22, 3, 1, 0, 57, 1, 0, 0, 53, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 10, 0, 51, 0, 6, 0, 4, 0, 29, 0, 0] : List UInt8)).isSome = false := by + decide +kernel + + +theorem Spec.rejects_key_share_empty_list : + (parse ([22, 3, 1, 0, 53, 1, 0, 0, 49, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 6, 0, 51, 0, 2, 0, 0] : List UInt8)).isSome = false := by + decide +kernel + + +theorem Spec.rejects_supported_versions_odd : + (parse ([22, 3, 1, 0, 55, 1, 0, 0, 51, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 8, 0, 43, 0, 4, 3, 3, 4, 3] : List UInt8)).isSome = false := by + decide +kernel + + +theorem Spec.rejects_supported_versions_zero : + (parse ([22, 3, 1, 0, 52, 1, 0, 0, 48, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 5, 0, 43, 0, 1, 0] : List UInt8)).isSome = false := by + decide +kernel + + +theorem Spec.rejects_alpn_empty_name : + (parse ([22, 3, 1, 0, 54, 1, 0, 0, 50, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 7, 0, 16, 0, 3, 0, 1, 0] : List UInt8)).isSome = false := by + decide +kernel + + +theorem Spec.rejects_sni_second_host_name : + (parse ([22, 3, 1, 0, 77, 1, 0, 0, 73, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 30, 0, 0, 0, 26, 0, 24, 0, 0, 9, 97, 46, 101, 120, 97, 109, 112, 108, 101, 0, 0, 9, 98, 46, 101, 120, 97, 109, 112, 108, 101] : List UInt8)).isSome = false := by + decide +kernel + + +theorem Spec.rejects_sni_list_length : + (parse ([22, 3, 1, 0, 67, 1, 0, 0, 63, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 20, 0, 0, 0, 16, 0, 99, 0, 0, 11, 101, 120, 97, 109, 112, 108, 101, 46, 99, 111, 109] : List UInt8)).isSome = false := by + decide +kernel diff --git a/Proofs/Verify.lean b/Proofs/Verify.lean new file mode 100644 index 0000000..ab094b5 --- /dev/null +++ b/Proofs/Verify.lean @@ -0,0 +1,4 @@ +import Proofs.RoundTrip + +#print axioms ClientHello.Proofs.parse_print +#print axioms ClientHello.Proofs.print_parse diff --git a/README.md b/README.md index 5d9891b..848f7b9 100644 --- a/README.md +++ b/README.md @@ -1,38 +1,167 @@ -# clienthello +# clienthello: a TLS ClientHello parser and printer, with proved round trips -A Lean parser for the TLS ClientHello message. This is a Proven Commons project: it rebuilds a widely used format in Lean and proves the new code follows its written specification. +Status: in-progress -Status: not verified. No code has landed yet. Plan issue 1 holds the first slice, and it is unclaimed. The specification has not been approved by a reviewer, so do not call this verified. +A parser and printer for the TLS ClientHello message, in +Lean, following RFC 8446 section 4.1.2, with the legacy +fields carried from RFC 5246, the server name indication +from RFC 6066, and ALPN from RFC 7301. The definitions are +in `ClientHello/Value.lean` (the data model and the +printer) and `ClientHello/Parse.lean` (the parser). The +proofs are in `Proofs/RoundTrip.lean`. The rules are +written out in `SPEC.md`. This slice reads one TLS record +holding one ClientHello; it does no handshake crypto and +parses no certificates. -## First slice +The statements a reviewer approves are in `Spec.lean`, +with their proofs in `Proofs/SpecProofs.lean`. No reviewer +has approved them yet, so this project is not called +verified. -- The TLS record header plus the ClientHello, from RFC 8446 section 4.1.2, with legacy fields from RFC 5246. -- Version, random, session id, cipher suites, and compression methods. -- Extensions as a type length value list. Four are decoded: server name indication, application layer protocol negotiation, supported versions, and key share. -- Other extensions are carried as opaque bytes with length checks, not interpreted. +## How to run it -This is distinct from the hostname repo. ClientHello extracts the server name string. Matching that name against a certificate stays in the hostname repo. +`lake build` builds the library, the proofs, and the +command line tool. The tool reads one request per line: +the word `parse`, a space, and the message as +comma-separated decimal byte codes. It answers `ok:` and +the byte codes of the canonical reprint when the message +parses, `none` when it is rejected, and `error` when the +request itself is malformed. -## Main claim +`python3 tests/run_tests.py` rebuilds, runs the fixed +cases, the named rejections, and the differential run +against the harness oracle, and writes the outcome to +`tests/TEST-RESULTS.md`. -The parser never reads past the end of the message. A duplicate extension type is rejected. A duplicate key share group is rejected. An extension length that runs past the message is rejected. Printing the parsed form gives the same bytes for the parsed subset. +## What is proved -## Test oracles +Each claim below names the theorem behind it. The +theorems are stated in `Spec.lean` (the challenge file, +where they end in `sorry`) and proved in +`Proofs/SpecProofs.lean`, under the same names. +`comparator.json` lists all of them. -- Go crypto/tls. -- OpenSSL captures. -- Wireshark TLS dissectors. +| Claim | Theorem | +|-------|---------| +| Parsing the printed form of a well formed message gives the message back. | `Spec.parse_print` | +| Printing a message the parser took gives the same bytes it was read from, and the message is well formed. | `Spec.print_parse` | +| A hello with a present, empty extensions block is accepted and writes back as the same bytes. | `Spec.accepts_empty_extensions` | +| A minimal hello carrying only supported_versions is accepted and writes back as the same bytes. | `Spec.accepts_supported_versions` | +| Empty input is refused. | `Spec.rejects_empty` | +| Input shorter than the record header is refused. | `Spec.rejects_short_header` | +| A record length of 0 is refused. | `Spec.rejects_record_length_zero` | +| A content type other than 22 is refused. | `Spec.rejects_content_type` | +| A record length longer than the input is refused. | `Spec.rejects_record_length_longer` | +| Bytes after the record are refused. | `Spec.rejects_trailing_bytes` | +| A handshake type other than 1 is refused. | `Spec.rejects_handshake_type` | +| A handshake length that does not match the body is refused. | `Spec.rejects_handshake_length` | +| A body with no extensions block is refused. | `Spec.rejects_missing_extensions` | +| A session id length of 33 is refused. | `Spec.rejects_session_id_33` | +| A cipher suite list with an odd byte length is refused. | `Spec.rejects_odd_cipher_suites` | +| An empty cipher suite list is refused. | `Spec.rejects_empty_cipher_suites` | +| Compression methods without the null method 0 are refused. | `Spec.rejects_compression_without_null` | +| An empty compression method list is refused. | `Spec.rejects_empty_compression` | +| An extension type standing twice is refused. | `Spec.rejects_duplicate_extension` | +| An extension length running past the block is refused. | `Spec.rejects_extension_overrun` | +| A key share group standing twice is refused. | `Spec.rejects_duplicate_key_share_group` | +| A key share entry with empty key bytes is refused. | `Spec.rejects_key_share_empty_key` | +| A key_share value with no entries is refused. | `Spec.rejects_key_share_empty_list` | +| A supported_versions value with an odd length is refused. | `Spec.rejects_supported_versions_odd` | +| A supported_versions value with length 0 is refused. | `Spec.rejects_supported_versions_zero` | +| An ALPN value with an empty protocol name is refused. | `Spec.rejects_alpn_empty_name` | +| A server_name value with two host_name entries is refused. | `Spec.rejects_sni_second_host_name` | +| A server_name list length that does not cover the value is refused. | `Spec.rejects_sni_list_length` | -## Score +A message is well formed when the record version and the +legacy version each fit two bytes; the random holds +exactly 32 bytes; the session id holds at most 32 bytes; +the cipher suites are nonempty, each fits two bytes, and +there are at most 32767 of them; the compression methods +are nonempty, contain the null method 0, and number at +most 255; every extension is well formed (its lengths fit +their fields, SNI has distinct entry types and a nonempty +host name when present, ALPN names are nonempty, key +share groups are distinct with nonempty keys, and an +opaque extension's type is none of the four decoded +types); no extension type stands twice; the printed +extensions block fits two bytes of length; and the +printed body fields fit the three byte handshake length +with room to spare (at most 65531 bytes). -15 out of 18, first pass score in mission issue 19, the round 4 sheet. Created at the org owner's direction on that sheet, on the judgement that the slice, claim, and oracles are sound and that it duplicates no existing repo. +The two round trip theorems rest on the proofs in +`Proofs/RoundTrip.lean`, where they are +`ClientHello.Proofs.parse_print` and +`ClientHello.Proofs.print_parse`. Both check against the +standard axioms only (`propext`, `Classical.choice`, +`Quot.sound`), which a reader can confirm with +`#print axioms`; `Proofs/Verify.lean` prints them at +build time. The example theorems are single inputs +checked in the kernel with `decide +kernel`. -## What is not in this slice +The command line tool in `Main.lean` calls +`ClientHello.parse` and `ClientHello.print` directly, +the same functions the theorems are about. -- The rest of the TLS handshake. -- Certificate parsing. That follows from the der repo. -- Any claim about a full TLS implementation. +## What is not proved -## Layout, when the first slice lands +- That the parser accepts every message the rules in + `SPEC.md` allow, and turns away every message they + forbid. The round trips do not need either, and the + example theorems pin single inputs only, so neither + holds in general as a proof. The differential tests in + `tests/` check that behaviour instead, and the results + file records the outcome, including any failure. +- The meaning of any extension other than the four + decoded ones. Every other extension is carried as its + type and value bytes, and no per extension content rule + is checked. +- Anything about the host name bytes beyond their being + nonempty when present: no label rules, no case rules, no + matching against a certificate. Name matching belongs + to the hostname work. +- Anything about the rest of the handshake, the key + schedule, or any other record or message type. -The layout follows the Proven Commons template in the mission repo, under bar/template. Spec.lean holds the statements a reviewer approves. Proofs.lean holds the proofs under the same names. Main.lean holds the command line tool used by the tests. The bar check runs in CI on every change. +## What you must trust + +- The Lean kernel (Lean 4.35.0, pinned in + `lean-toolchain`), which checks every proof. +- The Lean compiler, which turns the proved definitions + into the program that runs. +- The Lean runtime, which runs that program. +- The hardware the program runs on. +- Every dependency in `lake-manifest.json`: the manifest + lists no packages, so there are no library dependencies + to trust beyond the Lean toolchain itself. +- That `SPEC.md` states the reading of the RFCs you + intend. The proofs are about the parser and printer in + this repo following each other exactly; the fidelity of + the spec to the RFCs is a reading, pinned in SPEC.md + where the RFCs leave a choice open. +- The test oracle in `tests/run_tests.py` is a second + reading of the same rules, in Python. It is evidence, + not proof. +- The line handling in `Main.lean` (splitting a request + line, reading decimal codes). The tests drive it, and + no proof covers it. +- There are no exceptions to item 4 of the bar: the + project uses none of the features it forbids. + +## Re-check it + +1. `lake comparator --paranoid`: builds the challenge + file `Spec.lean` and the proofs in a sandbox and + checks that each theorem named in `comparator.json` + proves exactly the statement in the challenge file, + uses no axiom but the three standard ones, and is + accepted by Lean's kernel and every other kernel + shipped with Lean. +2. `python3 tests/run_tests.py`: the fixed cases, the + named rejections, and the differential run against + the oracle, with counts and any failures written to + `tests/TEST-RESULTS.md`. +3. `lake build`: the library, the proofs, and the tool + build clean, and the build prints the axiom list for + both round trip theorems. +4. Read `SPEC.md` against RFC 8446 section 4.1.2 and + check the pinned readings are the ones you want. diff --git a/SPEC.md b/SPEC.md new file mode 100644 index 0000000..71a123b --- /dev/null +++ b/SPEC.md @@ -0,0 +1,205 @@ +# Specification: clienthello + +A TLS ClientHello parser and printer in Lean, following +RFC 8446 section 4.1.2 (the ClientHello message), the +legacy fields as carried from RFC 5246, RFC 6066 section 3 +(the server name indication), and RFC 7301 (ALPN). This +slice reads exactly one TLS record holding exactly one +ClientHello, and prints that message back in canonical +form: every length is recomputed from the values. + +## The record layer + +A message is one TLS record: + +| Bytes | Field | +|-------|-------| +| 0 | content type: must be 22 (handshake) | +| 1, 2 | legacy record version: carried, value unchecked | +| 3, 4 | length: two bytes, big endian | +| 5 ... | the record body, exactly that many bytes | + +- Input shorter than the five byte header rejects. +- A body shorter than the declared length rejects. +- Bytes after the record reject. The decoder takes exactly + one record; a stream reader is later work. +- A record length of 0 rejects: an empty body cannot hold + a ClientHello. (In the code this falls out of the body + read failing; it is stated here because it is a rule a + reader of the bytes should expect.) + +## The handshake header + +Inside the record body: + +| Bytes | Field | +|-------|-------| +| 0 | message type: must be 1 (client_hello) | +| 1, 2, 3 | length: three bytes, big endian | +| 4 ... | the ClientHello body | + +The three byte length must equal the remaining body length +exactly. A mismatch rejects. + +## The ClientHello body + +In order: + +| Field | Size | Rule | +|-------|------|------| +| legacy version | 2 bytes | carried, value unchecked | +| random | 32 bytes | exactly 32 | +| legacy session id | 1 byte length, then that many bytes | length at most 32; a longer length rejects | +| cipher suites | 2 byte length, then that many bytes | length even and at least 2; the bytes read as two byte suite codes; an empty list or an odd length rejects | +| legacy compression methods | 1 byte length, then that many bytes | length at least 1; the list must contain the byte 0 (the null method) | +| extensions | 2 byte length, then that many bytes | the block must consume the rest of the body exactly | + +The extensions block must be present. A body that ends +after the compression methods is the pre-TLS-1.3 shape; +this slice rejects it, because the slice frames the +message by its extensions and supported_versions is how a +TLS 1.3 hello speaks. The block may be empty: a present +block of length 0 consumes the body and carries no +extensions, and is accepted. + +## Extensions + +Each extension is a two byte type, a two byte length, and +that many value bytes. An extension length running past +the end of the block rejects, and the block must be +consumed exactly. A duplicate extension type rejects. + +Four types are decoded. Every other type is carried as +the pair of its type and its raw value bytes, length +checked, not interpreted. + +### server_name (type 0), RFC 6066 section 3 + +The value is a two byte list length covering the rest of +the value, then entries. Each entry is a one byte name +type, a two byte length, and that many bytes. Type 0 is +host_name. + +- The list length must equal the value length minus two. +- The list must be nonempty and consume the value exactly. +- Two entries of the same type reject, so there is at + most one host_name entry. +- The host_name bytes must be nonempty. +- Host name bytes are carried as bytes. No case folding, + label, or character validation happens in this slice. + Entries of other types are carried as (type, bytes). + +### ALPN (type 16), RFC 7301 + +The value is a two byte list length covering the rest of +the value, then protocol names. Each name is a one byte +length and that many bytes. + +- The list length must equal the value length minus two. +- The list must be nonempty and consume the value exactly. +- A name length of 0 rejects. + +### supported_versions (type 43), RFC 8446 section 4.2.1 + +The client form: a one byte length, then that many bytes +read as two byte versions. + +- The length must equal the value length minus one. +- The length must be even and at least 2. An odd or zero + length rejects. + +The server form (a single version) is not this message and +is not read here. + +### key_share (type 51), RFC 8446 section 4.2.8 + +The client form: a two byte list length covering the rest +of the value, then entries. Each entry is a two byte +group, a two byte key exchange length, and that many +bytes. + +- The list length must equal the value length minus two. +- The list must be nonempty and consume the value exactly. +- A key exchange length of 0 rejects. +- A duplicate group rejects. + +## Pinned readings + +Where the RFCs or the plan leave a reading open, this +slice pins it: + +- Trailing bytes after the record reject. +- A missing extensions block rejects; a present block of + length 0 is accepted. +- Compression methods must contain the byte 0. +- The session id length is at most 32. +- The cipher suite list is nonempty, with an even byte + length. +- A duplicate extension type rejects. +- SNI carries at most one host_name entry, and duplicate + SNI entry types reject in general. +- Host name bytes are unvalidated beyond being nonempty. +- Unknown extension types are carried opaque. +- A duplicate key share group rejects. + +## Properties and their theorems + +Each property a reader can check in the page (`README.md`) +names its theorem. The theorems are stated in `Spec.lean` +and proved in `Proofs/SpecProofs.lean`. The example +theorems are single inputs; the tests in `tests/` cover +each rule on many more inputs. + +| Property | Theorem | +|----------|---------| +| Parsing the printed form of a well formed message gives the message back | `Spec.parse_print` | +| A message the parser took prints back to the bytes it was read from, and is well formed | `Spec.print_parse` | +| A present, empty extensions block is accepted | `Spec.accepts_empty_extensions` | +| A minimal hello with only supported_versions is accepted | `Spec.accepts_supported_versions` | +| Empty input is refused | `Spec.rejects_empty` | +| Input shorter than the record header is refused | `Spec.rejects_short_header` | +| A record length of 0 is refused | `Spec.rejects_record_length_zero` | +| A content type other than 22 is refused | `Spec.rejects_content_type` | +| A record length longer than the input is refused | `Spec.rejects_record_length_longer` | +| Bytes after the record are refused | `Spec.rejects_trailing_bytes` | +| A handshake type other than 1 is refused | `Spec.rejects_handshake_type` | +| A handshake length that does not match the body is refused | `Spec.rejects_handshake_length` | +| A body with no extensions block is refused | `Spec.rejects_missing_extensions` | +| A session id length over 32 is refused | `Spec.rejects_session_id_33` | +| A cipher suite list with an odd byte length is refused | `Spec.rejects_odd_cipher_suites` | +| An empty cipher suite list is refused | `Spec.rejects_empty_cipher_suites` | +| Compression methods must contain the null method 0 | `Spec.rejects_compression_without_null` | +| An empty compression method list is refused | `Spec.rejects_empty_compression` | +| A duplicate extension type is refused | `Spec.rejects_duplicate_extension` | +| An extension length running past the block is refused | `Spec.rejects_extension_overrun` | +| A duplicate key share group is refused | `Spec.rejects_duplicate_key_share_group` | +| A key share entry with empty key bytes is refused | `Spec.rejects_key_share_empty_key` | +| A key_share value with no entries is refused | `Spec.rejects_key_share_empty_list` | +| A supported_versions value with an odd length is refused | `Spec.rejects_supported_versions_odd` | +| A supported_versions value with length 0 is refused | `Spec.rejects_supported_versions_zero` | +| An ALPN value with an empty protocol name is refused | `Spec.rejects_alpn_empty_name` | +| A server_name value with two host_name entries is refused | `Spec.rejects_sni_second_host_name` | +| A server_name list length that does not cover the value is refused | `Spec.rejects_sni_list_length` | + +## Safety + +The parser never reads past the end of its input. Every +read goes through the length checked readers (getU8, +getU16, getU24, getBytes): a read either takes bytes that +are present, checked against the remaining length, or +fails. The extension parsers run over a value already cut +to its declared length, so the same check bounds them. +This is the reader model used across the sibling slices. + +## Slice boundaries + +- No server messages: no ServerHello, no EncryptedExtensions, + no Certificate, no Finished. +- No handshake crypto: no key schedule, no transcript hash, + no signature checking. +- No certificate work of any kind, and no matching of the + server name against a certificate. That matching belongs + to the hostname work; this slice only carries the name + bytes out of the message. +- One record only: no stream reading, no record splitting + or joining, no alerts, no renegotiation. diff --git a/Spec.lean b/Spec.lean new file mode 100644 index 0000000..428c659 --- /dev/null +++ b/Spec.lean @@ -0,0 +1,155 @@ +/- + The specification as Lean statements: the challenge file. + + A reviewer who did not write this file approves it, and `bar.toml` + records the SHA-256 it had then. The proofs live in `Proofs` + (`Proofs/SpecProofs.lean`); `lake comparator` checks that each one + proves exactly the statement written here. The `sorry` below is + expected in this file only. + + The statements use only the definitions in `ClientHello/Value.lean` + and `ClientHello/Parse.lean`, the code under proof named in + `bar.toml`. No definition of their own is needed, so this project + has no `Spec/Defs.lean`. +-/ + +import ClientHello + +open ClientHello + +/-! ## The round trips + +The two statements the slice stands on. Each one is the statement of +the proved theorem of the same shape in `Proofs/RoundTrip.lean`, over +the same well formedness predicate, `ClientHello.WF`. -/ + +/-- Parsing the printed form of a well formed message gives the + message back. -/ +theorem Spec.parse_print (m : Message) (hw : WF m) : + parse (print m) = some m := sorry + +/-- A message the parser took prints back to the bytes it was read + from, and the message is well formed. So a printer that wrote + nothing, or wrote something shorter, fails the first half. -/ +theorem Spec.print_parse {bs : List UInt8} {m : Message} + (hparse : parse bs = some m) : + print m = bs ∧ WF m := sorry + +/-! ## Accepted examples + +Single inputs the parser accepts. Each one is stated in the form the +round trip gives for a single input: parsing the bytes and printing +the result gives the same bytes back. -/ + +/-- A hello whose extensions block is present and empty is accepted, and writes back as the same bytes. -/ +theorem Spec.accepts_empty_extensions : + (parse ([22, 3, 1, 0, 47, 1, 0, 0, 43, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 0] : List UInt8)).map print = + some ([22, 3, 1, 0, 47, 1, 0, 0, 43, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 0] : List UInt8) := sorry + +/-- A minimal hello carrying only a supported_versions extension is accepted, and writes back as the same bytes. -/ +theorem Spec.accepts_supported_versions : + (parse ([22, 3, 1, 0, 56, 1, 0, 0, 52, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 9, 0, 43, 0, 5, 4, 3, 4, 3, 3] : List UInt8)).map print = + some ([22, 3, 1, 0, 56, 1, 0, 0, 52, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 9, 0, 43, 0, 5, 4, 3, 4, 3, 3] : List UInt8) := sorry + +/-! ## Refused inputs + +Single inputs the parser refuses, one for each headline rule of +`SPEC.md`. The differential tests cover these rules on many more +inputs; these statements pin them so a reader of the specification +can check each rule against one concrete case. -/ + +/-- Empty input is refused: it is not a record with an empty body. -/ +theorem Spec.rejects_empty : + (parse ([] : List UInt8)).isSome = false := sorry + +/-- Input shorter than the five byte record header is refused. -/ +theorem Spec.rejects_short_header : + (parse ([22, 3] : List UInt8)).isSome = false := sorry + +/-- A record length of 0 is refused: an empty body cannot hold a ClientHello. -/ +theorem Spec.rejects_record_length_zero : + (parse ([22, 3, 1, 0, 0] : List UInt8)).isSome = false := sorry + +/-- A content type other than 22 (handshake) is refused. -/ +theorem Spec.rejects_content_type : + (parse ([23, 3, 1, 0, 0] : List UInt8)).isSome = false := sorry + +/-- A record length longer than the input is refused rather than read past the end. -/ +theorem Spec.rejects_record_length_longer : + (parse ([22, 3, 1, 0, 10, 1, 0, 0, 0] : List UInt8)).isSome = false := sorry + +/-- Bytes after the record are refused rather than ignored. -/ +theorem Spec.rejects_trailing_bytes : + (parse ([22, 3, 1, 0, 47, 1, 0, 0, 43, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 0, 0] : List UInt8)).isSome = false := sorry + +/-- A handshake type other than 1 (client_hello) is refused. -/ +theorem Spec.rejects_handshake_type : + (parse ([22, 3, 1, 0, 4, 2, 0, 0, 0] : List UInt8)).isSome = false := sorry + +/-- A handshake length that does not equal the remaining body length is refused. -/ +theorem Spec.rejects_handshake_length : + (parse ([22, 3, 1, 0, 47, 1, 0, 0, 44, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 0] : List UInt8)).isSome = false := sorry + +/-- A body that ends after the compression methods, with no extensions block, is refused. -/ +theorem Spec.rejects_missing_extensions : + (parse ([22, 3, 1, 0, 45, 1, 0, 0, 41, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0] : List UInt8)).isSome = false := sorry + +/-- A session id length of 33 is refused: the limit is 32. -/ +theorem Spec.rejects_session_id_33 : + (parse ([22, 3, 1, 0, 39, 1, 0, 0, 35, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 33] : List UInt8)).isSome = false := sorry + +/-- A cipher suite list with an odd byte length is refused. -/ +theorem Spec.rejects_odd_cipher_suites : + (parse ([22, 3, 1, 0, 41, 1, 0, 0, 37, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 3] : List UInt8)).isSome = false := sorry + +/-- An empty cipher suite list is refused. -/ +theorem Spec.rejects_empty_cipher_suites : + (parse ([22, 3, 1, 0, 41, 1, 0, 0, 37, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 0] : List UInt8)).isSome = false := sorry + +/-- Compression methods that do not contain the null method 0 are refused. -/ +theorem Spec.rejects_compression_without_null : + (parse ([22, 3, 1, 0, 45, 1, 0, 0, 41, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 1] : List UInt8)).isSome = false := sorry + +/-- An empty compression method list is refused. -/ +theorem Spec.rejects_empty_compression : + (parse ([22, 3, 1, 0, 44, 1, 0, 0, 40, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 0] : List UInt8)).isSome = false := sorry + +/-- An extension type standing twice in one block is refused. -/ +theorem Spec.rejects_duplicate_extension : + (parse ([22, 3, 1, 0, 61, 1, 0, 0, 57, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 14, 0, 43, 0, 3, 2, 3, 4, 0, 43, 0, 3, 2, 3, 3] : List UInt8)).isSome = false := sorry + +/-- An extension length that runs past the end of the block is refused. -/ +theorem Spec.rejects_extension_overrun : + (parse ([22, 3, 1, 0, 54, 1, 0, 0, 50, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 7, 0, 0, 0, 10, 2, 3, 4] : List UInt8)).isSome = false := sorry + +/-- A key share group standing twice in one key_share value is refused. -/ +theorem Spec.rejects_duplicate_key_share_group : + (parse ([22, 3, 1, 0, 63, 1, 0, 0, 59, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 16, 0, 51, 0, 12, 0, 10, 0, 29, 0, 1, 1, 0, 29, 0, 1, 2] : List UInt8)).isSome = false := sorry + +/-- A key share entry with empty key exchange bytes is refused. -/ +theorem Spec.rejects_key_share_empty_key : + (parse ([22, 3, 1, 0, 57, 1, 0, 0, 53, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 10, 0, 51, 0, 6, 0, 4, 0, 29, 0, 0] : List UInt8)).isSome = false := sorry + +/-- A key_share value with no entries is refused. -/ +theorem Spec.rejects_key_share_empty_list : + (parse ([22, 3, 1, 0, 53, 1, 0, 0, 49, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 6, 0, 51, 0, 2, 0, 0] : List UInt8)).isSome = false := sorry + +/-- A supported_versions value with an odd byte length is refused. -/ +theorem Spec.rejects_supported_versions_odd : + (parse ([22, 3, 1, 0, 55, 1, 0, 0, 51, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 8, 0, 43, 0, 4, 3, 3, 4, 3] : List UInt8)).isSome = false := sorry + +/-- A supported_versions value with a length of 0 is refused. -/ +theorem Spec.rejects_supported_versions_zero : + (parse ([22, 3, 1, 0, 52, 1, 0, 0, 48, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 5, 0, 43, 0, 1, 0] : List UInt8)).isSome = false := sorry + +/-- An ALPN value holding an empty protocol name is refused. -/ +theorem Spec.rejects_alpn_empty_name : + (parse ([22, 3, 1, 0, 54, 1, 0, 0, 50, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 7, 0, 16, 0, 3, 0, 1, 0] : List UInt8)).isSome = false := sorry + +/-- A server_name value with two host_name entries is refused. -/ +theorem Spec.rejects_sni_second_host_name : + (parse ([22, 3, 1, 0, 77, 1, 0, 0, 73, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 30, 0, 0, 0, 26, 0, 24, 0, 0, 9, 97, 46, 101, 120, 97, 109, 112, 108, 101, 0, 0, 9, 98, 46, 101, 120, 97, 109, 112, 108, 101] : List UInt8)).isSome = false := sorry + +/-- A server_name value whose list length does not cover the rest of the value is refused. -/ +theorem Spec.rejects_sni_list_length : + (parse ([22, 3, 1, 0, 67, 1, 0, 0, 63, 3, 3, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 0, 2, 19, 1, 1, 0, 0, 20, 0, 0, 0, 16, 0, 99, 0, 0, 11, 101, 120, 97, 109, 112, 108, 101, 46, 99, 111, 109] : List UInt8)).isSome = false := sorry diff --git a/bar.toml b/bar.toml new file mode 100644 index 0000000..afebc16 --- /dev/null +++ b/bar.toml @@ -0,0 +1,53 @@ +# Read by bar/check.py in Proven-Commons/mission. +# See playbook/verified-bar.md there for what each field means. + +[project] +name = "clienthello" +# "in-progress" until every bar item passes, then "verified". +status = "in-progress" +page = "README.md" +# GitHub handles of everyone who wrote the specification. +spec_authors = ["abu-aska"] +# The program people run. A change to it voids the approval. +entry_points = ["Main.lean"] + +[spec] +files = ["SPEC.md", "Spec.lean"] +# The code under proof: the functions the statements are about. +code = [ + # The data types the statements are about, and their constructors. + "ClientHello.Message", "ClientHello.Hello", "ClientHello.Extension", + "ClientHello.Extension.serverName", "ClientHello.Extension.alpn", + "ClientHello.Extension.supportedVersions", "ClientHello.Extension.keyShare", + "ClientHello.Extension.opaque", + # The byte forms and the printer. + "ClientHello.be16", "ClientHello.u16", "ClientHello.be24", "ClientHello.u24", + "ClientHello.extType", "ClientHello.printPairs", "ClientHello.printNameEntries", + "ClientHello.printAlpnNames", "ClientHello.printShares", + "ClientHello.printExtValue", "ClientHello.printExt", "ClientHello.printExts", + "ClientHello.printBodyFields", "ClientHello.printBody", "ClientHello.print", + # Well formedness. + "ClientHello.ExtWF", "ClientHello.WF", + # The length checked readers and the parser. + "ClientHello.getU8", "ClientHello.getU16", "ClientHello.getU24", + "ClientHello.getBytes", "ClientHello.parsePairs", + "ClientHello.parseNameEntriesGo", "ClientHello.parseNameEntries", + "ClientHello.validNames", "ClientHello.parseSNI", + "ClientHello.parseAlpnGo", "ClientHello.parseAlpnNames", "ClientHello.parseALPN", + "ClientHello.parseSV", "ClientHello.parseSharesGo", "ClientHello.parseShares", + "ClientHello.parseKS", "ClientHello.parseExtValue", + "ClientHello.parseExtsGo", "ClientHello.parseExts", + "ClientHello.parseBodyFields", "ClientHello.parseBody", "ClientHello.parse", +] + +# One entry per approval, added in a pull request the reviewer approves. +# [[spec.approval]] +# reviewer = "github-handle" +# date = "2026-11-02" +# sha256 = "..." +# record = "https://github.com/Proven-Commons/clienthello/pull/" + +[tests] +results = "tests/TEST-RESULTS.md" +command = "python3 tests/run_tests.py" +files = ["tests/run_tests.py"] diff --git a/comparator.json b/comparator.json new file mode 100644 index 0000000..96381be --- /dev/null +++ b/comparator.json @@ -0,0 +1,39 @@ +{ + "challenge_module": "Spec", + "solution_module": "Proofs", + "theorem_names": [ + "Spec.parse_print", + "Spec.print_parse", + "Spec.accepts_empty_extensions", + "Spec.accepts_supported_versions", + "Spec.rejects_empty", + "Spec.rejects_short_header", + "Spec.rejects_record_length_zero", + "Spec.rejects_content_type", + "Spec.rejects_record_length_longer", + "Spec.rejects_trailing_bytes", + "Spec.rejects_handshake_type", + "Spec.rejects_handshake_length", + "Spec.rejects_missing_extensions", + "Spec.rejects_session_id_33", + "Spec.rejects_odd_cipher_suites", + "Spec.rejects_empty_cipher_suites", + "Spec.rejects_compression_without_null", + "Spec.rejects_empty_compression", + "Spec.rejects_duplicate_extension", + "Spec.rejects_extension_overrun", + "Spec.rejects_duplicate_key_share_group", + "Spec.rejects_key_share_empty_key", + "Spec.rejects_key_share_empty_list", + "Spec.rejects_supported_versions_odd", + "Spec.rejects_supported_versions_zero", + "Spec.rejects_alpn_empty_name", + "Spec.rejects_sni_second_host_name", + "Spec.rejects_sni_list_length" + ], + "permitted_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ] +} diff --git a/lake-manifest.json b/lake-manifest.json new file mode 100644 index 0000000..e965eb3 --- /dev/null +++ b/lake-manifest.json @@ -0,0 +1,6 @@ +{"version": "1.3.0", + "packagesDir": ".lake/packages", + "packages": [], + "name": "clienthello", + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/lakefile.toml b/lakefile.toml new file mode 100644 index 0000000..700b760 --- /dev/null +++ b/lakefile.toml @@ -0,0 +1,16 @@ +name = "clienthello" +version = "0.1.0" +defaultTargets = ["ClientHello", "Proofs", "clienthello"] + +[[lean_lib]] +name = "ClientHello" + +[[lean_lib]] +name = "Proofs" + +[[lean_lib]] +name = "Spec" + +[[lean_exe]] +name = "clienthello" +root = "Main" diff --git a/lean-toolchain b/lean-toolchain new file mode 100644 index 0000000..a6aff06 --- /dev/null +++ b/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.35.0 diff --git a/tests/TEST-RESULTS.md b/tests/TEST-RESULTS.md new file mode 100644 index 0000000..a647a11 --- /dev/null +++ b/tests/TEST-RESULTS.md @@ -0,0 +1,59 @@ +# ClientHello slice: test results + +Run: python3 tests/run_tests.py --seed 20261026 --count 3200 +Seed: 20261026. Python 3.12.3. + +## Oracles + +Every verdict is settled by the harness oracle, a Python implementation of the rules in SPEC.md written for these tests. The tool must agree with the oracle on every input, and an accepted message must reprint to the oracle's canonical reprint byte for byte. + +Python's ssl module cannot build a ClientHello on demand. Go is not installed (`go version` fails). Scapy 2.8.0 is present in the sibling dhcp project's venv and its TLS submodules import, but building or dissecting a TLS record raises NameError inside scapy's crypto support (HMAC is not defined), so Scapy could not be used as a byte source. No capture was fetched; the fixed cases are built by hand from the RFCs. + +## Counts + +| part | run | agreed | +| --- | --- | --- | +| named cases | 29 | 29 | +| generated messages | 3200 | 3200 | +| mutations of the full hello | 1308 | 1308 | +| random raw byte strings | 300 | 300 | +| malformed request lines | 7 | 7 | +| total | 4844 | 4844 | + +Of the 3200 generated messages, the oracle accepts 1125 and rejects 2075. + +## Named cases + +- full TLS 1.3 style hello: accept (252 bytes) +- minimal hello, supported versions only: accept (61 bytes) +- duplicate extension type: reject (66 bytes) +- duplicate key share group: reject (130 bytes) +- extension length overrunning the block: reject (59 bytes) +- record length longer than the input: reject (52 bytes) +- handshake length not matching the body: reject (52 bytes) +- content type 23: reject (61 bytes) +- handshake type 2: reject (61 bytes) +- session id length 33: reject (85 bytes) +- odd cipher suite length: reject (53 bytes) +- empty cipher suites: reject (50 bytes) +- compression methods without 0: reject (53 bytes) +- missing extensions block: reject (50 bytes) +- supported versions odd length: reject (60 bytes) +- supported versions length zero: reject (57 bytes) +- ALPN empty name: reject (59 bytes) +- ALPN list length mismatch: reject (61 bytes) +- ALPN empty list: reject (58 bytes) +- SNI second host_name entry: reject (82 bytes) +- SNI list length mismatch: reject (72 bytes) +- SNI empty list: reject (58 bytes) +- key share empty key bytes: reject (62 bytes) +- key share empty list: reject (58 bytes) +- trailing garbage after the record: reject (53 bytes) +- empty extensions block, length 0, accepted: accept (52 bytes) +- record length zero: reject (5 bytes) +- input shorter than the record header: reject (2 bytes) +- empty input: reject (0 bytes) + +## Differences + +No disagreements between the tool and the oracle, and every named case matched its stated expectation. diff --git a/tests/run_tests.py b/tests/run_tests.py new file mode 100644 index 0000000..24c8047 --- /dev/null +++ b/tests/run_tests.py @@ -0,0 +1,860 @@ +#!/usr/bin/env python3 +"""Tests for the Lean TLS ClientHello parser and printer. + +Three parts. + +1. Fixed cases built by hand from RFC 8446 section 4.1.2, + RFC 5246 and RFC 6066: one full TLS 1.3 style hello (SNI + for a named host, ALPN h2 and http/1.1, supported versions + 0x0304 and 0x0303, key shares for x25519 and secp256r1 + with fixed key bytes, and one opaque extension), one + minimal hello (supported versions only), and the named + rejection shapes listed in SPEC.md, plus the pinned + reading that a present but empty extensions block (length + 0) is accepted. + +2. A differential run against a strict Python oracle written + in this harness from the rules in SPEC.md: at least 3,000 + generated messages (varied record and legacy versions, + session ids, cipher suite lists, compression lists, + extension sets and orders, with defects injected from a + menu), plus raw mutations of the full fixed hello (every + truncation, single byte flips, random multi-byte changes) + and fully random byte strings. The oracle settles every + verdict; the tool must agree with it on each input. + +3. Malformed request lines must be answered `error`. + +Oracle availability, checked when this harness was written +and stated again in the results record: Python's ssl module +cannot build a ClientHello on demand. Go is not installed +(`go version` fails). Scapy 2.8.0 is importable from the +sibling dhcp project's venv and its TLS submodules import, +but building or dissecting a TLS record raises NameError +inside scapy's crypto support (HMAC is not defined), so +Scapy cannot serve as a byte source in this environment and +was not used. No captured ClientHello was fetched; the +fixed cases are built by hand from the RFCs. + + python3 tests/run_tests.py [--seed N] [--count N] + +The tool is driven one batch process per chunk of requests, +input written and closed, output drained until the process +exits. It builds the executable first, writes +tests/TEST-RESULTS.md, and exits non-zero if any check +fails. It needs Python 3.11 or later. +""" + +import argparse +import os +import platform +import random +import subprocess +import sys +import threading +from pathlib import Path + +ROOT = Path(__file__).resolve().parent.parent +EXE = ROOT / ".lake" / "build" / "bin" / "clienthello" +RESULTS = ROOT / "tests" / "TEST-RESULTS.md" + + +# ---------------------------------------------------------------- +# The oracle: an independent implementation of the SPEC rules. +# It parses bytes into a model and reprints the model; the +# reprint of an accepted message is the expected tool answer. +# ---------------------------------------------------------------- + +class Reject(Exception): + pass + + +def take(bs, i, n): + if i + n > len(bs): + raise Reject() + return bs[i:i + n], i + n + + +def u8(bs, i): + bs2, i = take(bs, i, 1) + return bs2[0], i + + +def u16(bs, i): + bs2, i = take(bs, i, 2) + return (bs2[0] << 8) | bs2[1], i + + +def u24(bs, i): + bs2, i = take(bs, i, 3) + return (bs2[0] << 16) | (bs2[1] << 8) | bs2[2], i + + +def be16(n): + return bytes([(n >> 8) & 0xFF, n & 0xFF]) + + +def be24(n): + return bytes([(n >> 16) & 0xFF, (n >> 8) & 0xFF, n & 0xFF]) + + +def oracle_sni(v): + listlen, i = u16(v, 0) + if listlen != len(v) - 2: + raise Reject() + entries = [] + seen = set() + while i < len(v): + t, i = u8(v, i) + ln, i = u16(v, i) + name, i = take(v, i, ln) + if t in seen: + raise Reject() + seen.add(t) + if t == 0 and len(name) == 0: + raise Reject() + entries.append((t, bytes(name))) + if not entries: + raise Reject() + out = be16(listlen) + for t, name in entries: + out += bytes([t]) + be16(len(name)) + name + return ("sni", entries), out + + +def oracle_alpn(v): + listlen, i = u16(v, 0) + if listlen != len(v) - 2: + raise Reject() + names = [] + while i < len(v): + ln, i = u8(v, i) + if ln < 1: + raise Reject() + name, i = take(v, i, ln) + names.append(bytes(name)) + if not names: + raise Reject() + out = be16(listlen) + for name in names: + out += bytes([len(name)]) + name + return ("alpn", names), out + + +def oracle_sv(v): + ln, i = u8(v, 0) + if ln != len(v) - 1 or ln % 2 != 0 or ln < 2: + raise Reject() + versions = [] + while i < len(v): + ver, i = u16(v, i) + versions.append(ver) + out = bytes([ln]) + for ver in versions: + out += be16(ver) + return ("sv", versions), out + + +def oracle_ks(v): + listlen, i = u16(v, 0) + if listlen != len(v) - 2: + raise Reject() + shares = [] + seen = set() + while i < len(v): + group, i = u16(v, i) + klen, i = u16(v, i) + if klen < 1: + raise Reject() + key, i = take(v, i, klen) + if group in seen: + raise Reject() + seen.add(group) + shares.append((group, bytes(key))) + if not shares: + raise Reject() + out = be16(listlen) + for group, key in shares: + out += be16(group) + be16(len(key)) + key + return ("ks", shares), out + + +def oracle_ext_value(t, v): + if t == 0: + return oracle_sni(v) + if t == 16: + return oracle_alpn(v) + if t == 43: + return oracle_sv(v) + if t == 51: + return oracle_ks(v) + return ("opaque", t, bytes(v)), bytes(v) + + +def oracle_exts(block): + exts = [] + seen = set() + i = 0 + while i < len(block): + t, i = u16(block, i) + ln, i = u16(block, i) + v, i = take(block, i, ln) + if t in seen: + raise Reject() + seen.add(t) + ext, _ = oracle_ext_value(t, bytes(v)) + exts.append((t, ext)) + return exts + + +def print_ext(ext): + kind = ext[0] + if kind == "sni": + body = b"" + for t, name in ext[1]: + body += bytes([t]) + be16(len(name)) + name + return be16(0) + be16(len(body) + 2) + be16(len(body)) + body + if kind == "alpn": + body = b"" + for name in ext[1]: + body += bytes([len(name)]) + name + return be16(16) + be16(len(body) + 2) + be16(len(body)) + body + if kind == "sv": + body = bytes([2 * len(ext[1])]) + for ver in ext[1]: + body += be16(ver) + return be16(43) + be16(len(body)) + body + if kind == "ks": + body = b"" + for group, key in ext[1]: + body += be16(group) + be16(len(key)) + key + return be16(51) + be16(len(body) + 2) + be16(len(body)) + body + _, t, v = ext + return be16(t) + be16(len(v)) + v + + +def oracle_parse(bs): + """The canonical reprint of the message, or None.""" + try: + return oracle_parse_go(bs) + except Reject: + return None + + +def oracle_parse_go(bs): + ct, i = u8(bs, 0) + if ct != 22: + raise Reject() + rv, i = take(bs, i, 2) + rlen, i = u16(bs, i) + body, i = take(bs, i, rlen) + if i != len(bs): + raise Reject() + htype, j = u8(body, 0) + if htype != 1: + raise Reject() + hlen, j = u24(body, j) + fields, j = take(body, j, hlen) + if j != len(body): + raise Reject() + ver, k = take(fields, 0, 2) + rand, k = take(fields, k, 32) + slen, k = u8(fields, k) + if slen > 32: + raise Reject() + sess, k = take(fields, k, slen) + clen, k = u16(fields, k) + if clen % 2 != 0 or clen < 2: + raise Reject() + cbytes, k = take(fields, k, clen) + suites = [] + for off in range(0, clen, 2): + suites.append((cbytes[off] << 8) | cbytes[off + 1]) + mlen, k = u8(fields, k) + if mlen < 1: + raise Reject() + comps, k = take(fields, k, mlen) + if 0 not in comps: + raise Reject() + elen, k = u16(fields, k) + block, k = take(fields, k, elen) + if k != len(fields): + raise Reject() + exts = oracle_exts(bytes(block)) + out_fields = bytes(ver) + bytes(rand) + out_fields += bytes([len(sess)]) + bytes(sess) + pairs = b"" + for s in suites: + pairs += be16(s) + out_fields += be16(len(pairs)) + pairs + out_fields += bytes([len(comps)]) + bytes(comps) + block_out = b"" + for _, ext in exts: + block_out += print_ext(ext) + out_fields += be16(len(block_out)) + block_out + out_body = bytes([1]) + be24(len(out_fields)) + out_fields + return bytes([22]) + bytes(rv) + be16(len(out_body)) + out_body + + +# ---------------------------------------------------------------- +# Builders: byte level construction of test messages, with +# knobs for the defect cases. The builders are not the oracle; +# every built message is judged by the oracle and the tool. +# ---------------------------------------------------------------- + +def sni_value(entries): + body = b"" + for t, name in entries: + body += bytes([t]) + be16(len(name)) + name + return be16(len(body)) + body + + +def alpn_value(names): + body = b"" + for name in names: + body += bytes([len(name)]) + name + return be16(len(body)) + body + + +def sv_value(versions): + body = bytes([2 * len(versions)]) + for ver in versions: + body += be16(ver) + return body + + +def ks_value(shares): + body = b"" + for group, key in shares: + body += be16(group) + be16(len(key)) + key + return be16(len(body)) + body + + +def ext_bytes(t, v): + return be16(t) + be16(len(v)) + v + + +def build_hello(record_version=b"\x03\x01", legacy_version=b"\x03\x03", + random_bytes=None, session_id=b"", suites=(0x1301,), + comps=(0,), exts=(), ext_block=True, + record_len_delta=0, hs_len_delta=0, trailing=b""): + if random_bytes is None: + random_bytes = bytes(range(32)) + fields = legacy_version + random_bytes + fields += bytes([len(session_id)]) + session_id + pairs = b"" + for s in suites: + pairs += be16(s) + fields += be16(len(pairs)) + pairs + fields += bytes([len(comps)]) + bytes(comps) + if ext_block: + block = b"" + for t, v in exts: + block += ext_bytes(t, v) + fields += be16(len(block)) + block + body = bytes([1]) + be24(len(fields) + hs_len_delta) + fields + rec = bytes([22]) + record_version + rec += be16(len(body) + record_len_delta) + body + return rec + trailing + + +FULL_EXTS = [ + (0, sni_value([(0, b"example.com")])), + (16, alpn_value([b"h2", b"http/1.1"])), + (43, sv_value([0x0304, 0x0303])), + (51, ks_value([(29, bytes(range(32))), + (23, b"\x04" + bytes(range(64)))])), + (23, b""), +] +FULL_HELLO = build_hello( + session_id=bytes(range(32)), + suites=(0x1301, 0x1302, 0x1303, 0xC02F), + exts=FULL_EXTS) +MIN_HELLO = build_hello(exts=[(43, sv_value([0x0304, 0x0303]))]) +EMPTY_EXT_HELLO = build_hello(exts=[]) + + +def raw_fields(suites_bytes, comps=(0,), exts=(), ext_block=True): + fields = b"\x03\x03" + bytes(range(32)) + b"\x00" + fields += be16(len(suites_bytes)) + suites_bytes + fields += bytes([len(comps)]) + bytes(comps) + if ext_block: + block = b"" + for t, v in exts: + block += ext_bytes(t, v) + fields += be16(len(block)) + block + body = bytes([1]) + be24(len(fields)) + fields + return bytes([22, 3, 1]) + be16(len(body)) + body + + +def named_cases(): + """(name, bytes, expected: True accept / False reject).""" + cases = [] + cases.append(("full TLS 1.3 style hello", FULL_HELLO, True)) + cases.append(("minimal hello, supported versions only", + MIN_HELLO, True)) + cases.append(("duplicate extension type", + build_hello(exts=[(43, sv_value([0x0304])), + (43, sv_value([0x0303]))]), + False)) + cases.append(("duplicate key share group", + build_hello(exts=[(51, ks_value( + [(29, b"\x01" * 32), (29, b"\x02" * 32)]))]), + False)) + overrun_block = be16(0) + be16(10) + b"\x02\x03\x04" + fields = b"\x03\x03" + bytes(range(32)) + b"\x00" + fields += be16(2) + b"\x13\x01" + b"\x01\x00" + fields += be16(len(overrun_block)) + overrun_block + body = bytes([1]) + be24(len(fields)) + fields + cases.append(("extension length overrunning the block", + bytes([22, 3, 1]) + be16(len(body)) + body, + False)) + cases.append(("record length longer than the input", + build_hello(record_len_delta=5), False)) + cases.append(("handshake length not matching the body", + build_hello(hs_len_delta=1), False)) + bad = bytearray(MIN_HELLO) + bad[0] = 23 + cases.append(("content type 23", bytes(bad), False)) + bad = bytearray(MIN_HELLO) + bad[5] = 2 + cases.append(("handshake type 2", bytes(bad), False)) + cases.append(("session id length 33", + build_hello(session_id=b"\x07" * 33), False)) + cases.append(("odd cipher suite length", + raw_fields(b"\x13\x01\x13"), False)) + cases.append(("empty cipher suites", + build_hello(suites=()), False)) + cases.append(("compression methods without 0", + build_hello(comps=(1, 2)), False)) + cases.append(("missing extensions block", + build_hello(ext_block=False), False)) + cases.append(("supported versions odd length", + build_hello(exts=[(43, bytes([3, 3, 4, 3]))]), + False)) + cases.append(("supported versions length zero", + build_hello(exts=[(43, bytes([0]))]), False)) + cases.append(("ALPN empty name", + build_hello(exts=[(16, be16(1) + b"\x00")]), + False)) + alpn_bad = be16(9) + alpn_value([b"h2"])[2:] + cases.append(("ALPN list length mismatch", + build_hello(exts=[(16, alpn_bad)]), False)) + cases.append(("ALPN empty list", + build_hello(exts=[(16, alpn_value([]))]), + False)) + cases.append(("SNI second host_name entry", + build_hello(exts=[(0, sni_value( + [(0, b"a.example"), (0, b"b.example")]))]), + False)) + sni_bad = be16(99) + sni_value([(0, b"example.com")])[2:] + cases.append(("SNI list length mismatch", + build_hello(exts=[(0, sni_bad)]), False)) + cases.append(("SNI empty list", + build_hello(exts=[(0, sni_value([]))]), + False)) + cases.append(("key share empty key bytes", + build_hello(exts=[(51, ks_value([(29, b"")]))]), + False)) + cases.append(("key share empty list", + build_hello(exts=[(51, ks_value([]))]), + False)) + cases.append(("trailing garbage after the record", + build_hello(trailing=b"\x00"), False)) + cases.append(("empty extensions block, length 0, accepted", + EMPTY_EXT_HELLO, True)) + cases.append(("record length zero", + bytes([22, 3, 1, 0, 0]), False)) + cases.append(("input shorter than the record header", + bytes([22, 3]), False)) + cases.append(("empty input", b"", False)) + return cases + + +# ---------------------------------------------------------------- +# The generated differential cases. +# ---------------------------------------------------------------- + +HOSTS = [b"example.com", b"a.b.example.org", b"x", b"host-name.example"] + + +def gen_sni(rng, defect): + entries = [(0, rng.choice(HOSTS))] + if rng.random() < 0.3: + entries.append((rng.choice([1, 2, 3, 17]), + bytes(rng.randrange(256) + for _ in range(rng.randrange(1, 6))))) + if defect == "sni-second-host": + entries.append((0, b"other.example")) + if defect == "sni-dup-type": + entries.append((entries[-1][0], b"zz")) + if defect == "sni-empty-host": + entries[0] = (0, b"") + v = sni_value(entries) + if defect == "sni-list-len": + v = be16(len(v)) + v[2:] + return (0, v) + + +def gen_alpn(rng, defect): + names = [bytes(rng.choice(b"abcdefg0123456789/.-") + for _ in range(rng.randrange(1, 9))) + for _ in range(rng.randrange(1, 4))] + if defect == "alpn-empty-name": + names.insert(0, b"") + v = alpn_value(names) + if defect == "alpn-list-len": + v = be16(len(v) + 2) + v[2:] + return (16, v) + + +def gen_sv(rng, defect): + versions = [rng.choice([0x0300, 0x0301, 0x0302, 0x0303, + 0x0304, 0x7F1C]) + for _ in range(rng.randrange(1, 5))] + if defect == "sv-odd": + return (43, bytes([3, 3, 4, 3])) + if defect == "sv-zero": + return (43, bytes([0])) + if defect == "sv-len-lie": + v = sv_value(versions) + return (43, bytes([v[0] + 2]) + v[1:]) + return (43, sv_value(versions)) + + +def gen_ks(rng, defect): + groups = rng.sample([29, 23, 24, 25, 256, 257], + rng.randrange(1, 4)) + shares = [(g, bytes(rng.randrange(256) + for _ in range(rng.choice([1, 32, 65])))) + for g in groups] + if defect == "ks-dup-group": + shares.append((shares[0][0], b"\x09" * 8)) + if defect == "ks-empty-key": + shares[0] = (shares[0][0], b"") + v = ks_value(shares) + if defect == "ks-list-len": + v = be16(len(v)) + v[2:] + return (51, v) + + +def gen_opaque(rng, taken): + choices = [t for t in [5, 10, 11, 13, 21, 23, 35, 42, 44, + 45, 49, 50, 300, 1000, 65281] + if t not in taken] + t = rng.choice(choices) + v = bytes(rng.randrange(256) + for _ in range(rng.choice([0, 1, 4, 17, 40]))) + return (t, v) + + +DEFECTS = [None, None, None, "dup-ext", "no-ext-block", + "trailing", "rec-len", "hs-len", "sess33", + "suites-empty", "comps-no-null", "comps-empty", + "sni-second-host", "sni-dup-type", "sni-empty-host", + "sni-list-len", "alpn-empty-name", "alpn-list-len", + "sv-odd", "sv-zero", "sv-len-lie", "ks-dup-group", + "ks-empty-key", "ks-list-len"] + + +def gen_message(rng): + defect = rng.choice(DEFECTS) + session_id = bytes(rng.randrange(256) + for _ in range(rng.choice([0, 0, 1, 8, 32]))) + if defect == "sess33": + session_id = bytes(33) + nsuites = rng.choice([1, 1, 2, 3, 4, 6]) + if defect == "suites-empty": + nsuites = 0 + suites = [rng.randrange(65536) for _ in range(nsuites)] + comps = [0] + if rng.random() < 0.3: + comps = [0, 1] + if defect == "comps-no-null": + comps = [1, 2] + if defect == "comps-empty": + comps = [] + builders = [gen_sni, gen_alpn, gen_sv, gen_ks] + rng.shuffle(builders) + nexts = rng.randrange(0, 5) + chosen = builders[:nexts] + exts = [] + taken = set() + for b in chosen: + e = b(rng, defect) + exts.append(e) + taken.add(e[0]) + if rng.random() < 0.5: + e = gen_opaque(rng, taken) + exts.insert(rng.randrange(len(exts) + 1), e) + taken.add(e[0]) + if defect == "dup-ext" and exts: + exts.append(exts[0]) + rng.shuffle(exts) + return build_hello( + record_version=bytes([rng.randrange(256), + rng.randrange(256)]), + legacy_version=bytes([rng.randrange(256), + rng.randrange(256)]), + random_bytes=bytes(rng.randrange(256) for _ in range(32)), + session_id=session_id, suites=suites, comps=comps, + exts=exts, ext_block=(defect != "no-ext-block"), + record_len_delta=(5 if defect == "rec-len" else 0), + hs_len_delta=(1 if defect == "hs-len" else 0), + trailing=(b"\xaa" if defect == "trailing" else b"")) + + +def gen_mutations(rng): + out = [] + for i in range(len(FULL_HELLO)): + out.append(FULL_HELLO[:i]) + for i in range(len(FULL_HELLO)): + for d in (0x01, 0x80, 0xFF): + b = bytearray(FULL_HELLO) + b[i] ^= d + out.append(bytes(b)) + for _ in range(300): + b = bytearray(FULL_HELLO) + for _ in range(rng.randrange(1, 9)): + op = rng.randrange(3) + pos = rng.randrange(len(b) + (1 if op == 1 else 0)) + if op == 0 and b: + b[pos % len(b)] = rng.randrange(256) + elif op == 1: + b.insert(pos, rng.randrange(256)) + elif op == 2 and b: + del b[pos % len(b)] + out.append(bytes(b)) + return out + + +def gen_random_raw(rng): + out = [] + for _ in range(300): + n = rng.randrange(0, 320) + b = bytes(rng.randrange(256) for _ in range(n)) + if n > 0 and rng.random() < 0.5: + b = bytes([22]) + b[1:] + out.append(b) + return out + + +# ---------------------------------------------------------------- +# The runner. +# ---------------------------------------------------------------- + +def run_batch(lines, timeout=120): + """Run the tool on request lines; return answer lines.""" + proc = subprocess.Popen( + [str(EXE)], stdin=subprocess.PIPE, stdout=subprocess.PIPE, + stderr=subprocess.PIPE) + out_lines = [] + err = [] + + def drain(): + try: + data = proc.stdout.read() + out_lines.extend(data.decode().splitlines()) + except Exception: + pass + + t = threading.Thread(target=drain, daemon=True) + t.start() + try: + proc.stdin.write(("\n".join(lines) + "\n").encode()) + proc.stdin.close() + except BrokenPipeError: + pass + t.join(timeout) + if t.is_alive(): + proc.kill() + raise TimeoutError("tool did not finish in time") + err = proc.stderr.read().decode() + if err.strip(): + raise RuntimeError(f"tool wrote to stderr: {err[:400]}") + return out_lines + + +def codes(bs): + return ",".join(str(b) for b in bs) + + +def expected_answer(bs): + rep = oracle_parse(bs) + if rep is None: + return "none" + return "ok:" + codes(rep) + + +def check_batch(cases, label, failures): + """cases: list of byte strings. Returns (run, agreed).""" + lines = [] + for bs in cases: + if bs: + lines.append("parse " + codes(bs)) + else: + lines.append("parse") + answers = [] + chunk = 400 + for i in range(0, len(lines), chunk): + answers.extend(run_batch(lines[i:i + chunk])) + if len(answers) != len(cases): + failures.append( + f"{label}: got {len(answers)} answers for " + f"{len(cases)} cases") + return len(cases), 0 + agreed = 0 + for bs, got in zip(cases, answers): + want = expected_answer(bs) + if got == want: + agreed += 1 + elif len(failures) < 25: + failures.append( + f"{label}: input {codes(bs)[:120]}... " + f"tool said {got[:80]}, oracle said {want[:80]}") + return len(cases), agreed + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument("--seed", type=int, default=20261026) + ap.add_argument("--count", type=int, default=3200) + args = ap.parse_args() + rng = random.Random(args.seed) + + env = dict(os.environ) + if not any(Path(p, "lake").exists() + for p in env.get("PATH", "").split(":")): + env["PATH"] = (str(Path.home() / ".elan" / "bin") + + ":" + env.get("PATH", "")) + build = subprocess.run( + ["lake", "build"], cwd=ROOT, capture_output=True, + text=True, timeout=1200, env=env) + if build.returncode != 0: + print(build.stdout[-2000:]) + print(build.stderr[-2000:]) + print("lake build failed", file=sys.stderr) + return 1 + + failures = [] + tally = {} + + named = named_cases() + agreed_named = 0 + named_lines = [] + named_want = [] + for name, bs, want_ok in named: + rep = oracle_parse(bs) + oracle_ok = rep is not None + if oracle_ok != want_ok: + failures.append( + f"named case {name}: oracle " + f"{'accepts' if oracle_ok else 'rejects'}, " + f"the case expects " + f"{'accept' if want_ok else 'reject'}") + named_lines.append(bs) + named_want.append(name) + n, a = check_batch(named_lines, "named", failures) + tally["named cases"] = (n, a) + + gen = [gen_message(rng) for _ in range(args.count)] + n, a = check_batch(gen, "generated", failures) + tally["generated messages"] = (n, a) + gen_accepted = sum(1 for bs in gen + if oracle_parse(bs) is not None) + + mut = gen_mutations(rng) + n, a = check_batch(mut, "mutations", failures) + tally["mutations of the full hello"] = (n, a) + + raw = gen_random_raw(rng) + n, a = check_batch(raw, "random raw", failures) + tally["random raw byte strings"] = (n, a) + + malformed = ["parse 256", "parse 1,x", "parse 1,,2", + "peek 1,2", "parse -1", "parse 1 2", + "parse 999999999999"] + bad_agreed = 0 + for line in malformed: + got = run_batch([line]) + if got == ["error"]: + bad_agreed += 1 + else: + failures.append( + f"malformed line {line!r}: got {got}") + tally["malformed request lines"] = (len(malformed), + bad_agreed) + + total = sum(n for n, _ in tally.values()) + agreed = sum(a for _, a in tally.values()) + + lines = [] + lines.append("# ClientHello slice: test results") + lines.append("") + lines.append(f"Run: python3 tests/run_tests.py " + f"--seed {args.seed} --count {args.count}") + lines.append(f"Seed: {args.seed}. " + f"Python {platform.python_version()}.") + lines.append("") + lines.append("## Oracles") + lines.append("") + lines.append("Every verdict is settled by the harness " + "oracle, a Python implementation of the rules " + "in SPEC.md written for these tests. The tool " + "must agree with the oracle on every input, " + "and an accepted message must reprint to the " + "oracle's canonical reprint byte for byte.") + lines.append("") + lines.append("Python's ssl module cannot build a " + "ClientHello on demand. Go is not installed " + "(`go version` fails). Scapy 2.8.0 is present " + "in the sibling dhcp project's venv and its " + "TLS submodules import, but building or " + "dissecting a TLS record raises NameError " + "inside scapy's crypto support (HMAC is not " + "defined), so Scapy could not be used as a " + "byte source. No capture was fetched; the " + "fixed cases are built by hand from the RFCs.") + lines.append("") + lines.append("## Counts") + lines.append("") + lines.append("| part | run | agreed |") + lines.append("| --- | --- | --- |") + for label, (n, a) in tally.items(): + lines.append(f"| {label} | {n} | {a} |") + lines.append(f"| total | {total} | {agreed} |") + lines.append("") + lines.append(f"Of the {tally['generated messages'][0]} " + f"generated messages, the oracle accepts " + f"{gen_accepted} and rejects " + f"{tally['generated messages'][0] - gen_accepted}.") + lines.append("") + lines.append("## Named cases") + lines.append("") + for name, bs, want_ok in named: + lines.append(f"- {name}: " + f"{'accept' if want_ok else 'reject'} " + f"({len(bs)} bytes)") + lines.append("") + lines.append("## Differences") + lines.append("") + if failures: + lines.append(f"{len(failures)} failure(s):") + lines.append("") + for f in failures: + lines.append(f"- {f}") + else: + lines.append("No disagreements between the tool and " + "the oracle, and every named case matched " + "its stated expectation.") + lines.append("") + RESULTS.write_text("\n".join(lines)) + print(f"run {total}, agreed {agreed}, " + f"failures {len(failures)}") + for f in failures: + print("FAIL:", f) + return 0 if not failures else 1 + + +if __name__ == "__main__": + sys.exit(main())