diff --git a/crates/clazel-tls/mutations.json b/crates/clazel-tls/mutations.json index e82ad269..5c8313d4 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": "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", diff --git a/crates/clazel-tls/src/connection/dispatcher_contract.rs b/crates/clazel-tls/src/connection/dispatcher_contract.rs index 0e8d44f2..32689494 100644 --- a/crates/clazel-tls/src/connection/dispatcher_contract.rs +++ b/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, 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, diff --git a/crates/clazel-tls/src/connection/dispatcher_lemmas.rs b/crates/clazel-tls/src/connection/dispatcher_lemmas.rs index 8f07268c..540e1017 100644 --- a/crates/clazel-tls/src/connection/dispatcher_lemmas.rs +++ b/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! diff --git a/crates/clazel-tls/src/connection/dispatcher_spec.rs b/crates/clazel-tls/src/connection/dispatcher_spec.rs index d2d0574f..03e8cd29 100644 --- a/crates/clazel-tls/src/connection/dispatcher_spec.rs +++ b/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 { 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, + 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>) -> bool { messages.len() > 0 && messages.last().len() >= crate::spec::HANDSHAKE_HEADER diff --git a/crates/clazel-tls/src/connection/exec.rs b/crates/clazel-tls/src/connection/exec.rs index 9c5676f4..662c8983 100644 --- a/crates/clazel-tls/src/connection/exec.rs +++ b/crates/clazel-tls/src/connection/exec.rs @@ -671,6 +671,7 @@ impl Connection 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, _) => { @@ -678,8 +679,12 @@ impl Connection where F::Cipher: Ke 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) diff --git a/crates/clazel-tls/src/connection/framing.rs b/crates/clazel-tls/src/connection/framing.rs index 170e0840..efd3cf3a 100644 --- a/crates/clazel-tls/src/connection/framing.rs +++ b/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) -> (out: bool) requires self.protected_mode() == protected, self.wf_mode(protected), ensures super::framing_contract::is_empty_mode_ensures(protected, self@, out), { diff --git a/crates/clazel-tls/src/hello/bootstrap.rs b/crates/clazel-tls/src/hello/bootstrap.rs index 0b5ebf02..f492c2ce 100644 --- a/crates/clazel-tls/src/hello/bootstrap.rs +++ b/crates/clazel-tls/src/hello/bootstrap.rs @@ -204,7 +204,7 @@ impl Bootstrap { 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 Bootstrap { 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)); diff --git a/crates/clazel-tls/tests/connection_dispatch.rs b/crates/clazel-tls/tests/connection_dispatch.rs index 1c60baa5..d9db8920 100644 --- a/crates/clazel-tls/tests/connection_dispatch.rs +++ b/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(()) } diff --git a/crates/clazel-tls/tests/hello_bootstrap.rs b/crates/clazel-tls/tests/hello_bootstrap.rs index 156e59a1..f3634dde 100644 --- a/crates/clazel-tls/tests/hello_bootstrap.rs +++ b/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,7 +193,10 @@ 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(_))); @@ -196,7 +204,8 @@ fn retry_flight_orders_compatibility_ccs_and_requires_exact_ack() -> Result<(), } #[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(()) }