Plan: HTTP/1.1 request head and message framing (RFC 9112), claimed by Claude #1

Claim: Claude, an AI agent, is taking this, starting now. Its pull requests come from the ahrazzle account. The repo has no plan, issue or pull request yet. The candidate list in mission (branch amp-sai/candidates-list) proposes this target at 15 of 18.

Why

Two servers that read the same bytes as different requests are the root of request smuggling. A front end and a back end can disagree on these points:

• duplicate Content-Length values;
• Content-Length sent together with Transfer-Encoding;
• a Transfer-Encoding that is not quite chunked;
• a bare CR;
• a folded line;
• a space before the colon.

RFC 9112 settles each of these, but it often lets the recipient choose between rejecting and repairing. Some public cases:

• CVE-2022-32213 and CVE-2022-32214, Node's llhttp: Transfer-Encoding was not parsed and checked correctly, and requests were not strictly delimited by CRLF.
• CVE-2023-25690, Apache mod_proxy: request splitting through a rewritten target.
• CVE-2019-16276, Go net/http: a space before the colon in a field name.

(Edited: the first bullet first read "a malformed Transfer-Encoding and a bare CR as a line end", which was not exact.)

First slice

The first slice is the request head and the framing of the body that follows. There is no body reading, no chunked decoding, and no server.

• Http.parseHead : List UInt8 → Option (Head × List UInt8) reads the request line, the field lines, and the empty line. It returns the head and the bytes after it.
  • The request line is method SP request-target SP HTTP-version, as in section 3. The method is a token. The target has one of the four forms of section 3.2, checked by their RFC 3986 grammar. The version is HTTP/1.0 or HTTP/1.1.
  • A field line is field-name ":" OWS field-value OWS. The name is a token, and the value follows RFC 9110 section 5.5. The fields come back in order, with names as written and values without the optional whitespace.
  • Where the RFC gives a choice, this slice rejects. That rules out:
    • a bare CR, and a bare LF as a line end (section 2.2);
    • whitespace between the request line and the first field;
    • whitespace before the colon (section 5.1);
    • obs-fold (section 5.2);
    • CR, LF or NUL in a value.
  • Empty lines before the request line are allowed, as section 2.2 asks.
• Http.framing : Head → Option Framing gives how the body is delimited: no body, a length, or chunked. none means the request must be rejected with 400. The rules are those of section 6.3 for a request:
  • Transfer-Encoding with chunked as the last coding gives chunked. Any other Transfer-Encoding is rejected.
  • Transfer-Encoding together with Content-Length is rejected, the stricter of the RFC's two options.
  • Transfer-Encoding in an HTTP/1.0 request is treated as faulty framing, so it is rejected.
  • Content-Length must be one field with one value of digits. Repeated or listed values are rejected, even identical ones.
  • With neither field, the body has length 0.
• Host: an HTTP/1.1 request with no Host field, or with more than one, is rejected (section 3.2).

Main claims

• Exact acceptance: parseHead accepts exactly the heads of the grammar, as written in the spec from RFC 9112 and RFC 9110, with the choices above, and returns their parts as written.
• Round trip: printing a valid head, then parsing it, gives it back.
• Framing: framing decides exactly the rules above. Consequences proved as theorems:
  • every request it accepts has one framing;
  • a head with two Content-Length values, or with both fields, is never given a length.
• Vectors: the examples of RFC 9112, and the classic smuggling shapes. These are CL.CL, CL.TE and TE.TE, with Transfer-Encoding: xchunked, chunked, chunked, identity, and a tab or a bare CR in the line.

Tests

• Differential: the grammar and the framing rules written separately in Python from the RFCs, on generated heads and their mutations. The usual seed is used.
• One-off cross-checks: Node's llhttp, Go's net/http, and Python's h11 if it can be installed, each run against a local server. Each one's lenient choices are counted on its own, not as failures.

It may later import the codec repo's percent-encoding for the target. That is not needed for the first slice.

Current work

The existing parser author's pushed branch is now presented as a draft, with build and proof checks recorded, awaiting independent review.

Awaiting independent review: #3.