From e1bb4c1e0f31ee19fb99adecee4f7dae7f8f18b5 Mon Sep 17 00:00:00 2001 From: Orda Date: Wed, 11 Nov 2026 13:35:58 -0600 Subject: [PATCH 1/3] Add initial configuration in bar.toml --- bar.toml | 15 +++++++++++++++ 1 file changed, 15 insertions(+) create mode 100644 bar.toml diff --git a/bar.toml b/bar.toml new file mode 100644 index 0000000..444c92a --- /dev/null +++ b/bar.toml @@ -0,0 +1,15 @@ +[project] +name = "http" +status = "in-progress" +page = "README.md" +spec_authors = ["ahrazzle"] +entry_points = ["Main.lean"] + +[spec] +files = ["SPEC.md", "Http/Types.lean", "Http/Spec/Defs.lean", "Http/Spec.lean"] +code = ["Http.Types", "Http.Framing", "Http"] + +[tests] +results = "tests/TEST-RESULTS.md" +command = ["python3", "tests/run_tests.py"] +files = ["tests/run_tests.py", "tests/planted_bugs.py", "tests/PLANTED-BUGS.md"] From a4481889a496b60958a88db24f0143d4876f65b7 Mon Sep 17 00:00:00 2001 From: Orda Date: Wed, 11 Nov 2026 13:38:56 -0600 Subject: [PATCH 2/3] Add HTTP/1.1 Message Framing and Chunked Transfer Coding spec This document outlines the rules for parsing and framing HTTP/1.x request messages, including line termination, request-line parsing, header section validation, message body framing, and chunked transfer coding. --- SPEC.md | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) create mode 100644 SPEC.md diff --git a/SPEC.md b/SPEC.md new file mode 100644 index 0000000..608fcae --- /dev/null +++ b/SPEC.md @@ -0,0 +1,22 @@ +# HTTP/1.1 Message Framing and Chunked Transfer Coding (`Http`) + +This specification defines the wire-level rules for parsing and framing an HTTP/1.x request message from a byte stream under RFC 9112 (HTTP/1.1) and RFC 9110 (HTTP Semantics), taking the strict reading wherever lenient parsers permit request-boundary disagreement. + +## Scope + +1. **Line Termination (`splitCRLF`)**: Every start-line, header field line, chunk-size line, chunk-data record, and trailer section MUST end with `CRLF` (`0x0D 0x0A`). Any bare `CR` (`0x0D` not followed by `0x0A`) or bare `LF` (`0x0A` not preceded by `0x0D`) inside a line is rejected (`none`). +2. **Request-Line (`parseRequestLine`, RFC 9112 Section 3)**: Must split on single `SP` (`0x20`) into three components `method SP request-target SP HTTP-version`. Runs of multiple spaces, `HTAB`, or control characters are rejected. `method` is `1*tchar`; `request-target` is `1*VCHAR`; `HTTP-version` is `HTTP/1.1` or `HTTP/1.0`. +3. **Header Section (`parseHeaders`, RFC 9112 Section 5)**: + - Obsolete line folding (`obs-fold`, lines beginning with `SP` or `HTAB`, Section 5.2) is rejected. + - Whitespace between `field-name` and `:` (Section 5.1) is rejected; `field-name` must satisfy `1*tchar`. + - Leading and trailing optional whitespace (`OWS`: `SP` / `HTAB`) around `field-value` is stripped; interior bytes must satisfy RFC 9110 Section 5.5 (`field-vchar` or `OWS`, no `NUL` or control octets). +4. **Message Body Framing (`determineFraming`, RFC 9112 Sections 6.1-6.3)**: + - **Combined `Transfer-Encoding` and `Content-Length` (Sections 6.1 / 6.3)**: Unconditionally rejected to prevent `CL.TE` and `TE.CL` boundary ambiguity. + - **`Transfer-Encoding` in `HTTP/1.0` (Section 6.1, EEF-CVE-2026-94194)**: Unconditionally rejected. + - **Transfer-Coding List (Sections 6.1 / 6.3, EEF-CVE-2026-94194)**: Tokenized across comma-separated values; empty elements, non-token characters, repeated `chunked`, or non-final `chunked` (`Transfer-Encoding: chunked, gzip`) are rejected. Only `[chunked]` (case-insensitively) selects chunked framing in this slice. + - **`Content-Length` (Section 6.2 / RFC 9110 Section 8.6)**: Duplicate `Content-Length` header fields are rejected; a single `Content-Length` value must match `1*DIGIT` (`< 2^64`, no `+`, `-`, or comma list). + - **Default**: Requests with neither `Transfer-Encoding` nor `Content-Length` have a zero-byte body (`fixed 0`). +5. **Chunked Transfer Coding (`decodeChunked`, RFC 9112 Section 7.1)**: + - `chunk-size` is `1*HEXDIG` (`< 2^64`). Optional chunk extensions after `;` must contain only `OWS` and `field-vchar`. + - Every non-zero chunk payload of `sz` bytes MUST be followed immediately by `0x0D 0x0A` (`CRLF`); non-CRLF terminators (CVE-2025-23167 class) are rejected. + - The terminating `0` chunk is followed by an optional RFC 9112 Section 7.1.2 trailer section (`*( field-line CRLF )`) and final `CRLF`. From e8920cc5a5af399c1ecf9226981835aa7b6edcc6 Mon Sep 17 00:00:00 2001 From: Orda Date: Wed, 11 Nov 2026 13:40:07 -0600 Subject: [PATCH 3/3] Enhance README with library details and theorems Expanded README to include detailed library specifications, planned theorems, and unproven aspects. --- README.md | 33 +++++++++++++++++++++++++++++++-- 1 file changed, 31 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index 2da4a73..955e541 100644 --- a/README.md +++ b/README.md @@ -1,2 +1,31 @@ -# http -lean HTTP request-line and header parser (RFC 9112) +# http: HTTP/1.1 request framing and chunked decoding, proved + +This library specifies, frames, and serializes HTTP/1.x request messages in Lean 4 following RFC 9112 (Sections 2, 3, 5, 6, and 7.1), targeting machine-checked theorems for prefix-free stream framing and rejection of HTTP request-boundary ambiguities (`CL.TE`, `TE.CL`, `TE.TE`, `HTTP/1.0` `Transfer-Encoding`, and malformed chunk terminators). + +Status: in progress. The specification has not yet been approved by an independent reviewer on the org's list, so this is not yet verified. + +## Planned and Drafted Theorems (`Http.Spec` / `Http.Proofs`) + +| Claim | Theorem | +| :--- | :--- | +| `splitCRLF` splits at the earliest `CRLF` with no bare `CR` or `LF` in the line. | `Http.Spec.splitCRLF_sound` | +| `splitCRLF` is prefix-free when trailing pipelined bytes are appended. | `Http.Spec.splitCRLF_prefix_free` | +| Decimal formatting of numbers below `2^64` parses back to the same number. | `Http.Spec.parseDec_printDec` | +| Hexadecimal formatting of numbers below `2^64` parses back to the same number. | `Http.Spec.parseHex_printHex` | +| Body framing resolution assigns at most one framing mode to any header list. | `Http.Spec.determineFraming_disjoint` | +| Requests carrying both `Transfer-Encoding` and `Content-Length` are always rejected. | `Http.Spec.determineFraming_rejects_cl_and_te` | +| `HTTP/1.0` requests carrying `Transfer-Encoding` are always rejected (EEF-CVE-2026-94194). | `Http.Spec.determineFraming_rejects_http10_te` | +| Chunked framing requires `HTTP/1.1` and zero `Content-Length` headers. | `Http.Spec.determineFraming_rejects_nonfinal_chunked` | +| `encodeChunked` round-trips through `decodeChunked` with empty remainder. | `Http.Spec.decodeChunked_encodeChunked` | +| `decodeChunked` is prefix-free across pipelined TCP byte streams. | `Http.Spec.decodeChunked_prefix_free` | +| Canonical fixed-length request serialization round-trips through `parseRequest`. | `Http.Spec.parseRequest_serializeFixed` | +| Canonical chunked request serialization round-trips through `parseRequest`. | `Http.Spec.parseRequest_serializeChunked` | +| `parseRequest` is prefix-free when pipelined bytes follow on the TCP stream. | `Http.Spec.parseRequest_prefix_free` | +| Multi-message TCP streams decompose uniquely under `StreamFrames`. | `Http.Spec.parseRequest_stream_unique` | +| Normative RFC 9112 / CVE boundary-ambiguity vectors are rejected. | `Http.Spec.reject_smuggling_vectors` | + +## What is not proved + +- Hex CLI decoding/encoding in `Main.lean` (covered by differential tests). +- HTTP response framing (`1xx`, `204`, `304`, and `HEAD` bodyless response rules in RFC 9112 Section 6.3). +- Content-coding decompression (`gzip`, `deflate`, `br`) and TLS / socket I/O.