tls: refuse a compatibility CCS inside a fragmented handshake message

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": "dispatcher-ccs-dropped-mid-message",
+      "file": "src/connection/dispatcher_spec.rs",
+      "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.",
+      "module": "connection::dispatcher_lemmas",
+      "certificate": {
+        "file": "src/connection/dispatcher_certificates.rs",
+        "lemma": "super::dispatcher_lemmas::lemma_compatibility_ccs_not_dropped_mid_message()",
+        "witness": "super::dispatcher_spec::compatibility_ccs_dropped(super::dispatcher_spec::Mode::Handshake, Some(crate::auth::spec::Phase::Finished), crate::spec::Reasm { buf: seq![1u8] })"
+      }
+    },
     {
       "id": "dispatcher-peer-update-epoch-construction-failure",
       "file": "src/connection/dispatcher_spec.rs",

crates/clazel-tls/src/connection/dispatcher_contract.rs

@@ -49,6 +49,16 @@ pub open spec fn feed_ensures(before: super::dispatcher_spec::State, input: Seq<
         && super::dispatcher_spec::action_refines(action, after)
 }
 
+/// RFC 8446 §5.1: a valid unprotected compatibility CCS record, in a state
+/// that still holds authentication, is dropped only at a handshake message
+/// boundary; in the middle of a fragmented handshake message it is fatal.
+pub open spec fn ccs_record_ensures(wire: Seq<u8>, before: super::dispatcher_spec::State,
+    action: super::dispatcher_spec::Action, after: super::dispatcher_spec::State) -> bool {
+    (before.auth is Some && crate::spec::read_record(wire, true) is Done
+        && crate::spec::read_record(wire, true)->Done_0 is Ccs)
+        ==> (action, after) == super::dispatcher_spec::receive_compatibility_ccs(before)
+}
+
 /// A peer close_notify closes only the peer's write direction and preserves
 /// the local send epoch until our own write side is closed.
 pub open spec fn peer_close_ensures(before: super::dispatcher_spec::State,

crates/clazel-tls/src/connection/dispatcher_lemmas.rs

@@ -78,4 +78,17 @@ pub proof fn lemma_peer_close_is_directional()
             ..super::dispatcher_certificates::sample_ready_state()
         });
 }
+
+/// RFC 8446 §5.1: a compatibility CCS between the fragments of one handshake
+/// message interleaves another record type and is refused; at a boundary the
+/// same record is still dropped.
+pub proof fn lemma_compatibility_ccs_not_dropped_mid_message()
+    ensures
+        !super::dispatcher_spec::compatibility_ccs_dropped(super::dispatcher_spec::Mode::Handshake,
+            Some(crate::auth::spec::Phase::Finished), crate::spec::Reasm { buf: seq![1u8] }),
+        super::dispatcher_spec::compatibility_ccs_dropped(super::dispatcher_spec::Mode::Handshake,
+            Some(crate::auth::spec::Phase::Finished), crate::spec::reasm_new()),
+{
+    reveal(crate::spec::reasm_new);
+}
 } // verus!

crates/clazel-tls/src/connection/dispatcher_spec.rs

@@ -12,6 +12,10 @@
 //! - The compatibility CCS is a one-byte dummy record, tracked separately
 //!   from the protected record epochs. For an HRR retry it was already sent
 //!   before ClientHello2 by the Hello driver.
+//! - RFC 8446 §5.1 forbids interleaving a handshake message with another
+//!   record type, and a compatibility CCS is another record type. It is
+//!   dropped only while no handshake message is partly received
+//!   (`message_boundary`); in the middle of one it is fatal unexpected_message.
 //! - Terminal states retain no authentication secrets, traffic epochs, or
 //!   partial input. NewSessionTicket bodies are parsed and discarded; ticket
 //!   caching, PSK resumption, 0-RTT, and secret-erasure guarantees are not
