Repository navigation
tls: refuse a compatibility CCS inside a fragmented handshake message - #8
Merged
Merged
Conversation
RFC 8446 §5.1: handshake messages MUST NOT be interleaved with other record types. Specify that a compatibility CCS is dropped only at a handshake message boundary, state the record-level contract, and add a certified mutation for dropping it mid-message. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
…ssage RFC 8446 §5.1: drop the CCS only when the reassembler is at a message boundary; otherwise fail with unexpected_message. The proof refines receive_compatibility_ccs through ccs_record_ensures. The test that asserted the old drop now expects the refusal, and a second test keeps the boundary case dropped. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
- framing: `is_empty_mode`'s mode argument is spec-only, so take it as `Ghost<bool>` (the pattern clazel-fetch uses) instead of an unused bool. - bootstrap: use `?` for the ClientHello start result (clippy::question_mark). - hello_bootstrap tests: checked `get` instead of slicing, and rustfmt. hello::bootstrap's proof does not pass before or after this change (assertion failures and an rlimit in its feed path); that is untouched here. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This was referenced Oct 26, 2026
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
atiernan
marked this pull request as ready for review
October 27, 2026 07:13
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Fixes review finding 7 from #1. RFC 8446 §5.1 says handshake messages "MUST NOT be interleaved with other record types", but the connection dispatcher dropped a compatibility ChangeCipherSpec that arrived between two fragments of one handshake message. It now drops one only at a message boundary; inside a message it fails with
unexpected_message.This PR's base is
phase3/tls-handover: the 19 unpushed commits from localphase3/tlsplus the previous agent's uncommitted work, preserved as one WIP commit (0c3b7ef). See the TLS takeover plan, step 0.Commits
4c1c29fspec:compatibility_ccs_dropped/receive_compatibility_ccs(dispatcher_spec),ccs_record_ensures(dispatcher_contract),lemma_compatibility_ccs_not_dropped_mid_message, and mutationdispatcher-ccs-dropped-mid-message(expect: killed).c7589a8fix:exec.rsFrame::Ccsarm requiresreassembler.at_message_boundary(). In the tests, the old test asserted the buggy drop, so it is replaced, and a new test covers the boundary case.23a5910style: clears clippy/fmt failures that the WIP commit brought in (framing.rsunused argument →Ghost<bool>,?inbootstrap.rs, checkedgetintests/hello_bootstrap.rs).Local results (per module, not a full verify)
connection::exec: 31 verified, 0 errors.connection::dispatcher_lemmas: 4 verified, 0 errors.connection::framing: 10 verified, 0 errors.cargo xtask mutatehas not been run.cargo test -p clazel-tlspasses. Strict clippy andcargo fmt --checkare clean forclazel-tls.Known failing (from the WIP base, not this PR)
hello::bootstrapdoes not verify, with or without this PR: assertion failures at about lines 395, 419 and 478, plus an rlimit in the function at about line 435. CI'sclazel-tlscrate job will fail on it.hello::bootstrap(spec line ~175, andtests/hello_bootstrap.rs) still drops a CCS between ServerHello fragments, citing RFC 8446 §5's "MUST simply drop it". That contradicts this fix. The two sections conflict for this case, so it needs one reading for the whole crate and adocs/ERRATA.mdentry.clazel-tlsstays at tier 0. Full verification has not run yet.🤖 Generated with Claude Code