From 57896d72e52746808990deaed87400f9afc3849f Mon Sep 17 00:00:00 2001 From: Alex Tiernan-Berry Date: Mon, 26 Oct 2026 15:47:38 +0000 Subject: [PATCH 1/4] spec(tls): bootstrap refuses a compatibility CCS inside a handshake message MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit RFC 8446 §5 (drop a CCS "at any time") and §5.1 (no record interleaved in a fragmented handshake message) conflict for a CCS between ServerHello fragments. Drop it only at a message boundary, as the connection dispatcher already does (#8); inside a message it is fatal with unexpected_message. BoringSSL and NSS also refuse it there. ERRATA entry added; not reported upstream. The implementation still drops it, so hello::bootstrap does not verify against this spec until the next commit. Co-Authored-By: Claude Opus 5.5 --- crates/clazel-tls/src/hello/bootstrap_spec.rs | 22 +++++++++++---- docs/ERRATA.md | 27 +++++++++++++++++++ 2 files changed, 44 insertions(+), 5 deletions(-) diff --git a/crates/clazel-tls/src/hello/bootstrap_spec.rs b/crates/clazel-tls/src/hello/bootstrap_spec.rs index aeddd688..15935ae4 100644 --- a/crates/clazel-tls/src/hello/bootstrap_spec.rs +++ b/crates/clazel-tls/src/hello/bootstrap_spec.rs @@ -13,6 +13,10 @@ //! - A nonempty legacy session ID requests compatibility mode. For an HRR, //! the client dummy CCS is prefixed to the CH2 flight as Appendix D.4 allows. //! Without HRR, the later protected-handshake driver owns that CCS. +//! - A valid unencrypted CCS is dropped only at a handshake message boundary +//! and is fatal (unexpected_message) inside a fragmented ServerHello or HRR: +//! §5 and §5.1 conflict there; see docs/ERRATA.md. The connection +//! dispatcher applies the same rule to protected handshake messages. //! - Authentication, key derivation, socket I/O, early data and PSK are outside //! this bootstrap model. #[allow(unused_imports)] @@ -172,11 +176,19 @@ pub open spec fn receive(hash: spec_fn(Seq) -> Seq, s: State, event: Pee recommends wf(s), s.mode == Mode::AwaitServerHello, { match event { - // RFC 8446 §5 specifically says to drop a valid unencrypted CCS - // without further processing at any time after the first ClientHello - // and before peer Finished. Therefore it does not enter reassembly, - // even when a fragmented handshake message is in progress. - PeerEvent::Ccs => (s, Action::None), + // RFC 8446 §5 says to drop a valid unencrypted CCS "at any time after + // the first ClientHello message has been sent or received and before + // the peer's Finished message has been received", but §5.1 says + // handshake messages "MUST NOT be interleaved with other record types". + // We drop it only at a handshake message boundary; inside a + // fragmented message it is fatal (docs/ERRATA.md, RFC 8446 §5). + PeerEvent::Ccs => if crate::spec::at_message_boundary(s.reassembly) { + (s, Action::None) + } else { + (State { mode: Mode::Failed, hello: None, pending_flight: seq![], + compatibility: s.compatibility, reassembly: s.reassembly }, + Action::Fail(crate::spec::UNEXPECTED_MESSAGE)) + }, PeerEvent::Error(alert) => (State { mode: Mode::Failed, hello: None, pending_flight: seq![], compatibility: s.compatibility, reassembly: s.reassembly }, Action::Fail(alert)), PeerEvent::Eof => (State { mode: Mode::Failed, hello: None, diff --git a/docs/ERRATA.md b/docs/ERRATA.md index ab021355..d0dd7455 100644 --- a/docs/ERRATA.md +++ b/docs/ERRATA.md @@ -194,3 +194,30 @@ it evidently means. Each entry records what we specified instead. such issue. - **Reported upstream:** not yet (RFC 9110, which obsoletes RFC 7230, already states the corrected rule). + +## RFC 8446 §5 and §5.1: a compatibility CCS inside a fragmented handshake message + +- **Spec:** RFC 8446 (August 2018), §5 "Record Protocol" and §5.1 "Record + Layer", +- **Text:** §5: "An implementation may receive an unencrypted record of type + change_cipher_spec consisting of the single byte value 0x01 at any time + after the first ClientHello message has been sent or received and before + the peer's Finished message has been received and MUST simply drop it + without further processing." §5.1: "Handshake messages MUST NOT be + interleaved with other record types. That is, if a handshake message is + split over two or more records, there MUST NOT be any other records + between them." +- **Problem:** a CCS record between two fragments of one handshake message + is covered by both. §5 says drop it; §5.1 says the peer may not send it. + The CCS exists only for middlebox compatibility (Appendix D.4), which has + the server send it immediately after its first handshake message, so it + evidently never needs to fall inside one. Implementations differ: + BoringSSL and NSS refuse a CCS inside a fragmented ServerHello, and after + ServerHello both drop one without checking for a message boundary. +- **We specify:** the §5 drop applies only at a handshake message boundary; + inside a fragmented message a CCS is fatal with `unexpected_message`. See + `receive` in `crates/clazel-tls/src/hello/bootstrap_spec.rs` (plaintext + ServerHello/HRR) and `compatibility_ccs_dropped` in + `crates/clazel-tls/src/connection/dispatcher_spec.rs` (protected + handshake). +- **Reported upstream:** not yet. From dd67840771bbd384ec99eadbf86634a7a6a674eb Mon Sep 17 00:00:00 2001 From: Alex Tiernan-Berry Date: Mon, 26 Oct 2026 15:50:30 +0000 Subject: [PATCH 2/4] fix(tls): bootstrap refuses a CCS inside a fragmented handshake message MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit RFC 8446 §5.1; see docs/ERRATA.md. The Ccs arm of handle_record and record_step now drop only at a message boundary, matching bootstrap_spec. Tests updated; adds the certificate lemma used by the next commit. Co-Authored-By: Claude Sonnet 5.5 --- crates/clazel-tls/src/hello/bootstrap.rs | 8 +++- .../clazel-tls/src/hello/bootstrap_lemmas.rs | 8 +++- crates/clazel-tls/src/hello/certificates.rs | 22 ++++++++++ crates/clazel-tls/tests/hello_bootstrap.rs | 42 +++++++++++-------- 4 files changed, 60 insertions(+), 20 deletions(-) diff --git a/crates/clazel-tls/src/hello/bootstrap.rs b/crates/clazel-tls/src/hello/bootstrap.rs index 1efcb6d8..ec20e4e1 100644 --- a/crates/clazel-tls/src/hello/bootstrap.rs +++ b/crates/clazel-tls/src/hello/bootstrap.rs @@ -442,8 +442,12 @@ impl Bootstrap { { match crate::record::read_record(wire, false) { ReadOut::Done(Frame::Ccs, rest) => { - if !rest.is_empty() { self.fail(crate::spec::UNEXPECTED_MESSAGE) } - else { Action::None } + // RFC 8446 §5.1: a CCS inside a fragmented handshake message + // is fatal; §5's drop applies only at a message boundary + // (docs/ERRATA.md, "RFC 8446 §5 and §5.1"). + if !rest.is_empty() || !self.reassembler.at_message_boundary() { + self.fail(crate::spec::UNEXPECTED_MESSAGE) + } else { Action::None } }, ReadOut::Done(Frame::Plain(typ, bytes), rest) => { if !rest.is_empty() { return self.fail(crate::spec::UNEXPECTED_MESSAGE); } diff --git a/crates/clazel-tls/src/hello/bootstrap_lemmas.rs b/crates/clazel-tls/src/hello/bootstrap_lemmas.rs index 2386627c..3e9198a6 100644 --- a/crates/clazel-tls/src/hello/bootstrap_lemmas.rs +++ b/crates/clazel-tls/src/hello/bootstrap_lemmas.rs @@ -144,7 +144,13 @@ pub open spec fn record_step(hash: spec_fn(Seq) -> Seq, s: super::bootst (terminal(s, Mode::Failed, s.reassembly), Action::Fail(crate::spec::UNEXPECTED_MESSAGE)) } else { match frame { - crate::spec::Frame::Ccs => (s, Action::None), + // RFC 8446 §5.1: dropped only at a message boundary (docs/ERRATA.md). + crate::spec::Frame::Ccs => if crate::spec::at_message_boundary(s.reassembly) { + (s, Action::None) + } else { + (terminal(s, Mode::Failed, s.reassembly), + Action::Fail(crate::spec::UNEXPECTED_MESSAGE)) + }, crate::spec::Frame::Plain(rec) if rec.ctype == crate::spec::CT_HANDSHAKE => fragment_step(hash, s, rec.fragment), crate::spec::Frame::Plain(rec) if rec.ctype == crate::spec::CT_ALERT => diff --git a/crates/clazel-tls/src/hello/certificates.rs b/crates/clazel-tls/src/hello/certificates.rs index 69c1e850..ae5a2bb3 100644 --- a/crates/clazel-tls/src/hello/certificates.rs +++ b/crates/clazel-tls/src/hello/certificates.rs @@ -50,4 +50,26 @@ pub proof fn lemma_legacy_server_hello_uses_protocol_version() ) == Some(crate::spec::PROTOCOL_VERSION)) by (compute_only); } +/// A hash that is irrelevant to a CCS event. +pub open spec fn empty_hash(_messages: Seq) -> Seq { seq![] } + +/// A bootstrap state awaiting ServerHello with `buf` already reassembled. +pub open spec fn awaiting_with_buffer(buf: Seq) -> super::bootstrap_spec::State { + super::bootstrap_spec::State { mode: super::bootstrap_spec::Mode::AwaitServerHello, + hello: None, pending_flight: seq![], compatibility: true, + reassembly: crate::spec::Reasm { buf } } +} + +/// RFC 8446 §5.1 (docs/ERRATA.md): a CCS inside a fragmented ServerHello is +/// fatal, while the same record at a message boundary is still dropped. +pub proof fn lemma_ccs_fatal_mid_message() + ensures + super::bootstrap_spec::receive(|m: Seq| empty_hash(m), awaiting_with_buffer(seq![1u8]), + super::bootstrap_spec::PeerEvent::Ccs).1 + == super::bootstrap_spec::Action::Fail(crate::spec::UNEXPECTED_MESSAGE), + super::bootstrap_spec::receive(|m: Seq| empty_hash(m), awaiting_with_buffer(seq![]), + super::bootstrap_spec::PeerEvent::Ccs) + == (awaiting_with_buffer(seq![]), super::bootstrap_spec::Action::None), +{ +} } diff --git a/crates/clazel-tls/tests/hello_bootstrap.rs b/crates/clazel-tls/tests/hello_bootstrap.rs index f3634dde..16926c66 100644 --- a/crates/clazel-tls/tests/hello_bootstrap.rs +++ b/crates/clazel-tls/tests/hello_bootstrap.rs @@ -141,7 +141,7 @@ fn exact_send_ack_gates_peer_input_and_wrong_ack_is_terminal() -> Result<(), Str } #[test] -fn ccs_is_dropped_during_fragmented_server_hello_without_losing_prefix() -> Result<(), String> { +fn ccs_inside_fragmented_server_hello_is_unexpected_message() -> Result<(), String> { let (mut bootstrap, client_wire) = started(SESSION)?; ack_initial(&mut bootstrap, &client_wire)?; @@ -152,27 +152,35 @@ fn ccs_is_dropped_during_fragmented_server_hello_without_losing_prefix() -> Resu assert_eq!(consumed, first_record.len()); assert!(matches!(first_action, Action::None)); - // RFC 8446 §5 specifically requires dropping a valid unencrypted CCS - // between ClientHello and peer Finished, including during reassembly. + // RFC 8446 §5 says to drop a CCS at any time, but §5.1 forbids any other + // record between fragments of one handshake message. Inside a message the + // CCS is fatal (docs/ERRATA.md); it is dropped only at a boundary. let dummy_ccs = [20, 3, 3, 0, 1, 1]; let (consumed, ccs_action) = bootstrap.feed(&dummy_ccs); assert_eq!(consumed, dummy_ccs.len()); - assert!(matches!(ccs_action, Action::None)); + assert!(matches!(ccs_action, Action::Fail(UNEXPECTED_MESSAGE))); + // The failure is terminal: the remaining fragment is not accepted. let last_record = plaintext(22, hello.get(split..).ok_or("missing last fragment")?); - let (consumed, final_action) = bootstrap.feed(&last_record); - assert_eq!(consumed, last_record.len()); - let established = match final_action { - Action::Established(established) => established, - _ => return Err("fragmented final ServerHello was not accepted".to_owned()), - }; - let (accepted_config, transcript, peer_key) = established.into_parts(); - assert_eq!(accepted_config.host, HOST); - assert_eq!(peer_key, SERVER_KEY); - assert_eq!( - transcript.phase(), - clazel_tls::transcript::spec::Phase::Handshake - ); + let (_, final_action) = bootstrap.feed(&last_record); + assert!(!matches!(final_action, Action::Established(_))); + Ok(()) +} + +#[test] +fn ccs_at_message_boundary_before_server_hello_is_dropped() -> Result<(), String> { + let (mut bootstrap, client_wire) = started(SESSION)?; + ack_initial(&mut bootstrap, &client_wire)?; + + let dummy_ccs = [20, 3, 3, 0, 1, 1]; + let (consumed, ccs_action) = bootstrap.feed(&dummy_ccs); + assert_eq!(consumed, dummy_ccs.len()); + assert!(matches!(ccs_action, Action::None)); + + let hello = plaintext(22, &handshake(2, &server_hello(SESSION, false))); + let (consumed, action) = bootstrap.feed(&hello); + assert_eq!(consumed, hello.len()); + assert!(matches!(action, Action::Established(_))); Ok(()) } From 923f001c37e26dce8f12d4410fbe021ae8a43364 Mon Sep 17 00:00:00 2001 From: Alex Tiernan-Berry Date: Mon, 26 Oct 2026 15:50:30 +0000 Subject: [PATCH 3/4] test(tls): mutation for a bootstrap CCS dropped mid-message Co-Authored-By: Claude Sonnet 5.5 --- crates/clazel-tls/mutations.json | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/crates/clazel-tls/mutations.json b/crates/clazel-tls/mutations.json index 5c8313d4..088a8a53 100644 --- a/crates/clazel-tls/mutations.json +++ b/crates/clazel-tls/mutations.json @@ -2352,6 +2352,20 @@ "witness": "super::dispatcher_spec::prepare_key_update(super::dispatcher_certificates::crypto(), super::dispatcher_certificates::ciphers(), super::dispatcher_certificates::sample_ready_state(), 2, false) != super::dispatcher_certificates::sample_ready_state()" } }, + { + "id": "bootstrap-ccs-dropped-mid-message", + "file": "src/hello/bootstrap_spec.rs", + "find": "PeerEvent::Ccs => if crate::spec::at_message_boundary(s.reassembly) {", + "replace": "PeerEvent::Ccs => if true {", + "expect": "killed", + "reason": "RFC 8446 \u00a75.1 forbids interleaving a handshake message with another record type: a CCS between two fragments of one ServerHello must be refused with unexpected_message, not dropped (docs/ERRATA.md).", + "module": "hello::mutation_certificates", + "certificate": { + "file": "src/hello/mutation_certificates.rs", + "lemma": "super::certificates::lemma_ccs_fatal_mid_message()", + "witness": "super::bootstrap_spec::receive(|m: Seq| super::certificates::empty_hash(m), super::certificates::awaiting_with_buffer(seq![1u8]), super::bootstrap_spec::PeerEvent::Ccs).1 == super::bootstrap_spec::Action::None" + } + }, { "id": "dispatcher-ccs-dropped-mid-message", "file": "src/connection/dispatcher_spec.rs", From 1f83f94549a63734232271c3bb28d012bba1a196 Mon Sep 17 00:00:00 2001 From: Alex Tiernan-Berry Date: Mon, 26 Oct 2026 21:15:58 +0000 Subject: [PATCH 4/4] test(tls): repair stale and mis-hosted proof mutations Point four mutations at the module holding their killing lemma (hello::certificates, auth::certificates) so they no longer survive. Retarget alert-closure-any-level (restore warning-only user_canceled), missing-version-only-sh (now legacy-server-hello-extensions-without-supported-versions), has-ext-first-only (re-certified through the legacy ServerHello predicate) and server-hello-extensions-floor (floor raised to 6; empty extension vector). New lemmas in hello::certificates and lemma_server_hello. Remove certificate-context: 8b04e0b deliberately dropped the generic parser's empty-context check; the initial-authentication rule now lives in auth::spec::initial_certificate_context_valid, covered by auth-initial-server-certificate-empty-context. Co-Authored-By: Claude Sonnet 5.5 --- crates/clazel-tls/mutations.json | 104 +++++++++----------- crates/clazel-tls/src/examples_hs.rs | 3 + crates/clazel-tls/src/hello/certificates.rs | 33 +++++++ 3 files changed, 81 insertions(+), 59 deletions(-) diff --git a/crates/clazel-tls/mutations.json b/crates/clazel-tls/mutations.json index 088a8a53..2510201e 100644 --- a/crates/clazel-tls/mutations.json +++ b/crates/clazel-tls/mutations.json @@ -451,15 +451,15 @@ { "id": "alert-closure-any-level", "file": "src/spec.rs", - "find": "a.description == CLOSE_NOTIFY || (a.description == USER_CANCELED && a.level == LEVEL_WARNING)", - "replace": "a.description == CLOSE_NOTIFY || a.description == USER_CANCELED", + "find": "a.description == CLOSE_NOTIFY || a.description == USER_CANCELED", + "replace": "a.description == CLOSE_NOTIFY || (a.description == USER_CANCELED && a.level == LEVEL_WARNING)", "expect": "killed", - "reason": "A fatal user_canceled is a closure: lemma_alert_closure is false.", + "reason": "Restores the old warning-only rule (TLS 1.3 §6.1 ignores the level): a fatal user_canceled is no longer a closure, so lemma_alert_closure is false.", "module": "examples", "certificate": { "file": "src/certificates.rs", "lemma": "super::examples::lemma_alert_closure()", - "witness": "alert_is_closure(Alert { level: 2, description: 90 })" + "witness": "!alert_is_closure(Alert { level: 2, description: 90 })" } }, { @@ -468,7 +468,7 @@ "find": "if t == EXT_SERVER_NAME {\n m is Ch || m is Ee", "replace": "if t == EXT_SERVER_NAME {\n m is Ch", "expect": "killed", - "reason": "The \u00a74.2 table row `server_name` is changed: lemma_ext_row_server_name is false.", + "reason": "The §4.2 table row `server_name` is changed: lemma_ext_row_server_name is false.", "module": "examples", "certificate": { "file": "src/certificates.rs", @@ -482,7 +482,7 @@ "find": "} else if t == EXT_STATUS_REQUEST {\n m is Ch || m is Cr || m is Ct", "replace": "} else if t == EXT_STATUS_REQUEST {\n m is Ch || m is Cr", "expect": "killed", - "reason": "The \u00a74.2 table row `status_request` is changed: lemma_ext_row_status_request is false.", + "reason": "The §4.2 table row `status_request` is changed: lemma_ext_row_status_request is false.", "module": "examples", "certificate": { "file": "src/certificates.rs", @@ -496,7 +496,7 @@ "find": "} else if t == EXT_SIGNATURE_ALGORITHMS {\n m is Ch || m is Cr", "replace": "} else if t == EXT_SIGNATURE_ALGORITHMS {\n m is Ch || m is Cr || m is Sh", "expect": "killed", - "reason": "The \u00a74.2 table row `signature_algorithms` is changed: lemma_ext_row_signature_algorithms is false.", + "reason": "The §4.2 table row `signature_algorithms` is changed: lemma_ext_row_signature_algorithms is false.", "module": "examples", "certificate": { "file": "src/certificates.rs", @@ -510,7 +510,7 @@ "find": "} else if t == EXT_PADDING {\n m is Ch", "replace": "} else if t == EXT_PADDING {\n m is Ch || m is Ee", "expect": "killed", - "reason": "The \u00a74.2 table row `padding` is changed: lemma_ext_row_padding is false.", + "reason": "The §4.2 table row `padding` is changed: lemma_ext_row_padding is false.", "module": "examples", "certificate": { "file": "src/certificates.rs", @@ -524,7 +524,7 @@ "find": "} else if t == EXT_KEY_SHARE {\n m is Ch || m is Sh || m is Hrr", "replace": "} else if t == EXT_KEY_SHARE {\n m is Ch || m is Sh", "expect": "killed", - "reason": "The \u00a74.2 table row `key_share` is changed: lemma_ext_row_key_share is false.", + "reason": "The §4.2 table row `key_share` is changed: lemma_ext_row_key_share is false.", "module": "examples", "certificate": { "file": "src/certificates.rs", @@ -538,7 +538,7 @@ "find": "} else if t == EXT_COOKIE {\n m is Ch || m is Hrr", "replace": "} else if t == EXT_COOKIE {\n m is Ch || m is Hrr || m is Sh", "expect": "killed", - "reason": "The \u00a74.2 table row `cookie` is changed: lemma_ext_row_cookie is false.", + "reason": "The §4.2 table row `cookie` is changed: lemma_ext_row_cookie is false.", "module": "examples", "certificate": { "file": "src/certificates.rs", @@ -552,7 +552,7 @@ "find": "} else if t == EXT_EARLY_DATA {\n m is Ch || m is Ee || m is Nst", "replace": "} else if t == EXT_EARLY_DATA {\n m is Ch || m is Ee", "expect": "killed", - "reason": "The \u00a74.2 table row `early_data` is changed: lemma_ext_row_early_data is false.", + "reason": "The §4.2 table row `early_data` is changed: lemma_ext_row_early_data is false.", "module": "examples", "certificate": { "file": "src/certificates.rs", @@ -566,7 +566,7 @@ "find": "} else if t == EXT_OID_FILTERS {\n m is Cr", "replace": "} else if t == EXT_OID_FILTERS {\n m is Cr || m is Ch", "expect": "killed", - "reason": "The \u00a74.2 table row `oid_filters` is changed: lemma_ext_row_oid_filters is false.", + "reason": "The §4.2 table row `oid_filters` is changed: lemma_ext_row_oid_filters is false.", "module": "examples", "certificate": { "file": "src/certificates.rs", @@ -580,7 +580,7 @@ "find": "} else if t == EXT_SUPPORTED_VERSIONS {\n m is Ch || m is Sh || m is Hrr", "replace": "} else if t == EXT_SUPPORTED_VERSIONS {\n m is Ch || m is Hrr", "expect": "killed", - "reason": "The \u00a74.2 table row `supported_versions` is changed: lemma_ext_row_supported_versions is false.", + "reason": "The §4.2 table row `supported_versions` is changed: lemma_ext_row_supported_versions is false.", "module": "examples", "certificate": { "file": "src/certificates.rs", @@ -594,7 +594,7 @@ "find": "} else if t == EXT_PRE_SHARED_KEY {\n m is Ch || m is Sh", "replace": "} else if t == EXT_PRE_SHARED_KEY {\n m is Ch || m is Sh || m is Hrr", "expect": "killed", - "reason": "The \u00a74.2 table row `pre_shared_key` is changed: lemma_ext_row_pre_shared_key is false.", + "reason": "The §4.2 table row `pre_shared_key` is changed: lemma_ext_row_pre_shared_key is false.", "module": "examples", "certificate": { "file": "src/certificates.rs", @@ -608,7 +608,7 @@ "find": "} else if t == EXT_SCT {\n m is Ch || m is Cr || m is Ct", "replace": "} else if t == EXT_SCT {\n m is Ch || m is Ct", "expect": "killed", - "reason": "The \u00a74.2 table row `signed_certificate_timestamp` is changed: lemma_ext_row_signed_certificate_timestamp is false.", + "reason": "The §4.2 table row `signed_certificate_timestamp` is changed: lemma_ext_row_signed_certificate_timestamp is false.", "module": "examples", "certificate": { "file": "src/certificates.rs", @@ -622,7 +622,7 @@ "find": "} else if t == EXT_CERTIFICATE_AUTHORITIES {\n m is Ch || m is Cr", "replace": "} else if t == EXT_CERTIFICATE_AUTHORITIES {\n m is Ch", "expect": "killed", - "reason": "The \u00a74.2 table row `certificate_authorities` is changed: lemma_ext_row_certificate_authorities is false.", + "reason": "The §4.2 table row `certificate_authorities` is changed: lemma_ext_row_certificate_authorities is false.", "module": "examples", "certificate": { "file": "src/certificates.rs", @@ -636,7 +636,7 @@ "find": "} else if t == EXT_SIGNATURE_ALGORITHMS_CERT {\n m is Ch || m is Cr", "replace": "} else if t == EXT_SIGNATURE_ALGORITHMS_CERT {\n m is Ch || m is Cr || m is Ct", "expect": "killed", - "reason": "The \u00a74.2 table row `signature_algorithms_cert` is changed: lemma_ext_row_signature_algorithms_cert is false.", + "reason": "The §4.2 table row `signature_algorithms_cert` is changed: lemma_ext_row_signature_algorithms_cert is false.", "module": "examples", "certificate": { "file": "src/certificates.rs", @@ -650,7 +650,7 @@ "find": "} else if t == EXT_ALPN {\n m is Ch || m is Ee", "replace": "} else if t == EXT_ALPN {\n m is Ch", "expect": "killed", - "reason": "The \u00a74.2 table row `alpn` is changed: lemma_ext_row_alpn is false.", + "reason": "The §4.2 table row `alpn` is changed: lemma_ext_row_alpn is false.", "module": "examples", "certificate": { "file": "src/certificates.rs", @@ -664,7 +664,7 @@ "find": "} else if t == EXT_SUPPORTED_GROUPS {\n m is Ch || m is Ee", "replace": "} else if t == EXT_SUPPORTED_GROUPS {\n m is Ch || m is Ee || m is Sh", "expect": "killed", - "reason": "The \u00a74.2 table row `supported_groups` is changed: lemma_ext_row_supported_groups is false.", + "reason": "The §4.2 table row `supported_groups` is changed: lemma_ext_row_supported_groups is false.", "module": "examples", "certificate": { "file": "src/certificates.rs", @@ -678,7 +678,7 @@ "find": "} else if t == EXT_PSK_KEY_EXCHANGE_MODES {\n m is Ch", "replace": "} else if t == EXT_PSK_KEY_EXCHANGE_MODES {\n m is Ch || m is Cr", "expect": "killed", - "reason": "The \u00a74.2 table row `psk_key_exchange_modes` is changed: lemma_ext_row_psk_key_exchange_modes is false.", + "reason": "The §4.2 table row `psk_key_exchange_modes` is changed: lemma_ext_row_psk_key_exchange_modes is false.", "module": "examples", "certificate": { "file": "src/certificates.rs", @@ -692,7 +692,7 @@ "find": "} else if t == EXT_POST_HANDSHAKE_AUTH {\n m is Ch", "replace": "} else if t == EXT_POST_HANDSHAKE_AUTH {\n m is Ch || m is Ee", "expect": "killed", - "reason": "The \u00a74.2 table row `post_handshake_auth` is changed: lemma_ext_row_post_handshake_auth is false.", + "reason": "The §4.2 table row `post_handshake_auth` is changed: lemma_ext_row_post_handshake_auth is false.", "module": "examples", "certificate": { "file": "src/certificates.rs", @@ -757,17 +757,17 @@ } }, { - "id": "missing-version-only-sh", + "id": "legacy-server-hello-extensions-without-supported-versions", "file": "src/spec.rs", - "find": "} else if (m is Sh || m is Hrr) && !has_ext(es, EXT_SUPPORTED_VERSIONS) {", - "replace": "} else if (m is Sh) && !has_ext(es, EXT_SUPPORTED_VERSIONS) {", + "find": "Some((es, rest)) => rest.len() == 0 && !has_ext(es, 43),", + "replace": "Some((es, rest)) => rest.len() == 0 && false,", "expect": "killed", - "reason": "A HelloRetryRequest without supported_versions is accepted: lemma_extension_checks is false.", - "module": "examples_hs", + "reason": "A ServerHello with a nonempty extension list lacking supported_versions is no longer recognised as legacy and falls to the generic parser, so it is not reported as protocol_version: lemma_legacy_server_hello_extensions_without_supported_versions is false.", + "module": "hello::certificates", "certificate": { - "file": "src/certificates.rs", - "lemma": "super::examples_hs::lemma_extension_checks()", - "witness": "check_extensions(Seq::::empty(), MsgKind::Hrr) != Some(ErrKind::MissingExtension)" + "file": "src/hello/mutation_certificates.rs", + "lemma": "super::certificates::lemma_legacy_server_hello_extensions_without_supported_versions()", + "witness": "super::spec::validate(Seq::empty(), false, super::certificates::legacy_server_hello_with_extensions(seq![0u8, 0, 0, 0])) != Err(crate::spec::PROTOCOL_VERSION)" } }, { @@ -776,12 +776,12 @@ "find": "es[0].etype == t || has_ext(es.skip(1), t)", "replace": "es[0].etype == t", "expect": "killed", - "reason": "supported_versions is only found in the first place: lemma_extension_checks is false.", - "module": "examples_hs", + "reason": "has_ext sees only the first extension, so a supported_versions after another extension is missed and the message is misclassified as a legacy ServerHello: lemma_supported_versions_found_after_other_extension is false.", + "module": "hello::certificates", "certificate": { - "file": "src/certificates.rs", - "lemma": "super::examples_hs::lemma_extension_checks()", - "witness": "check_extensions(seq![Ext { etype: 1234, data: seq![9u8] }, Ext { etype: 43, data: seq![3u8, 4] }], MsgKind::Sh) is Some" + "file": "src/hello/mutation_certificates.rs", + "lemma": "super::certificates::lemma_supported_versions_found_after_other_extension()", + "witness": "crate::spec::legacy_server_hello_without_supported_versions(super::certificates::legacy_server_hello_with_extensions(seq![0x12u8, 0x34, 0, 1, 9, 0, 0x2b, 0, 2, 3, 4]))" } }, { @@ -997,15 +997,15 @@ { "id": "server-hello-extensions-floor", "file": "src/spec.rs", - "find": "match read_exts(r5, 6, 65535) {", - "replace": "match read_exts(r5, 5, 65535) {", + "find": " match read_exts(r5, 0, 65535) {\n None => None,\n Some((exts, r6)) => {", + "replace": " match read_exts(r5, 6, 65535) {\n None => None,\n Some((exts, r6)) => {", "expect": "killed", - "reason": "A ServerHello whose extension block is 5 bytes is read: lemma_server_hello is false.", + "reason": "Raising the floor to 6 makes an empty extension vector a decode error: lemma_server_hello (an empty extension vector parses) is false.", "module": "examples_hs", "certificate": { "file": "src/certificates.rs", "lemma": "super::examples_hs::lemma_server_hello()", - "witness": "parse_handshake_body(2, super::examples_hs::sh_body(super::examples_hs::z32(), 0, seq![0u8, 5, 0x12, 0x34, 0, 1, 9]), 32) != Res::::Err(ErrKind::Decode)" + "witness": "!(parse_handshake_body(2, super::examples_hs::sh_body(super::examples_hs::z32(), 0, seq![0u8, 0]), 32) is Ok)" } }, { @@ -1022,20 +1022,6 @@ "witness": "parse_handshake(seq![11u8, 0, 0, 9, 0, 0, 0, 5, 0, 0, 0, 0, 0], 32) != Res::::Err(ErrKind::Decode)" } }, - { - "id": "certificate-context", - "file": "src/spec.rs", - "find": "if c.context.len() != 0 {", - "replace": "if c.context.len() > 1 {", - "expect": "killed", - "reason": "A server Certificate with a context of one byte is accepted: lemma_server_messages is false.", - "module": "examples_hs", - "certificate": { - "file": "src/certificates.rs", - "lemma": "super::examples_hs::lemma_server_messages()", - "witness": "parse_handshake(seq![11u8, 0, 0, 5, 1, 7, 0, 0, 0], 32) != Res::::Err(ErrKind::NonEmptyContext)" - } - }, { "id": "ticket-floor", "file": "src/spec.rs", @@ -2344,7 +2330,7 @@ "find": "if request > 1 || (is_response && request != 0)", "replace": "if request > 2 || (is_response && request != 0)", "expect": "killed", - "reason": "RFC 8446 \u00a74.6.3 restricts request_update to 0 or 1; the dispatcher must not queue an out-of-range KeyUpdate.", + "reason": "RFC 8446 §4.6.3 restricts request_update to 0 or 1; the dispatcher must not queue an out-of-range KeyUpdate.", "module": "connection::dispatcher_lemmas", "certificate": { "file": "src/connection/dispatcher_certificates.rs", @@ -2358,8 +2344,8 @@ "find": "PeerEvent::Ccs => if crate::spec::at_message_boundary(s.reassembly) {", "replace": "PeerEvent::Ccs => if true {", "expect": "killed", - "reason": "RFC 8446 \u00a75.1 forbids interleaving a handshake message with another record type: a CCS between two fragments of one ServerHello must be refused with unexpected_message, not dropped (docs/ERRATA.md).", - "module": "hello::mutation_certificates", + "reason": "RFC 8446 §5.1 forbids interleaving a handshake message with another record type: a CCS between two fragments of one ServerHello must be refused with unexpected_message, not dropped (docs/ERRATA.md).", + "module": "hello::certificates", "certificate": { "file": "src/hello/mutation_certificates.rs", "lemma": "super::certificates::lemma_ccs_fatal_mid_message()", @@ -2372,7 +2358,7 @@ "find": " && crate::spec::at_message_boundary(reassembly)\n}", "replace": " && true\n}", "expect": "killed", - "reason": "RFC 8446 \u00a75.1 forbids interleaving a handshake message with another record type: a compatibility CCS between two fragments of one handshake message must be refused, not dropped.", + "reason": "RFC 8446 §5.1 forbids interleaving a handshake message with another record type: a compatibility CCS between two fragments of one handshake message must be refused, not dropped.", "module": "connection::dispatcher_lemmas", "certificate": { "file": "src/connection/dispatcher_certificates.rs", @@ -2415,7 +2401,7 @@ "replace": "pub open spec fn initial_certificate_context_valid(context: Seq) -> bool {\n true", "expect": "killed", "reason": "RFC 8446 §4.4.2 requires the server Certificate context to be empty during initial server authentication; nonempty client contexts remain supported by the generic parser.", - "module": "auth::mutation_certificates", + "module": "auth::certificates", "certificate": { "file": "src/auth/mutation_certificates.rs", "lemma": "super::certificates::lemma_nonempty_server_certificate_context_is_rejected()", @@ -2429,7 +2415,7 @@ "replace": "else if false {", "expect": "killed", "reason": "RFC 5246 §7.4.1.3 allows the legacy ServerHello extension field to be absent; a complete pre-TLS-1.3 response maps to protocol_version, while the strict generic TLS 1.3 parser would report decode_error.", - "module": "hello::mutation_certificates", + "module": "hello::certificates", "certificate": { "file": "src/hello/mutation_certificates.rs", "lemma": "super::certificates::lemma_absent_legacy_extension_field_uses_protocol_version()", @@ -2443,7 +2429,7 @@ "replace": "None => Some(crate::spec::MISSING_EXTENSION),", "expect": "killed", "reason": "A legacy ServerHello without supported_versions selects an unsupported protocol for this TLS 1.3-only client and must fail with protocol_version.", - "module": "hello::mutation_certificates", + "module": "hello::certificates", "certificate": { "file": "src/hello/mutation_certificates.rs", "lemma": "super::certificates::lemma_legacy_server_hello_uses_protocol_version()", diff --git a/crates/clazel-tls/src/examples_hs.rs b/crates/clazel-tls/src/examples_hs.rs index ba3cebd4..b46ca2b1 100644 --- a/crates/clazel-tls/src/examples_hs.rs +++ b/crates/clazel-tls/src/examples_hs.rs @@ -345,6 +345,8 @@ pub proof fn lemma_server_hello() parse_handshake_body(2, sh_body(z32(), 0, seq![0u8, 7, 0, 0x2b, 0, 3, 3, 4, 5]), 32) == Res::::Err(ErrKind::Decode), // RFC 5246's legacy extension syntax permits a five-byte extension vector. parse_handshake_body(2, sh_body(z32(), 0, seq![0u8, 5, 0x12, 0x34, 0, 1, 9]), 32) is Ok, + // An empty extension vector is syntactically allowed; negotiation reports protocol_version. + parse_handshake_body(2, sh_body(z32(), 0, seq![0u8, 0]), 32) is Ok, { assert(parse_handshake_body(2, sh_body(z32(), 0, seq![0u8, 6] + sv_ext()), 32) == Res::::Ok( HsMsg::ServerHello( @@ -405,6 +407,7 @@ pub proof fn lemma_server_hello() assert(parse_handshake_body(2, sh_body(z32(), 0, seq![0u8, 7, 0, 0x2b, 0, 3, 3, 4, 5]), 32) == Res::::Err(ErrKind::Decode)) by (compute_only); assert(parse_handshake_body(2, sh_body(z32(), 0, seq![0u8, 5, 0x12, 0x34, 0, 1, 9]), 32) is Ok) + by (compute_only); assert(parse_handshake_body(2, sh_body(z32(), 0, seq![0u8, 0]), 32) is Ok) by (compute_only); } diff --git a/crates/clazel-tls/src/hello/certificates.rs b/crates/clazel-tls/src/hello/certificates.rs index ae5a2bb3..402dff35 100644 --- a/crates/clazel-tls/src/hello/certificates.rs +++ b/crates/clazel-tls/src/hello/certificates.rs @@ -50,6 +50,39 @@ pub proof fn lemma_legacy_server_hello_uses_protocol_version() ) == Some(crate::spec::PROTOCOL_VERSION)) by (compute_only); } +/// A complete base ServerHello whose extension vector is `exts` (the bytes +/// after the two-byte vector length, which this prefixes). +pub open spec fn legacy_server_hello_with_extensions(exts: Seq) -> Seq { + legacy_server_hello_without_extension_field() + seq![0u8, exts.len() as u8] + exts +} + +/// A nonempty extension list without `supported_versions` identifies no +/// TLS 1.3 version: `protocol_version`, even though the generic parser would +/// reject the (server_name) extension as not allowed in a ServerHello. +pub proof fn lemma_legacy_server_hello_extensions_without_supported_versions() + ensures + super::spec::validate( + Seq::empty(), false, legacy_server_hello_with_extensions(seq![0u8, 0, 0, 0]), + ) == Err(crate::spec::PROTOCOL_VERSION), +{ + assert(super::spec::validate( + Seq::empty(), false, legacy_server_hello_with_extensions(seq![0u8, 0, 0, 0]), + ) == Err(crate::spec::PROTOCOL_VERSION)) by (compute_only); +} + +/// `supported_versions` in a non-first position is found: the message is not +/// a legacy ServerHello without it. +pub proof fn lemma_supported_versions_found_after_other_extension() + ensures + !crate::spec::legacy_server_hello_without_supported_versions( + legacy_server_hello_with_extensions(seq![0x12u8, 0x34, 0, 1, 9, 0, 0x2b, 0, 2, 3, 4]), + ), +{ + assert(!crate::spec::legacy_server_hello_without_supported_versions( + legacy_server_hello_with_extensions(seq![0x12u8, 0x34, 0, 1, 9, 0, 0x2b, 0, 2, 3, 4]), + )) by (compute_only); +} + /// A hash that is irrelevant to a CCS event. pub open spec fn empty_hash(_messages: Seq) -> Seq { seq![] }