@@ -127,6 +131,31 @@ pub open spec fn message_boundary(s: State) -> bool {
 /// Appendix D.4 dummy CCS record, sent only when the retained Hello profile owes it.
 pub open spec fn compatibility_ccs_record() -> Seq<u8> { seq![20u8, 3u8, 3u8, 0u8, 1u8, 1u8] }
 
+/// RFC 8446 §5.1 "Handshake messages MUST NOT be interleaved with other
+/// record types" and Appendix D.4: an unprotected compatibility CCS is dropped
+/// only in the server-flight phases of the handshake, and only when no
+/// handshake message is partly received.
+pub open spec fn compatibility_ccs_dropped(mode: Mode, phase: Option<crate::auth::spec::Phase>,
+    reassembly: crate::spec::Reasm) -> bool {
+    mode == Mode::Handshake
+        && match phase {
+            Some(p) => p != crate::auth::spec::Phase::SendFinished && p != crate::auth::spec::Phase::Ready,
+            None => false,
+        }
+        && crate::spec::at_message_boundary(reassembly)
+}
+
+/// The effect of one valid unprotected compatibility CCS record: dropped with
+/// no state change when permitted, else a fatal unexpected_message.
+pub open spec fn receive_compatibility_ccs(s: State) -> (Action, State) {
+    let phase = match s.auth { Some(a) => Some(a.phase), None => None };
+    if compatibility_ccs_dropped(s.mode, phase, s.reassembly) {
+        (Action::Ignored, s)
+    } else {
+        (Action::Fail(crate::spec::UNEXPECTED_MESSAGE), failed())
+    }
+}
+
 /// A handshake record flight has Finished as its last complete message.
 pub open spec fn finished_is_last(messages: Seq<Seq<u8>>) -> bool {
     messages.len() > 0 && messages.last().len() >= crate::spec::HANDSHAKE_HEADER

crates/clazel-tls/src/connection/exec.rs

@@ -671,15 +671,20 @@ impl<C: Crypto, F: Factory, V: Verifier> Connection<C, F, V> where F::Cipher: Ke
         requires old(self).wf(), old(self).auth_wf(), old(self).resources_wf(), old(self).cipher_bindings_wf(),
         ensures final(self).wf(), final(self).auth_wf(), final(self).resources_wf(), final(self).cipher_bindings_wf(),
             super::dispatcher_spec::action_refines(out@, final(self)@),
+            super::dispatcher_contract::ccs_record_ensures(wire@, old(self)@, out@, final(self)@),
     {
         match crate::record::read_record(wire, true) {
             ReadOut::Done(Frame::Ccs, _) => {
                 let auth = match self.auth.as_ref() {
                     Some(auth) => auth,
                     None => return self.fail(crate::spec::INTERNAL_ERROR),
                 };
+                // RFC 8446 §5.1: handshake messages "MUST NOT be interleaved with
+                // other record types", so a compatibility CCS is dropped only at a
+                // message boundary; inside a fragmented message it is fatal.
                 if matches!(self.mode, Mode::Handshake)
-                    && !matches!(auth.phase(), crate::auth::spec::Phase::SendFinished | crate::auth::spec::Phase::Ready) {
+                    && !matches!(auth.phase(), crate::auth::spec::Phase::SendFinished | crate::auth::spec::Phase::Ready)
+                    && self.reassembler.at_message_boundary() {
                     Action::Ignored
                 } else {
                     self.fail(crate::spec::UNEXPECTED_MESSAGE)

crates/clazel-tls/src/connection/framing.rs

@@ -79,7 +79,7 @@ impl Buffer {
     }
 
     /// Whether this mode's byte prefix is empty.
-    pub fn is_empty_mode(&self, protected: bool) -> (out: bool)
+    pub fn is_empty_mode(&self, Ghost(protected): Ghost<bool>) -> (out: bool)
         requires self.protected_mode() == protected, self.wf_mode(protected),
         ensures super::framing_contract::is_empty_mode_ensures(protected, self@, out),
     {

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

@@ -204,7 +204,7 @@ impl<C: Crypto> Bootstrap<C> {
         if messages.is_empty() {
             return Action::None;
         }
-        if messages.len() != 1 || !self.reassembler.at_message_boundary() || !self.framer.is_empty_mode(false) {
+        if messages.len() != 1 || !self.reassembler.at_message_boundary() || !self.framer.is_empty_mode(Ghost(false)) {
             return self.fail(crate::spec::UNEXPECTED_MESSAGE);
         }
         let message = match messages.first() {
@@ -337,10 +337,7 @@ impl<C: Crypto> Bootstrap<C> {
         let compatibility = !config.session_id.is_empty();
         let started = Hello::start(config);
         let ghost started_view = super::client::start_view(started);
-        let (hello, flight) = match started {
-            Ok(pair) => pair,
-            Err(alert) => return Err(alert),
-        };
+        let (hello, flight) = started?;
         proof {
             assert(started_view == Ok((hello@, flight@)));
             assert(super::client_spec::config_ok(config_view));

crates/clazel-tls/tests/connection_dispatch.rs

@@ -885,20 +885,12 @@ fn valid_new_session_tickets_are_discarded_without_resumption_state() -> Result<
     Ok(())
 }
 
+/// RFC 8446 §5.1: a compatibility CCS between the fragments of one handshake
+/// message interleaves another record type and is fatal unexpected_message.
 #[test]
-fn compatibility_ccs_is_dropped_between_handshake_fragments() -> Result<(), String> {
+fn compatibility_ccs_between_handshake_fragments_is_refused() -> Result<(), String> {
     let mut fixture = fixture()?;
     let encrypted_extensions = handshake(8, &encrypted_extensions());
-    let certificate = handshake(11, &certificate_body());
-    let certificate_verify = handshake(15, &certificate_verify());
-    let (_, client_hello) = Hello::start(config()).map_err(|e| format!("Hello alert {e}"))?;
-    let mut server_transcript = client_hello;
-    server_transcript.extend_from_slice(&handshake(2, &server_hello()));
-    server_transcript.extend_from_slice(&encrypted_extensions);
-    server_transcript.extend_from_slice(&certificate);
-    server_transcript.extend_from_slice(&certificate_verify);
-    let finished_body = finished(&fixture.crypto, &fixture.server_secret, &server_transcript);
-    let finished = handshake(20, &finished_body);
     let split = encrypted_extensions.len().saturating_div(2);
     let prefix = encrypted_extensions.get(..split).ok_or("short EE prefix")?;
     let suffix = encrypted_extensions
@@ -915,29 +907,39 @@ fn compatibility_ccs_is_dropped_between_handshake_fragments() -> Result<(), Stri
         (prefix_record.len(), Action::None)
     );
     let ccs = [20, 3, 3, 0, 1, 1];
-    assert_eq!(fixture.connection.feed(&ccs), (ccs.len(), Action::Ignored));
-
+    assert_eq!(fixture.connection.feed(&ccs), (ccs.len(), Action::Fail(10)));
+    // The failure is terminal: the rest of the message is not accepted.
     let suffix_record = server
         .seal(22, suffix, 0)
         .map_err(|e| format!("suffix seal alert {e}"))?;
+    assert_eq!(fixture.connection.feed(&suffix_record).1, Action::None);
+    Ok(())
+}
+
+/// A compatibility CCS between two whole handshake messages is still dropped.
+#[test]
+fn compatibility_ccs_between_whole_handshake_messages_is_dropped() -> Result<(), String> {
+    let mut fixture = fixture()?;
+    let encrypted_extensions = handshake(8, &encrypted_extensions());
+    let certificate = handshake(11, &certificate_body());
+    let mut server = Encryptor::new(&fixture.crypto, &fixture.factory, &fixture.server_secret)
+        .map_err(|e| format!("server epoch alert {e}"))?;
+    let ee_record = server
+        .seal(22, &encrypted_extensions, 0)
+        .map_err(|e| format!("EE seal alert {e}"))?;
     assert_eq!(
-        fixture.connection.feed(&suffix_record),
-        (suffix_record.len(), Action::None)
+        fixture.connection.feed(&ee_record),
+        (ee_record.len(), Action::None)
+    );
+    let ccs = [20, 3, 3, 0, 1, 1];
+    assert_eq!(fixture.connection.feed(&ccs), (ccs.len(), Action::Ignored));
+    let certificate_record = server
+        .seal(22, &certificate, 0)
+        .map_err(|e| format!("certificate seal alert {e}"))?;
+    assert_eq!(
+        fixture.connection.feed(&certificate_record),
+        (certificate_record.len(), Action::None)
     );
-    let mut last_action = Action::None;
-    for message in [certificate, certificate_verify, finished] {
-        let record = server
-            .seal(22, &message, 0)
-            .map_err(|e| format!("server flight seal alert {e}"))?;
-        let (consumed, action) = fixture.connection.feed(&record);
-        assert_eq!(consumed, record.len());
-        last_action = action;
-    }
-    if !matches!(last_action, Action::Send(_)) {
-        return Err(format!(
-            "expected client flight after in-fragment CCS, got {last_action:?}"
-        ));
-    }
     Ok(())
 }
 

crates/clazel-tls/tests/hello_bootstrap.rs

@@ -15,9 +15,8 @@ const RANDOM: [u8; 32] = [0x35; 32];
 const CLIENT_KEY: [u8; 32] = [0x48; 32];
 const SERVER_KEY: [u8; 32] = [0x5a; 32];
 const HRR_RANDOM: [u8; 32] = [
-    0xcf, 0x21, 0xad, 0x74, 0xe5, 0x9a, 0x61, 0x11, 0xbe, 0x1d, 0x8c, 0x02, 0x1e, 0x65, 0xb8,
-    0x91, 0xc2, 0xa2, 0x11, 0x16, 0x7a, 0xbb, 0x8c, 0x5e, 0x07, 0x9e, 0x09, 0xe2, 0xc8, 0xa8,
-    0x33, 0x9c,
+    0xcf, 0x21, 0xad, 0x74, 0xe5, 0x9a, 0x61, 0x11, 0xbe, 0x1d, 0x8c, 0x02, 0x1e, 0x65, 0xb8, 0x91,
+    0xc2, 0xa2, 0x11, 0x16, 0x7a, 0xbb, 0x8c, 0x5e, 0x07, 0x9e, 0x09, 0xe2, 0xc8, 0xa8, 0x33, 0x9c,
 ];
 
 /// Deterministic transcript provider only; not an interoperable crypto suite.
@@ -131,7 +130,10 @@ fn exact_send_ack_gates_peer_input_and_wrong_ack_is_terminal() -> Result<(), Str
     assert_eq!(client_wire.first(), Some(&22));
 
     let wrong = [client_wire.as_slice(), &[0]].concat();
-    assert!(matches!(bootstrap.acknowledge_send(&wrong), Action::Fail(INTERNAL_ERROR)));
+    assert!(matches!(
+        bootstrap.acknowledge_send(&wrong),
+        Action::Fail(INTERNAL_ERROR)
+    ));
     let peer = plaintext(22, &handshake(2, &server_hello(SESSION, false)));
     assert_eq!(bootstrap.feed(&peer).0, 0);
     assert!(matches!(bootstrap.eof(), Action::None));
@@ -145,7 +147,7 @@ fn ccs_is_dropped_during_fragmented_server_hello_without_losing_prefix() -> Resu
 
     let hello = handshake(2, &server_hello(SESSION, false));
     let split = hello.len() / 2;
-    let first_record = plaintext(22, &hello[..split]);
+    let first_record = plaintext(22, hello.get(..split).ok_or("missing first fragment")?);
     let (consumed, first_action) = bootstrap.feed(&first_record);
     assert_eq!(consumed, first_record.len());
     assert!(matches!(first_action, Action::None));
@@ -157,7 +159,7 @@ fn ccs_is_dropped_during_fragmented_server_hello_without_losing_prefix() -> Resu
     assert_eq!(consumed, dummy_ccs.len());
     assert!(matches!(ccs_action, Action::None));
 
-    let last_record = plaintext(22, &hello[split..]);
+    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 {
@@ -167,7 +169,10 @@ fn ccs_is_dropped_during_fragmented_server_hello_without_losing_prefix() -> Resu
     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);
+    assert_eq!(
+        transcript.phase(),
+        clazel_tls::transcript::spec::Phase::Handshake
+    );
     Ok(())
 }
 
@@ -188,15 +193,19 @@ fn retry_flight_orders_compatibility_ccs_and_requires_exact_ack() -> Result<(),
 
     let server = plaintext(22, &handshake(2, &server_hello(SESSION, false)));
     assert_eq!(bootstrap.feed(&server).0, 0);
-    assert!(matches!(bootstrap.acknowledge_send(&retry_wire), Action::None));
+    assert!(matches!(
+        bootstrap.acknowledge_send(&retry_wire),
+        Action::None
+    ));
     let (consumed, action) = bootstrap.feed(&server);
     assert_eq!(consumed, server.len());
     assert!(matches!(action, Action::Established(_)));
     Ok(())
 }
 
 #[test]
-fn no_compatibility_ccs_for_empty_session_id_and_coalesced_suffix_stays_unconsumed() -> Result<(), String> {
+fn no_compatibility_ccs_for_empty_session_id_and_coalesced_suffix_stays_unconsumed()
+-> Result<(), String> {
     let (mut bootstrap, client_wire) = started(&[])?;
     ack_initial(&mut bootstrap, &client_wire)?;
     let retry = plaintext(22, &handshake(2, &server_hello(&[], true)));
@@ -206,14 +215,22 @@ fn no_compatibility_ccs_for_empty_session_id_and_coalesced_suffix_stays_unconsum
         _ => return Err("valid HRR did not produce a retry flight".to_owned()),
     };
     assert_eq!(retry_wire.first(), Some(&22));
-    assert!(matches!(bootstrap.acknowledge_send(&retry_wire), Action::None));
+    assert!(matches!(
+        bootstrap.acknowledge_send(&retry_wire),
+        Action::None
+    ));
 
     let final_record = plaintext(22, &handshake(2, &server_hello(&[], false)));
     let suffix = [final_record.as_slice(), &[20, 3, 3, 0, 1, 1]].concat();
     let (consumed, action) = bootstrap.feed(&suffix);
     assert_eq!(consumed, final_record.len());
     assert!(matches!(action, Action::Established(_)));
-    assert_eq!(bootstrap.feed(&suffix[consumed..]).0, 0);
+    assert_eq!(
+        bootstrap
+            .feed(suffix.get(consumed..).ok_or("bad consumed boundary")?)
+            .0,
+        0
+    );
     Ok(())
 }