tls: bootstrap refuses a CCS inside a fragmented ServerHello

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::<HsMsg>::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::<HsMsg>::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::<HsMsg>::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);
 }
 

crates/clazel-tls/src/hello/bootstrap.rs

@@ -442,8 +442,12 @@ impl<C: Crypto> Bootstrap<C> {
     {
         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); }

crates/clazel-tls/src/hello/bootstrap_lemmas.rs

@@ -144,7 +144,13 @@ pub open spec fn record_step(hash: spec_fn(Seq<u8>) -> Seq<u8>, 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 =>

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<u8>) -> Seq<u8>, 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,

crates/clazel-tls/src/hello/certificates.rs

@@ -50,4 +50,59 @@ 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<u8>) -> Seq<u8> {
+    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<u8>) -> Seq<u8> { seq![] }
+
+/// A bootstrap state awaiting ServerHello with `buf` already reassembled.
+pub open spec fn awaiting_with_buffer(buf: Seq<u8>) -> 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<u8>| 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<u8>| empty_hash(m), awaiting_with_buffer(seq![]),
+            super::bootstrap_spec::PeerEvent::Ccs)
+            == (awaiting_with_buffer(seq![]), super::bootstrap_spec::Action::None),
+{
+}
 }

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(())
 }
 

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", <https://www.rfc-editor.org/rfc/rfc8446#section-5>
+- **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.