diff --git a/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-04::src::application_message_generation_skip_dos.json b/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-04::src::application_message_generation_skip_dos.json new file mode 100644 index 0000000000..47d3ed6b5d --- /dev/null +++ b/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-04::src::application_message_generation_skip_dos.json @@ -0,0 +1,28 @@ +{ + "built_by": "t27c-bootstrap@0.5.2+01d0a635f", + "closure": [], + "config": "gen=c,rust,verilog,zig;tests=zig", + "gen_hash_c": "sha256:a5685b2503fa6471b679a8a6612050aa1f2b2bf8156d2ec44213ea85d613ef99", + "gen_hash_rust": "sha256:abd1593938d72bbfc9d572f8adfd08bdd090e21a3d3f7385ec3d6d2acdb8cf31", + "gen_hash_verilog": "sha256:a969cc380ea1f50c30ed1a35e36c60e75d11b127c90ea9bc8087fa247e7e5685", + "gen_hash_zig": "sha256:d811fdb0334f599db5adfe3fb5ac646f01c39e487a2d71c97f7d24acd6b4f248", + "module": "port::trios::crates::trios-chat::rings::CR-CHAT-04::src::application_message_generation_skip_dos", + "ring": 12, + "seal_schema": 2, + "sealed_at": "2026-10-15T21:25:10Z", + "sealed_by": "t27c-bootstrap@0.5.2", + "spec_hash": "sha256:c6c5d8d439602f073ae1fa1100496f631ab6107fe6a6dd9a4af2ba4d1c95d282", + "spec_path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/application_message_generation_skip_dos.t27", + "tests": { + "failed": 0, + "failing": [], + "forced": false, + "passed": 14, + "total": 14, + "vacuous": 0 + }, + "toolchain": { + "test_runner": "sha256:1982ae948e24d00c5d221ccec12dfce1eb01204b53e37b0f857f93b16d64629d", + "zig": "0.16.0" + } +} \ No newline at end of file diff --git a/docs/reports/t27b_expectations.json b/docs/reports/t27b_expectations.json index 3483595ccc..09f98ab20a 100644 --- a/docs/reports/t27b_expectations.json +++ b/docs/reports/t27b_expectations.json @@ -857,6 +857,7 @@ {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-03/src/ratchet_tree_resolution_guard.t27", "t27b": "pass"}, {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-03/src/ratchet_tree_update_integrity_guard.t27", "t27b": "pass"}, {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-03/src/unmerged_leaves_bound_guard.t27", "t27b": "pass"}, + {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/application_message_generation_skip_dos.t27", "t27b": "pass"}, {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_alignment_boundary_guard.t27", "t27b": "pass"}, {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_block_size_alignment_guard.t27", "t27b": "pass"}, {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-05/src/envelope_size_distribution_uniformity.t27", "t27b": "pass"}, diff --git a/specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/application_message_generation_skip_dos.t27 b/specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/application_message_generation_skip_dos.t27 new file mode 100644 index 0000000000..2b7ea52a8f --- /dev/null +++ b/specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/application_message_generation_skip_dos.t27 @@ -0,0 +1,318 @@ +module port::trios::crates::trios-chat::rings::CR-CHAT-04::src::application_message_generation_skip_dos; + +// Port of gHashTag/trios crates/trios-chat/rings/CR-CHAT-04/src/application_message_generation_skip_dos.rs +// (CR-CHAT-04 - Application-message generation skip-window DoS defence, +// Wave-36 Lane L-CHAT-4-amgsd, requirement R-CHAT-4, RFC 9420 sections +// 9.3 and 15.2). +// +// Within one (sender, epoch) the MLS generation counter is strictly +// monotone, but receivers tolerate a bounded amount of out-of-order +// delivery by key-deriving skipped generations on demand. Without a cap +// one attacker packet claiming generation u64::MAX forces a +// tens-of-billions-of-rounds HKDF chain, so the skip distance the +// receiver will derive is capped at APP_MSG_SKIP_WINDOW. +// +// The original returns Result<(), AppMessageSkipError>. This port +// carries the verdict as a named struct (owner decision D5): Ok first, +// then the seven error variants in the original's declaration order - +// NonCanonicalSenderIdLength, UnknownSender, ZeroGeneration, +// NonMonotonicGeneration, SkipDistanceExceeded, EpochMismatch, +// CiphertextEmpty. No variant carries a payload, so the verdict is the +// code alone. +// +// The original's Vec sender ids are read by length and equality; +// its known_senders and last_generation tables by membership and +// lookup. The port uses fixed-size ids ([16]u8) with helpers (equality, +// membership, table lookup), each with its own test. The ciphertext is +// read only by emptiness, so the record carries the length. The +// (Vec, u64, u64) last_generation rows become a record of the id +// and the two numbers. + +// Canonical sender_id length (16 bytes - MLS LeafNodeRef, RFC 9420 6.1). +pub const APP_MSG_SENDER_ID_LEN: usize = 16; + +// Maximum number of skipped generations the receiver will key-derive +// ahead of last_generation. +pub const APP_MSG_SKIP_WINDOW: u64 = 1024; + +// A row of the receiver's last_generation table: a sender, its epoch +// and the last generation seen for that pair. +pub struct GenRow { + sender: [16]u8, + epoch: u64, + last: u64, +} + +// A known sender's id, wrapped in a record so the known-sender table +// is a one-dimensional array of records (a two-dimensional fixed array +// is not lowered by the Rust backend - conventions section 4). +pub struct SenderId { + id: [16]u8, +} + +// A single MLS application-message header arriving at the receiver. +pub struct AppMessagePacket { + sender_id: [16]u8, + sender_id_len: usize, + epoch: u64, + generation: u64, + ciphertext_len: usize, +} + +// Receiver-side view of application-key state. +pub struct AppMessageView { + current_epoch: u64, + known_senders: [2]SenderId, + last_generation: [2]GenRow, +} + +// Verdict codes: Ok(()) and AppMessageSkipError's variants, in declaration order. +pub enum AppMessageSkipCode { + Ok, + NonCanonicalSenderIdLength, + UnknownSender, + ZeroGeneration, + NonMonotonicGeneration, + SkipDistanceExceeded, + EpochMismatch, + CiphertextEmpty, +} + +// The verdict of the skip-window validation. No variant of the +// original's error carries a payload, so the code is the whole verdict. +pub struct AppMessageSkipVerdict { + code: AppMessageSkipCode, +} + +// Whole-id equality over the fixed-size ids. +pub fn ids_equal(a: [16]u8, b: [16]u8) -> bool { + for i in 0..16 { + if (a[i] != b[i]) { + return false; + } + } + return true; +} + +// Membership of a sender in the fixed-size known-sender table. The +// original asks known_senders.contains(&sender); there is no Vec here, +// so the scan covers exactly the slots the caller filled. The sentinel +// row holds id 255 in every byte, which no fixture id equals. +pub fn sender_known(id: [16]u8, known: [2]SenderId) -> bool { + for i in 0..2 { + if (ids_equal(id, known[i].id)) { + return true; + } + } + return false; +} + +// The last generation seen for one (sender, epoch), 0 when the table has +// no row for the pair - the original's unwrap_or(0). +pub fn last_seen_for(id: [16]u8, epoch: u64, table: [2]GenRow) -> u64 { + for i in 0..2 { + if (ids_equal(id, table[i].sender)) { + if (table[i].epoch == epoch) { + return table[i].last; + } + } + } + return 0; +} + +// [VERIFIED] Validate a single application packet's (sender, epoch, +// generation) triple plus body shape against the receiver's view. +// Returns Ok only when every rule holds, checked in the original's +// order: canonical sender-id length, known sender, active epoch, +// non-empty ciphertext, non-zero generation, strictly monotone +// generation, and a skip distance within the window. +pub fn validate_app_message_skip(packet: AppMessagePacket, view: AppMessageView) -> AppMessageSkipVerdict { + if (packet.sender_id_len != APP_MSG_SENDER_ID_LEN) { + return AppMessageSkipVerdict { code: AppMessageSkipCode.NonCanonicalSenderIdLength, }; + } + if (!sender_known(packet.sender_id, view.known_senders)) { + return AppMessageSkipVerdict { code: AppMessageSkipCode.UnknownSender, }; + } + if (packet.epoch != view.current_epoch) { + return AppMessageSkipVerdict { code: AppMessageSkipCode.EpochMismatch, }; + } + if (packet.ciphertext_len == 0) { + return AppMessageSkipVerdict { code: AppMessageSkipCode.CiphertextEmpty, }; + } + if (packet.generation == 0) { + return AppMessageSkipVerdict { code: AppMessageSkipCode.ZeroGeneration, }; + } + const last_seen: u64 = last_seen_for(packet.sender_id, packet.epoch, view.last_generation); + if (packet.generation <= last_seen) { + return AppMessageSkipVerdict { code: AppMessageSkipCode.NonMonotonicGeneration, }; + } + const skip_distance: u64 = packet.generation - last_seen - 1; + if (skip_distance > APP_MSG_SKIP_WINDOW) { + return AppMessageSkipVerdict { code: AppMessageSkipCode.SkipDistanceExceeded, }; + } + return AppMessageSkipVerdict { code: AppMessageSkipCode.Ok, }; +} + +// The fixtures' sender ids, one byte repeated 16 times. +pub const SENDER_A: [16]u8 = [16]u8{0xA1, 0xA1, 0xA1, 0xA1, 0xA1, 0xA1, 0xA1, 0xA1, 0xA1, 0xA1, 0xA1, 0xA1, 0xA1, 0xA1, 0xA1, 0xA1,}; +pub const SENDER_B: [16]u8 = [16]u8{0xB2, 0xB2, 0xB2, 0xB2, 0xB2, 0xB2, 0xB2, 0xB2, 0xB2, 0xB2, 0xB2, 0xB2, 0xB2, 0xB2, 0xB2, 0xB2,}; + +// The sentinel row of the tables: id 255 in every byte, epoch and last +// at values no fixture pair equals. +pub const EMPTY_ROW: GenRow = GenRow { sender: [16]u8{255, 255, 255, 255, 255, 255, 255, 255, 255, 255, 255, 255, 255, 255, 255, 255,}, epoch: 18446744073709551615, last: 0, }; + +// The canonical view fixture of the tests: one known sender, one +// last_generation row (sender A, epoch 7, generation 10). +fn ok_view() -> AppMessageView { + return AppMessageView { + current_epoch: 7, + known_senders: [2]SenderId{ SenderId { id: SENDER_A, }, SenderId { id: SENDER_B, }, }, + last_generation: [2]GenRow{ GenRow { sender: SENDER_A, epoch: 7, last: 10, }, EMPTY_ROW, }, + }; +} + +// The canonical packet fixture of the tests: sender A, epoch 7, +// generation 11 (last seen 10, skip distance 0), 64 bytes of ciphertext. +fn ok_packet() -> AppMessagePacket { + return AppMessagePacket { + sender_id: SENDER_A, + sender_id_len: APP_MSG_SENDER_ID_LEN, + epoch: 7, + generation: 11, + ciphertext_len: 64, + }; +} + +// **AMGSD-01** - short sender id rejected: 8 of a canonical 16. +test amgsd_01_short_sender_id_rejected { + var p = ok_packet(); + p.sender_id_len = 8; + var view = ok_view(); + const v = validate_app_message_skip(p, view); + assert(v.code == AppMessageSkipCode.NonCanonicalSenderIdLength); +} + +// **AMGSD-02** - unknown sender rejected: sender B is not in the view's +// known table. +test amgsd_02_unknown_sender_rejected { + var p = ok_packet(); + p.sender_id = SENDER_B; + var view = ok_view(); + view.known_senders = [2]SenderId{ SenderId { id: SENDER_A, }, SenderId { id: EMPTY_ROW.sender, }, }; + const v = validate_app_message_skip(p, view); + assert(v.code == AppMessageSkipCode.UnknownSender); +} + +// **AMGSD-03** - wrong epoch rejected: packet claims epoch 6 against a +// current 7. +test amgsd_03_epoch_mismatch_rejected { + var p = ok_packet(); + p.epoch = 6; + var view = ok_view(); + const v = validate_app_message_skip(p, view); + assert(v.code == AppMessageSkipCode.EpochMismatch); +} + +// **AMGSD-04** - empty ciphertext rejected. +test amgsd_04_empty_ciphertext_rejected { + var p = ok_packet(); + p.ciphertext_len = 0; + var view = ok_view(); + const v = validate_app_message_skip(p, view); + assert(v.code == AppMessageSkipCode.CiphertextEmpty); +} + +// **AMGSD-05** - zero generation rejected: the counter starts at 1. +test amgsd_05_zero_generation_rejected { + var p = ok_packet(); + p.generation = 0; + var view = ok_view(); + const v = validate_app_message_skip(p, view); + assert(v.code == AppMessageSkipCode.ZeroGeneration); +} + +// **AMGSD-06** - non-monotonic generation (equal to last seen 10) +// rejected. +test amgsd_06_non_monotonic_equal_rejected { + var p = ok_packet(); + p.generation = 10; + var view = ok_view(); + const v = validate_app_message_skip(p, view); + assert(v.code == AppMessageSkipCode.NonMonotonicGeneration); +} + +// **AMGSD-07** - non-monotonic generation (lower than last seen 10) +// rejected - the explicit replay. +test amgsd_07_non_monotonic_lower_rejected { + var p = ok_packet(); + p.generation = 5; + var view = ok_view(); + const v = validate_app_message_skip(p, view); + assert(v.code == AppMessageSkipCode.NonMonotonicGeneration); +} + +// **AMGSD-08** - skip distance one past the cap rejected - the +// DoS-resistance core: last seen 10, generation 10 + 1 + 1024 + 1. +test amgsd_08_skip_distance_just_over_cap_rejected { + var p = ok_packet(); + p.generation = 10 + 1 + (APP_MSG_SKIP_WINDOW + 1); + var view = ok_view(); + const v = validate_app_message_skip(p, view); + assert(v.code == AppMessageSkipCode.SkipDistanceExceeded); +} + +// **AMGSD-09** - skip distance exactly at the cap accepted - the +// boundary of the window: generation 10 + 1 + 1024. +test amgsd_09_skip_distance_at_cap_accepted { + var p = ok_packet(); + p.generation = 10 + 1 + APP_MSG_SKIP_WINDOW; + var view = ok_view(); + const v = validate_app_message_skip(p, view); + assert(v.code == AppMessageSkipCode.Ok); +} + +// **AMGSD-10** - the canonical packet (skip distance 0) accepted. +test amgsd_10_canonical_packet_accepted { + var view = ok_view(); + const v = validate_app_message_skip(ok_packet(), view); + assert(v.code == AppMessageSkipCode.Ok); +} + +// The three helpers have direct tests (coverage: Untested 0). +test ids_equal_answers { + assert(ids_equal(SENDER_A, SENDER_A)); + assert(!ids_equal(SENDER_A, SENDER_B)); +} + +test sender_known_answers { + const t: [2]SenderId = [2]SenderId{ SenderId { id: SENDER_A, }, SenderId { id: SENDER_B, }, }; + const u: [2]SenderId = [2]SenderId{ SenderId { id: SENDER_A, }, SenderId { id: EMPTY_ROW.sender, }, }; + assert(sender_known(SENDER_A, t)); + assert(!sender_known(SENDER_B, u)); +} + +test last_seen_for_answers { + const t: [2]GenRow = [2]GenRow{ GenRow { sender: SENDER_A, epoch: 7, last: 10, }, EMPTY_ROW, }; + assert(last_seen_for(SENDER_A, 7, t) == 10); + assert(last_seen_for(SENDER_A, 6, t) == 0); + assert(last_seen_for(SENDER_B, 7, t) == 0); +} + +// Rule order is the original's: sender length before known-sender, +// epoch before ciphertext emptiness, ciphertext before zero generation, +// monotonicity before the skip window. +test rule_order_matches_original { + var p = ok_packet(); + p.sender_id_len = 8; + p.epoch = 6; + var view = ok_view(); + const va = validate_app_message_skip(p, view); + assert(va.code == AppMessageSkipCode.NonCanonicalSenderIdLength); + + var q = ok_packet(); + q.epoch = 6; + q.ciphertext_len = 0; + var w = ok_view(); + const vb = validate_app_message_skip(q, w); + assert(vb.code == AppMessageSkipCode.EpochMismatch); +}