diff --git a/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-04::src::mac_truncation.json b/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-04::src::mac_truncation.json new file mode 100644 index 0000000000..d8cd2edafb --- /dev/null +++ b/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-04::src::mac_truncation.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:2472637916229b9eb8b7084f360f2b0cfa1494161222a8f6c8ef50b8051c0e8f", + "gen_hash_rust": "sha256:80c92ce669dfc4a98d756a7220754de457336f7e1d7e144ebf267ac6fa16910f", + "gen_hash_verilog": "sha256:59d88717eef90fe5a44694b3b7e2e561e60536e9e1e143415075e71da53f3fad", + "gen_hash_zig": "sha256:153eff87ecaaf3e11d381d86eec93efbb4f6f9c11debbfb3406aa360b6f28924", + "module": "port::trios::crates::trios-chat::rings::CR-CHAT-04::src::mac_truncation", + "ring": 12, + "seal_schema": 2, + "sealed_at": "2026-10-17T00:28:07Z", + "sealed_by": "t27c-bootstrap@0.5.2", + "spec_hash": "sha256:9c3547e53c1da0f70ee74ebb609c0027d6731529b0e15e8df880f8cc9ab3f0b9", + "spec_path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/mac_truncation.t27", + "tests": { + "failed": 0, + "failing": [], + "forced": false, + "passed": 11, + "total": 11, + "vacuous": 0 + }, + "toolchain": { + "test_runner": "sha256:1982ae948e24d00c5d221ccec12dfce1eb01204b53e37b0f857f93b16d64629d", + "zig": "0.16.0" + } +} \ No newline at end of file diff --git a/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-04::src::padding_ciphertext_length_consistency_guard.json b/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-04::src::padding_ciphertext_length_consistency_guard.json new file mode 100644 index 0000000000..2b7b773ed5 --- /dev/null +++ b/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-04::src::padding_ciphertext_length_consistency_guard.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:34ccb2881931ec3d55fbbe533b012d2fe5cec64a1bf3bc129bc1fb7d105d24ce", + "gen_hash_rust": "sha256:14448b9a934b77a424dbd231152216ee46f1f50883f51857128681dc72b86268", + "gen_hash_verilog": "sha256:4140dd44258be8b26b21ac1c822dc1febfbc0652809b21fa160890a0018cb871", + "gen_hash_zig": "sha256:50e6681bcf0806b043797486e6caf9776f31259ce73e7f3de4d5417a65f858dc", + "module": "port::trios::crates::trios-chat::rings::CR-CHAT-04::src::padding_ciphertext_length_consistency_guard", + "ring": 12, + "seal_schema": 2, + "sealed_at": "2026-10-16T14:45:29Z", + "sealed_by": "t27c-bootstrap@0.5.2", + "spec_hash": "sha256:47ec189874c25800c97f00c7c1049f12c435ca108d9bbf940438a4f3fcc6c224", + "spec_path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_ciphertext_length_consistency_guard.t27", + "tests": { + "failed": 0, + "failing": [], + "forced": false, + "passed": 12, + "total": 12, + "vacuous": 0 + }, + "toolchain": { + "test_runner": "sha256:1982ae948e24d00c5d221ccec12dfce1eb01204b53e37b0f857f93b16d64629d", + "zig": "0.16.0" + } +} \ No newline at end of file diff --git a/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-04::src::padding_class_downgrade_guard.json b/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-04::src::padding_class_downgrade_guard.json new file mode 100644 index 0000000000..b470166d0f --- /dev/null +++ b/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-04::src::padding_class_downgrade_guard.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:6107e045b4377de051491e22e7ef5a2231cc3ee1b63a444ff795c2beda87134e", + "gen_hash_rust": "sha256:e59f03fce02f279364e8635209f9ad4b58c834ccd96978da1a6044534213cb0e", + "gen_hash_verilog": "sha256:c40a564ebda4aa514a10f39939efc8559318736e86eb7d7b64a4bff117df60a8", + "gen_hash_zig": "sha256:662eefcc9a23b824c8f30159a77851312dc9fd46ac120b6cf2397cf4b880fc53", + "module": "port::trios::crates::trios-chat::rings::CR-CHAT-04::src::padding_class_downgrade_guard", + "ring": 12, + "seal_schema": 2, + "sealed_at": "2026-10-16T15:10:50Z", + "sealed_by": "t27c-bootstrap@0.5.2", + "spec_hash": "sha256:73ee43b21aee93eebddb92ab7eb36b705bd382cc6c519a197926e5f0190a84a9", + "spec_path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_class_downgrade_guard.t27", + "tests": { + "failed": 0, + "failing": [], + "forced": false, + "passed": 12, + "total": 12, + "vacuous": 0 + }, + "toolchain": { + "test_runner": "sha256:1982ae948e24d00c5d221ccec12dfce1eb01204b53e37b0f857f93b16d64629d", + "zig": "0.16.0" + } +} \ No newline at end of file diff --git a/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-04::src::padding_oracle_timing_sidechannel.json b/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-04::src::padding_oracle_timing_sidechannel.json new file mode 100644 index 0000000000..7963232880 --- /dev/null +++ b/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-04::src::padding_oracle_timing_sidechannel.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:19698787ba3df4d2d57b3c4f3b829495e3c5fe6c32351e4292d248768dd587a3", + "gen_hash_rust": "sha256:f2c46aee741b67b4c24c21fdda09d4aa4f6fc75f40e679dd1ea2ea3b334b66c3", + "gen_hash_verilog": "sha256:24d458163413022a7995553a49ecff02b22d5942914c6b1521c305d76db22050", + "gen_hash_zig": "sha256:62a43bd156acc2baa05439317043ded3ae691f47b996d9766ce1bdc2f5e4a394", + "module": "port::trios::crates::trios-chat::rings::CR-CHAT-04::src::padding_oracle_timing_sidechannel", + "ring": 12, + "seal_schema": 2, + "sealed_at": "2026-10-16T12:25:40Z", + "sealed_by": "t27c-bootstrap@0.5.2", + "spec_hash": "sha256:e70f365dd769ebd9bc7922d2f564df0096d6e4c4944c7bca916c6efed667af80", + "spec_path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_oracle_timing_sidechannel.t27", + "tests": { + "failed": 0, + "failing": [], + "forced": false, + "passed": 12, + "total": 12, + "vacuous": 0 + }, + "toolchain": { + "test_runner": "sha256:1982ae948e24d00c5d221ccec12dfce1eb01204b53e37b0f857f93b16d64629d", + "zig": "0.16.0" + } +} \ No newline at end of file diff --git a/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-04::src::safety_number.json b/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-04::src::safety_number.json new file mode 100644 index 0000000000..0ff5472bd1 --- /dev/null +++ b/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-04::src::safety_number.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:0e3eca72ecc964fd826cf384ca27e651feffe7eff2255db57fb64407407009a3", + "gen_hash_rust": "sha256:523935ae1031e20735ae7a9fa62057f0636d671c08364042207c7c4b763b6cd2", + "gen_hash_verilog": "sha256:50564f05903758c6eeb492013799c727638cf9d9e04223580ee8ff6dfd71ae3b", + "gen_hash_zig": "sha256:c2af7ff8deacc4587f29a34a99dc917be3a3c95e302df43d262f9c822ed48f40", + "module": "port::trios::crates::trios-chat::rings::CR-CHAT-04::src::safety_number", + "ring": 12, + "seal_schema": 2, + "sealed_at": "2026-10-17T00:37:25Z", + "sealed_by": "t27c-bootstrap@0.5.2", + "spec_hash": "sha256:c7b566d21e71d132f35cdb0a9a792aca02886240189cc8d5c54cbb6cd45407a8", + "spec_path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/safety_number.t27", + "tests": { + "failed": 0, + "failing": [], + "forced": false, + "passed": 6, + "total": 6, + "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 ab985e7951..537ba8aeca 100644 --- a/docs/reports/t27b_expectations.json +++ b/docs/reports/t27b_expectations.json @@ -877,12 +877,15 @@ {"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/external_init_secret_pinning.t27", "t27b": "pass"}, {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/header_extension_order_guard.t27", "t27b": "pass"}, + {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/mac_truncation.t27", "t27b": "pass"}, {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/mls_plaintext_framing_integrity.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-04/src/padding_byte_entropy_guard.t27", "t27b": "pass"}, {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_byte_pattern_uniformity_guard.t27", "t27b": "pass"}, + {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_ciphertext_length_consistency_guard.t27", "t27b": "pass"}, {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_class_collision_guard.t27", "t27b": "pass"}, + {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_class_downgrade_guard.t27", "t27b": "pass"}, {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_class_oracle.t27", "t27b": "pass"}, {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_class_selection_entropy_guard.t27", "t27b": "pass"}, {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_class_transition_audit.t27", "t27b": "pass"}, @@ -893,6 +896,8 @@ {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_key_derivation_domain_separation_guard.t27", "t27b": "pass"}, {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_length_class_transition_uniformity_guard.t27", "t27b": "pass"}, {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_length_distribution_guard.t27", "t27b": "pass"}, + {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_oracle_timing_sidechannel.t27", "t27b": "pass"}, + {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/safety_number.t27", "t27b": "pass"}, {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-05/src/envelope_size_distribution_uniformity.t27", "t27b": "pass"}, {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-07/src/blind_signature_sender_token.t27", "t27b": "pass"}, {"path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-07/src/cover_decoy_ratio_governor.t27", "t27b": "pass"}, diff --git a/specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/mac_truncation.t27 b/specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/mac_truncation.t27 new file mode 100644 index 0000000000..85d217e931 --- /dev/null +++ b/specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/mac_truncation.t27 @@ -0,0 +1,299 @@ +module port::trios::crates::trios-chat::rings::CR-CHAT-04::src::mac_truncation; + +// Port of gHashTag/trios crates/trios-chat/rings/CR-CHAT-04/src/mac_truncation.rs +// (CR-CHAT-04 - AEAD/MAC tag truncation defence, Wave-22 Lane B, +// L-CHAT-9-mt, requirement R-CHAT-4). +// +// Every encrypted chat frame ends with a sixteen-byte AEAD tag. +// The truncation family of attacks strips trailing tag bytes - +// a verifier comparing only the bytes that arrived forgives with +// probability 2^-8(16-k) instead of 2^-128, and a two-byte strip +// lands the forgery inside an online brute-force budget. The +// defence: sixteen is the only accepted tag length, the length +// is checked before any byte is compared, the compare reads all +// sixteen bytes with no early exit, and the frame split treats +// the trailer as its own domain. +// +// The original returns Result with four variants +// carrying no payloads. This port carries every outcome as one +// named struct (owner decision D5): Ok first, then the variants +// in the original's declaration order - Truncated, Oversized, +// Mismatch, FrameTooShort - plus the fields the accepted forms +// deliver: the constructed or split tag bytes and the split +// payload length (the original's returned slice becomes its +// length; the bytes live in the caller's frame). +// +// The original's subtle::ConstantTimeEq fold becomes a sum of +// absolute byte differences over all sixteen positions - every +// byte is read, no early exit, the sum is zero exactly when the +// tags match. The t27 backends carry no bitwise primitives, and +// the sum-zero equivalence is exact. The original's MacTag +// newtype becomes a record holding the fixed [16]u8 form. + +// The only accepted MAC tag length, in bytes. +pub const MAC_TAG_LEN: usize = 16; + +// A strongly-typed 16-byte MAC tag. +pub struct MacTag { + bytes: [16]u8, +} + +// Outcome codes: Ok and MacError's variants, in declaration order. +pub enum MacCode { + Ok, + Truncated, + Oversized, + Mismatch, + FrameTooShort, +} + +// The outcome of a tag construction, verification or frame split: +// the code, the tag the accepted forms deliver, and the split +// payload length. +pub struct MacOutcome { + code: MacCode, + payload_len: usize, + tag: [16]u8, +} + +// Constant-time equality over the fixed sixteen tag bytes: the +// absolute difference of every position accumulates, and the sum +// is zero exactly when the tags match - all bytes read, no +// early exit. +pub fn ct_eq(a: MacTag, b: MacTag) -> bool { + var da: usize = 0; + var db: usize = 0; + var diff: usize = 0; + for i in 0..16 { + da = @as(usize, a.bytes[i]); + db = @as(usize, b.bytes[i]); + if (da > db) { + diff = diff + (da - db); + } else { + diff = diff + (db - da); + } + } + return diff == 0; +} + +// Construct a tag from a slice: any length but sixteen answers +// Truncated or Oversized before a single byte is read, exactly +// the original's from_slice. +pub fn from_slice(bytes: []const u8) -> MacOutcome { + if (bytes.len < MAC_TAG_LEN) { + return MacOutcome { code: MacCode.Truncated, payload_len: 0, tag: ZERO_TAG, }; + } + if (bytes.len > MAC_TAG_LEN) { + return MacOutcome { code: MacCode.Oversized, payload_len: 0, tag: ZERO_TAG, }; + } + var tag: [16]u8 = ZERO_TAG; + for i in 0..16 { + tag[i] = bytes[i]; + } + return MacOutcome { code: MacCode.Ok, payload_len: 0, tag: tag, }; +} + +// Verify an arrived tag against the expected one: the length is +// checked first - the arrived length is the framing's public +// quantity - and only a full-length arrival reaches the +// sixteen-byte compare, which leaks no differing position. +pub fn verify_mac(expected: MacTag, arrived: []const u8) -> MacOutcome { + if (arrived.len < MAC_TAG_LEN) { + return MacOutcome { code: MacCode.Truncated, payload_len: 0, tag: ZERO_TAG, }; + } + if (arrived.len > MAC_TAG_LEN) { + return MacOutcome { code: MacCode.Oversized, payload_len: 0, tag: ZERO_TAG, }; + } + var arrived_tag: [16]u8 = ZERO_TAG; + for i in 0..16 { + arrived_tag[i] = arrived[i]; + } + if (ct_eq(expected, MacTag { bytes: arrived_tag, })) { + return MacOutcome { code: MacCode.Ok, payload_len: 0, tag: arrived_tag, }; + } + return MacOutcome { code: MacCode.Mismatch, payload_len: 0, tag: ZERO_TAG, }; +} + +// Split a wire frame into its payload length and its trailing +// tag. A frame shorter than the tag cannot hold one; the split +// reads the last sixteen bytes as the tag's own domain. +pub fn split_frame(frame: []const u8) -> MacOutcome { + if (frame.len < MAC_TAG_LEN) { + return MacOutcome { code: MacCode.FrameTooShort, payload_len: 0, tag: ZERO_TAG, }; + } + const cut: usize = frame.len - MAC_TAG_LEN; + var tag: [16]u8 = ZERO_TAG; + for j in 0..16 { + tag[j] = frame[cut + j]; + } + return MacOutcome { code: MacCode.Ok, payload_len: cut, tag: tag, }; +} + +// The all-zero tag - the empty form of the fixed sixteen bytes. +pub const ZERO_TAG: [16]u8 = [16]u8{0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,}; + +// The canonical tag of the fixtures, byte by byte. +pub const CANONICAL_BYTES: [16]u8 = [16]u8{1, 35, 69, 103, 137, 171, 205, 239, 254, 220, 186, 152, 118, 84, 50, 16,}; + +// The canonical tag with its eighth byte flipped by one - the +// single-byte mutation of MT-05. +pub const MUTATED_BYTES: [16]u8 = [16]u8{1, 35, 69, 103, 137, 171, 204, 239, 254, 220, 186, 152, 118, 84, 50, 16,}; + +// The canonical tag with the top bit of its last byte flipped - +// the single-bit flip of MT-09. +pub const FLIPPED_BYTES: [16]u8 = [16]u8{1, 35, 69, 103, 137, 171, 205, 239, 254, 220, 186, 152, 118, 84, 50, 144,}; + +// The first fifteen canonical bytes - the one-byte strip. +pub const SHORT_15: [15]u8 = [15]u8{1, 35, 69, 103, 137, 171, 205, 239, 254, 220, 186, 152, 118, 84, 50,}; + +// The first fourteen canonical bytes - the two-byte strip of the +// 2^-16 brute-force regime. +pub const SHORT_14: [14]u8 = [14]u8{1, 35, 69, 103, 137, 171, 205, 239, 254, 220, 186, 152, 118, 84,}; + +// The canonical tag plus one trailing byte - the length-extension +// attack of MT-04. +pub const LONG_17: [17]u8 = [17]u8{1, 35, 69, 103, 137, 171, 205, 239, 254, 220, 186, 152, 118, 84, 50, 16, 170,}; + +// **MT-01** - identical full-length tags accepted. +test mt_01_full_match_accepted { + const expected: MacTag = MacTag { bytes: CANONICAL_BYTES, }; + const v = verify_mac(expected, &CANONICAL_BYTES); + assert(v.code == MacCode.Ok); +} + +// **MT-02** - a single trailing byte stripped rejected as +// Truncated - even though every arrived byte matches. +test mt_02_strip_one_byte_rejected { + const expected: MacTag = MacTag { bytes: CANONICAL_BYTES, }; + const v = verify_mac(expected, &SHORT_15); + assert(v.code == MacCode.Truncated); +} + +// **MT-03** - a two-byte truncation rejected - the 2^-16 regime +// never reached. +test mt_03_strip_two_bytes_rejected { + const expected: MacTag = MacTag { bytes: CANONICAL_BYTES, }; + const v = verify_mac(expected, &SHORT_14); + assert(v.code == MacCode.Truncated); +} + +// **MT-04** - a length-extension (oversized) tag rejected as +// Oversized. +test mt_04_oversized_rejected { + const expected: MacTag = MacTag { bytes: CANONICAL_BYTES, }; + const v = verify_mac(expected, &LONG_17); + assert(v.code == MacCode.Oversized); +} + +// **MT-05** - a single-byte mutation at full length rejected as +// Mismatch - the eighth byte carries 0xCC where 0xCD belongs. +test mt_05_mismatch_rejected { + const expected: MacTag = MacTag { bytes: CANONICAL_BYTES, }; + const v = verify_mac(expected, &MUTATED_BYTES); + assert(v.code == MacCode.Mismatch); +} + +// **MT-06** - an empty tag rejected at construction - the +// degenerate no-tag-at-all case. +test mt_06_empty_tag_rejected_at_construction { + const empty: [0]u8 = [0]u8{}; + const v = from_slice(&empty); + assert(v.code == MacCode.Truncated); +} + +// **MT-07** - split_frame of a 32-byte frame: sixteen payload +// bytes and the trailing canonical tag. +test mt_07_split_frame_canonical { + var frame: [32]u8; + for i in 0..16 { + frame[i] = 0; + } + for j in 0..16 { + frame[16 + j] = CANONICAL_BYTES[j]; + } + const v = split_frame(&frame); + assert(v.code == MacCode.Ok); + assert(v.payload_len == 16); + const got: MacTag = MacTag { bytes: v.tag, }; + const want: MacTag = MacTag { bytes: CANONICAL_BYTES, }; + assert(ct_eq(got, want)); +} + +// **MT-08** - split_frame of a frame shorter than the tag +// rejected as FrameTooShort. +test mt_08_split_frame_too_short { + var frame: [15]u8; + for i in 0..15 { + frame[i] = 0; + } + const v = split_frame(&frame); + assert(v.code == MacCode.FrameTooShort); +} + +// **MT-09** - constant-time equality: one on the identical pair, +// zero on a single flipped bit. +test mt_09_ct_eq_single_bit_flip { + const t: MacTag = MacTag { bytes: CANONICAL_BYTES, }; + const other: MacTag = MacTag { bytes: FLIPPED_BYTES, }; + assert(ct_eq(t, t)); + assert(!ct_eq(t, other)); +} + +// **MT-10** - end-to-end: build a frame, split it, verify the tag +// against the canonical expected - the payload's spot bytes +// confirm the split domain. +test mt_10_e2e_split_then_verify { + var frame: [32]u8; + frame[0] = 104; + frame[1] = 101; + frame[2] = 108; + frame[3] = 108; + frame[4] = 111; + frame[5] = 45; + frame[6] = 116; + frame[7] = 114; + frame[8] = 105; + frame[9] = 110; + frame[10] = 105; + frame[11] = 116; + frame[12] = 121; + frame[13] = 45; + frame[14] = 50; + frame[15] = 50; + for j in 0..16 { + frame[16 + j] = CANONICAL_BYTES[j]; + } + const v = split_frame(&frame); + assert(v.code == MacCode.Ok); + assert(v.payload_len == 16); + assert(frame[0] == 104); + assert(frame[15] == 50); + const expected: MacTag = MacTag { bytes: CANONICAL_BYTES, }; + const arrived: MacTag = MacTag { bytes: v.tag, }; + const check = verify_mac(expected, &arrived.bytes); + assert(check.code == MacCode.Ok); +} + +// Rule order is the original's: the length checks before any +// byte compare (a short arrival whose bytes all match still +// answers Truncated), the frame floor before the split, and the +// split of an exactly-sixteen-byte frame yielding an empty +// payload with the whole frame as the tag. +test rule_order_matches_original { + const expected: MacTag = MacTag { bytes: CANONICAL_BYTES, }; + const short_matching = verify_mac(expected, &SHORT_15); + assert(short_matching.code == MacCode.Truncated); + + const oversized = from_slice(&LONG_17); + assert(oversized.code == MacCode.Oversized); + + var bare_tag_frame: [16]u8; + for j in 0..16 { + bare_tag_frame[j] = CANONICAL_BYTES[j]; + } + const bare = split_frame(&bare_tag_frame); + assert(bare.code == MacCode.Ok); + assert(bare.payload_len == 0); + const bare_tag: MacTag = MacTag { bytes: bare.tag, }; + assert(ct_eq(bare_tag, expected)); +} diff --git a/specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_ciphertext_length_consistency_guard.t27 b/specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_ciphertext_length_consistency_guard.t27 new file mode 100644 index 0000000000..cb5bb5d700 --- /dev/null +++ b/specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_ciphertext_length_consistency_guard.t27 @@ -0,0 +1,281 @@ +module port::trios::crates::trios-chat::rings::CR-CHAT-04::src::padding_ciphertext_length_consistency_guard; + +// Port of gHashTag/trios crates/trios-chat/rings/CR-CHAT-04/src/padding_ciphertext_length_consistency_guard.rs +// (CR-CHAT-04 - Padding ciphertext length consistency guard, +// Wave-109 Lane B, requirement R-CHAT-4). +// +// Each padding class has a fixed wire size: two ciphertexts of +// the same class differing by a byte break the size-class +// privacy, off-by-one padding leaks a payload of exactly +// class minus one, and unique lengths fingerprint sessions +// across epochs. The rules, in the original's order: the batch +// ceiling, then per record the zero-length probe, the +// class-canonical scan, the length-canonical scan and the +// class-consistency check - a length need not equal its class, +// only every record of one class must agree. +// +// The original returns Result<(), LengthConsistencyError>. This +// port carries the verdict as a named struct (owner decision D5): +// Ok first, then the five error variants in the original's +// declaration order - Inconsistent, NotCanonical, InvalidClass, +// ZeroLength, TooMany - with every payload field: class, +// expected and got for Inconsistent, the offending length or +// class for the canonical rules, idx for the zero-length rule, +// and got and max for the ceiling. +// +// The original's BTreeMap class-to-length becomes four scalar +// slots (the conventions' fixed form) - the zero-length rule +// runs before the map, so the all-zero slot doubles as the +// unseen marker without collision. The canonical-class set +// becomes a scan over the class ladder. + +// Canonical padding classes. +pub const PCLG_CLASSES: [4]usize = [4]usize{256, 1024, 4096, 16384,}; + +// Maximum ciphertexts per batch. +pub const PCLG_MAX_CIPHERTEXTS: usize = 10000; + +// A ciphertext with its class assignment. +pub struct CiphertextRecord { + class: usize, + length: usize, +} + +// Verdict codes: Ok(()) and LengthConsistencyError's variants, in declaration order. +pub enum LengthConsistencyCode { + Ok, + Inconsistent, + NotCanonical, + InvalidClass, + ZeroLength, + TooMany, +} + +// The verdict of the length consistency validation, with every +// error payload field. +pub struct LengthConsistencyVerdict { + code: LengthConsistencyCode, + idx: usize, + class: usize, + expected: usize, + got: usize, + bound: usize, +} + +// Whether the value is one of the four canonical classes - the +// original's BTreeSet membership probes, answered by a scan. +pub fn is_canonical(v: usize) -> bool { + for c in PCLG_CLASSES { + if (c == v) { + return true; + } + } + return false; +} + +// The slot of a class in the consistency table - 4 marks a class +// no rule accepted, never reached by the consistency check. +pub fn class_slot(class: usize) -> usize { + if (class == 256) { + return 0; + } + if (class == 1024) { + return 1; + } + if (class == 4096) { + return 2; + } + if (class == 16384) { + return 3; + } + return 4; +} + +// [VERIFIED] Validate padding ciphertext length consistency. +// Returns Ok only when every rule holds, checked in the +// original's order: the batch ceiling, then per record the zero +// length, the class-canonical scan, the length-canonical scan +// and the class-consistency check. +pub fn validate_length_consistency(records: []const CiphertextRecord) -> LengthConsistencyVerdict { + if (records.len > PCLG_MAX_CIPHERTEXTS) { + return LengthConsistencyVerdict { code: LengthConsistencyCode.TooMany, idx: 0, class: 0, expected: 0, got: records.len, bound: PCLG_MAX_CIPHERTEXTS, }; + } + var slots: [4]usize = [4]usize{0, 0, 0, 0,}; + var slot: usize = 0; + for i in 0..records.len { + if (records[i].length == 0) { + return LengthConsistencyVerdict { code: LengthConsistencyCode.ZeroLength, idx: i, class: 0, expected: 0, got: 0, bound: 0, }; + } + if (!is_canonical(records[i].class)) { + return LengthConsistencyVerdict { code: LengthConsistencyCode.InvalidClass, idx: i, class: records[i].class, expected: 0, got: 0, bound: 0, }; + } + if (!is_canonical(records[i].length)) { + return LengthConsistencyVerdict { code: LengthConsistencyCode.NotCanonical, idx: i, class: 0, expected: 0, got: records[i].length, bound: 0, }; + } + slot = class_slot(records[i].class); + if (slots[slot] == 0) { + slots[slot] = records[i].length; + } else { + if (records[i].length != slots[slot]) { + return LengthConsistencyVerdict { code: LengthConsistencyCode.Inconsistent, idx: i, class: records[i].class, expected: slots[slot], got: records[i].length, bound: 0, }; + } + } + } + return LengthConsistencyVerdict { code: LengthConsistencyCode.Ok, idx: 0, class: 0, expected: 0, got: 0, bound: 0, }; +} + +// **PCLG-01** - inconsistent length within a class rejected: +// the second 256-class ciphertext carries 1024 bytes. +test pclg_01_inconsistent_rejected { + const records: [2]CiphertextRecord = [2]CiphertextRecord{ + CiphertextRecord { class: 256, length: 256, }, + CiphertextRecord { class: 256, length: 1024, }, + }; + const v = validate_length_consistency(&records); + assert(v.code == LengthConsistencyCode.Inconsistent); + assert(v.class == 256); + assert(v.expected == 256); + assert(v.got == 1024); +} + +// **PCLG-02** - non-canonical length rejected: three hundred +// bytes is no class size. +test pclg_02_not_canonical_rejected { + const records: [1]CiphertextRecord = [1]CiphertextRecord{ + CiphertextRecord { class: 256, length: 300, }, + }; + const v = validate_length_consistency(&records); + assert(v.code == LengthConsistencyCode.NotCanonical); + assert(v.got == 300); +} + +// **PCLG-03** - invalid class rejected: five hundred is no class. +test pclg_03_invalid_class_rejected { + const records: [1]CiphertextRecord = [1]CiphertextRecord{ + CiphertextRecord { class: 500, length: 500, }, + }; + const v = validate_length_consistency(&records); + assert(v.code == LengthConsistencyCode.InvalidClass); + assert(v.class == 500); +} + +// **PCLG-04** - zero length rejected. +test pclg_04_zero_length_rejected { + const records: [1]CiphertextRecord = [1]CiphertextRecord{ + CiphertextRecord { class: 256, length: 0, }, + }; + const v = validate_length_consistency(&records); + assert(v.code == LengthConsistencyCode.ZeroLength); + assert(v.idx == 0); +} + +// **PCLG-05** - too many rejected: 10001 ciphertexts of a maximum +// 10000, built in a loop like the original's. The batch rule +// fires before any record is examined. +test pclg_05_too_many_rejected { + var records: [10001]CiphertextRecord; + for i in 0..10001 { + records[i] = CiphertextRecord { class: 256, length: 256, }; + } + const v = validate_length_consistency(&records); + assert(v.code == LengthConsistencyCode.TooMany); + assert(v.got == 10001); + assert(v.bound == 10000); +} + +// **PCLG-06** - a class carrying a different class's length +// accepted: consistency asks only that one class agree with +// itself, the first of its kind sets the expectation. +test pclg_06_class_length_mismatch_rejected { + const records: [1]CiphertextRecord = [1]CiphertextRecord{ + CiphertextRecord { class: 256, length: 1024, }, + }; + const v = validate_length_consistency(&records); + assert(v.code == LengthConsistencyCode.Ok); +} + +// **PCLG-07** - the valid batch accepted. +test pclg_07_valid_accepted { + const records: [4]CiphertextRecord = [4]CiphertextRecord{ + CiphertextRecord { class: 256, length: 256, }, + CiphertextRecord { class: 256, length: 256, }, + CiphertextRecord { class: 1024, length: 1024, }, + CiphertextRecord { class: 16384, length: 16384, }, + }; + const v = validate_length_consistency(&records); + assert(v.code == LengthConsistencyCode.Ok); +} + +// **PCLG-08** - an empty batch accepted. +test pclg_08_empty_accepted { + const records: [0]CiphertextRecord = [0]CiphertextRecord{}; + const v = validate_length_consistency(&records); + assert(v.code == LengthConsistencyCode.Ok); +} + +// **PCLG-09** - one ciphertext per class accepted. +test pclg_09_single_per_class_accepted { + const records: [4]CiphertextRecord = [4]CiphertextRecord{ + CiphertextRecord { class: 256, length: 256, }, + CiphertextRecord { class: 1024, length: 1024, }, + CiphertextRecord { class: 4096, length: 4096, }, + CiphertextRecord { class: 16384, length: 16384, }, + }; + const v = validate_length_consistency(&records); + assert(v.code == LengthConsistencyCode.Ok); +} + +// **PCLG-10** - a large consistent batch accepted: a hundred +// rounds over the four classes. +test pclg_10_large_batch_accepted { + var records: [400]CiphertextRecord; + for i in 0..400 { + records[i] = CiphertextRecord { class: PCLG_CLASSES[i % 4], length: PCLG_CLASSES[i % 4], }; + } + const v = validate_length_consistency(&records); + assert(v.code == LengthConsistencyCode.Ok); +} + +// The two helpers have direct tests (coverage: Untested 0). +test pclg_helpers_answer { + assert(is_canonical(256)); + assert(is_canonical(1024)); + assert(is_canonical(4096)); + assert(is_canonical(16384)); + assert(!is_canonical(300)); + assert(!is_canonical(500)); + assert(!is_canonical(0)); + assert(class_slot(256) == 0); + assert(class_slot(1024) == 1); + assert(class_slot(4096) == 2); + assert(class_slot(16384) == 3); + assert(class_slot(500) == 4); +} + +// Rule order is the original's: the zero length before the class +// scan, the class scan before the length scan, and the length +// scan before the consistency check. +test rule_order_matches_original { + const zero_invalid: [1]CiphertextRecord = [1]CiphertextRecord{ + CiphertextRecord { class: 500, length: 0, }, + }; + const v1 = validate_length_consistency(&zero_invalid); + assert(v1.code == LengthConsistencyCode.ZeroLength); + assert(v1.idx == 0); + + const invalid_non_canonical: [1]CiphertextRecord = [1]CiphertextRecord{ + CiphertextRecord { class: 500, length: 300, }, + }; + const v2 = validate_length_consistency(&invalid_non_canonical); + assert(v2.code == LengthConsistencyCode.InvalidClass); + assert(v2.class == 500); + + const non_canonical_inconsistent: [2]CiphertextRecord = [2]CiphertextRecord{ + CiphertextRecord { class: 256, length: 256, }, + CiphertextRecord { class: 256, length: 300, }, + }; + const v3 = validate_length_consistency(&non_canonical_inconsistent); + assert(v3.code == LengthConsistencyCode.NotCanonical); + assert(v3.got == 300); + assert(v3.idx == 1); +} diff --git a/specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_class_downgrade_guard.t27 b/specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_class_downgrade_guard.t27 new file mode 100644 index 0000000000..dbee8220f7 --- /dev/null +++ b/specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_class_downgrade_guard.t27 @@ -0,0 +1,229 @@ +module port::trios::crates::trios-chat::rings::CR-CHAT-04::src::padding_class_downgrade_guard; + +// Port of gHashTag/trios crates/trios-chat/rings/CR-CHAT-04/src/padding_class_downgrade_guard.rs +// (CR-CHAT-04 - Padding class downgrade guard, Wave-53 Lane B, +// requirement R-CHAT-9). +// +// Within a session the padding class may only grow: a shrink +// from 4096 to 256 tells an observer the plaintext became +// shorter and leaks its content. The rules, in the original's +// order: the batch ceiling, the empty log (accepted), then per +// entry the canonical-class probe and the non-decreasing check +// over the class ladder, and after the whole log the +// first-is-smallest and final-is-largest checks. +// +// The original returns Result<(), PadDowngradeError>. No +// variant carries a payload, so the verdict is the code alone +// (owner decision D5): Ok first, then the six variants in the +// original's declaration order - ClassDowngraded, +// NonCanonicalClass, DuplicateEntry, TooManyTransitions, +// FirstNotSmallest, FinalNotLargest. +// +// The original's DuplicateEntry is declared but never answered: +// its BTreeSet inserts (index, class) pairs and the index is +// unique per entry, so the insert never collides - repeated +// classes pass (PCDG-08 exercises exactly that). The variant +// stays in the enum, declared and unreachable exactly as in the +// original, and the dead insert drops out of the port. The +// original's Option class index becomes the sentinel +// four: the canonical check runs before any index use. + +// Canonical padding classes. +pub const PCDG_CLASSES: [4]usize = [4]usize{256, 1024, 4096, 16384,}; + +// Maximum transitions in a log. +pub const PCDG_MAX_TRANSITIONS: usize = 1024; + +// The sentinel class index for a non-canonical class. +pub const PCDG_NON_CANONICAL: usize = 4; + +// Verdict codes: Ok(()) and PadDowngradeError's variants, in declaration order. +pub enum PadDowngradeCode { + Ok, + ClassDowngraded, + NonCanonicalClass, + DuplicateEntry, + TooManyTransitions, + FirstNotSmallest, + FinalNotLargest, +} + +// The verdict of the downgrade validation. No variant of the +// original's error carries a payload, so the code is the whole +// verdict. +pub struct PadDowngradeVerdict { + code: PadDowngradeCode, +} + +// The ladder position of a class - the original's Option +// class_index, four marking a class the ladder does not hold. +pub fn class_index(cls: usize) -> usize { + if (cls == 256) { + return 0; + } + if (cls == 1024) { + return 1; + } + if (cls == 4096) { + return 2; + } + if (cls == 16384) { + return 3; + } + return PCDG_NON_CANONICAL; +} + +// [VERIFIED] Validate a sequence of padding class transitions. +// Returns Ok only when every rule holds, checked in the +// original's order: the batch ceiling, the empty log, then per +// entry the canonical class and the non-decreasing ladder walk, +// then the first-is-smallest and final-is-largest checks. +pub fn validate_padding_downgrade(transitions: []const usize) -> PadDowngradeVerdict { + if (transitions.len > PCDG_MAX_TRANSITIONS) { + return PadDowngradeVerdict { code: PadDowngradeCode.TooManyTransitions, }; + } + if (transitions.len == 0) { + return PadDowngradeVerdict { code: PadDowngradeCode.Ok, }; + } + var idx: usize = 0; + var prev_idx: usize = 0; + var first_idx: usize = 0; + for i in 0..transitions.len { + idx = class_index(transitions[i]); + if (idx == PCDG_NON_CANONICAL) { + return PadDowngradeVerdict { code: PadDowngradeCode.NonCanonicalClass, }; + } + if (i == 0) { + first_idx = idx; + } else { + if (idx < prev_idx) { + return PadDowngradeVerdict { code: PadDowngradeCode.ClassDowngraded, }; + } + } + prev_idx = idx; + } + if (first_idx != 0) { + return PadDowngradeVerdict { code: PadDowngradeCode.FirstNotSmallest, }; + } + if (idx != 3) { + return PadDowngradeVerdict { code: PadDowngradeCode.FinalNotLargest, }; + } + return PadDowngradeVerdict { code: PadDowngradeCode.Ok, }; +} + +// **PCDG-01** - a downgrade rejected: 256 after 1024. +test pcdg_01_downgrade_rejected { + const transitions: [3]usize = [3]usize{256, 1024, 256,}; + const v = validate_padding_downgrade(&transitions); + assert(v.code == PadDowngradeCode.ClassDowngraded); +} + +// **PCDG-02** - a non-canonical class rejected: 512 is on no +// ladder rung. +test pcdg_02_non_canonical_rejected { + const transitions: [1]usize = [1]usize{512,}; + const v = validate_padding_downgrade(&transitions); + assert(v.code == PadDowngradeCode.NonCanonicalClass); +} + +// **PCDG-03** - too many rejected: 1025 transitions of a maximum +// 1024, built in a loop like the original's. The batch rule +// fires before any entry is examined. +test pcdg_03_too_many_rejected { + var transitions: [1025]usize; + for i in 0..1025 { + transitions[i] = 256; + } + const v = validate_padding_downgrade(&transitions); + assert(v.code == PadDowngradeCode.TooManyTransitions); +} + +// **PCDG-04** - first not smallest rejected: the log opens on +// 1024. +test pcdg_04_first_not_smallest_rejected { + const transitions: [3]usize = [3]usize{1024, 4096, 16384,}; + const v = validate_padding_downgrade(&transitions); + assert(v.code == PadDowngradeCode.FirstNotSmallest); +} + +// **PCDG-05** - final not largest rejected: the log ends on +// 1024. +test pcdg_05_final_not_largest_rejected { + const transitions: [2]usize = [2]usize{256, 1024,}; + const v = validate_padding_downgrade(&transitions); + assert(v.code == PadDowngradeCode.FinalNotLargest); +} + +// **PCDG-06** - the full progression accepted: every rung once, +// ascending. +test pcdg_06_full_progression_accepted { + const transitions: [4]usize = [4]usize{256, 1024, 4096, 16384,}; + const v = validate_padding_downgrade(&transitions); + assert(v.code == PadDowngradeCode.Ok); +} + +// **PCDG-07** - an empty log accepted. +test pcdg_07_empty_accepted { + const transitions: [0]usize = [0]usize{}; + const v = validate_padding_downgrade(&transitions); + assert(v.code == PadDowngradeCode.Ok); +} + +// **PCDG-08** - repeated classes accepted: the original's dedup +// keys on the entry index, so a repeated class never collides - +// the unreachable-duplicate property this port keeps. +test pcdg_08_same_class_accepted { + const transitions: [4]usize = [4]usize{256, 256, 256, 16384,}; + const v = validate_padding_downgrade(&transitions); + assert(v.code == PadDowngradeCode.Ok); +} + +// **PCDG-09** - a skipped rung accepted: 256 straight to 16384. +test pcdg_09_skip_class_accepted { + const transitions: [2]usize = [2]usize{256, 16384,}; + const v = validate_padding_downgrade(&transitions); + assert(v.code == PadDowngradeCode.Ok); +} + +// **PCDG-10** - the canonical ladder itself accepted. +test pcdg_10_minimal_accepted { + const transitions: [4]usize = [4]usize{256, 1024, 4096, 16384,}; + const v = validate_padding_downgrade(&transitions); + assert(v.code == PadDowngradeCode.Ok); +} + +// The helper has a direct test (coverage: Untested 0). +test class_index_answers { + assert(class_index(256) == 0); + assert(class_index(1024) == 1); + assert(class_index(4096) == 2); + assert(class_index(16384) == 3); + assert(class_index(512) == 4); + assert(class_index(0) == 4); + assert(class_index(16385) == 4); +} + +// Rule order is the original's: the batch ceiling before any +// entry, the canonical probe before the ladder walk, the ladder +// walk before the post-loop checks, and the first check before +// the final check. +test rule_order_matches_original { + var flooded: [1025]usize; + for i in 0..1025 { + flooded[i] = 512; + } + const v1 = validate_padding_downgrade(&flooded); + assert(v1.code == PadDowngradeCode.TooManyTransitions); + + const non_canonical: [2]usize = [2]usize{512, 256,}; + const v2 = validate_padding_downgrade(&non_canonical); + assert(v2.code == PadDowngradeCode.NonCanonicalClass); + + const downgraded_first_bad: [3]usize = [3]usize{1024, 4096, 256,}; + const v3 = validate_padding_downgrade(&downgraded_first_bad); + assert(v3.code == PadDowngradeCode.ClassDowngraded); + + const both_post_bad: [2]usize = [2]usize{1024, 1024,}; + const v4 = validate_padding_downgrade(&both_post_bad); + assert(v4.code == PadDowngradeCode.FirstNotSmallest); +} diff --git a/specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_oracle_timing_sidechannel.t27 b/specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_oracle_timing_sidechannel.t27 new file mode 100644 index 0000000000..3430f0a878 --- /dev/null +++ b/specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_oracle_timing_sidechannel.t27 @@ -0,0 +1,299 @@ +module port::trios::crates::trios-chat::rings::CR-CHAT-04::src::padding_oracle_timing_sidechannel; + +// Port of gHashTag/trios crates/trios-chat/rings/CR-CHAT-04/src/padding_oracle_timing_sidechannel.rs +// (CR-CHAT-04 - Padding oracle timing side-channel guard, Wave-51 +// Lane A, requirement R-CHAT-9). +// +// Unpadding must cost time independent of the plaintext length: +// an adversary measuring unpad latency reads the original message +// size off the envelope and the padding class collapses back into +// a size oracle. The guard therefore walks the whole class every +// time - the wire length must equal the class size exactly, the +// payload prefix must fit the class bounds, and the padding region +// must be zeros to the end of the class. The rules, in the +// original's order: the wire-length floor, the wire-length ceiling, +// the class-size floor, the zero-payload probe, the payload ceiling +// and the zero-padding scan. +// +// The original returns Result<&[u8], PaddingTimingError> - the +// payload slice on accept. The port's verdict carries the code and +// the payload length; the bytes themselves live in the caller's +// wire and never reach the spec (owner decision D5). The codes +// keep the original's declaration order: Ok first, then +// WireDataTooShort, PayloadTooLong, LengthPrefixOverflow, +// NonZeroPadding, ZeroPayload and WireDataTooLong. +// +// The original declares LengthPrefixOverflow but never answers it: +// on the target the u32 length lands in usize without wrapping, so +// an oversized prefix always trips the payload ceiling first. The +// variant stays in the enum, declared and unreachable exactly as in +// the original. The length prefix folds from the first four wire +// bytes through the int-widening cast - no shift-and-truncate +// anywhere. + +// Length of the u32 BE payload-length prefix. +pub const POTC_LEN_PREFIX: usize = 4; + +// The class size of the standard fixtures. +pub const POTC_CLASS_64: usize = 64; + +// The class size of the larger fixture. +pub const POTC_CLASS_128: usize = 128; + +// Verdict codes: Ok(&[u8]) and PaddingTimingError's variants, in declaration order. +pub enum PaddingTimingCode { + Ok, + WireDataTooShort, + PayloadTooLong, + LengthPrefixOverflow, + NonZeroPadding, + ZeroPayload, + WireDataTooLong, +} + +// The verdict of one padded envelope: the code and, on accept, the +// payload length the wire carries. +pub struct PaddingTimingVerdict { + code: PaddingTimingCode, + payload_len: usize, +} + +// The big-endian u32 of the first four bytes - the original's +// u32::from_be_bytes, folded byte by byte through the +// int-widening cast. +pub fn read_be32(b: []const u8) -> u32 { + var v: u32 = 0; + var wide: u32 = 0; + for i in 0..4 { + wide = @as(u32, b[i]); + v = v * 256 + wide; + } + return v; +} + +// [VERIFIED] Validate a padded envelope against a class size. +// Returns Ok with the payload length only when every rule holds, +// checked in the original's order: the wire-length floor and +// ceiling, the class-size floor, the zero-payload probe, the +// payload ceiling, then the zero scan over the whole padding +// region to the end of the class. +pub fn validate_padded_envelope(wire: []const u8, class_size: usize) -> PaddingTimingVerdict { + if (wire.len < class_size) { + return PaddingTimingVerdict { code: PaddingTimingCode.WireDataTooShort, payload_len: 0, }; + } + if (wire.len > class_size) { + return PaddingTimingVerdict { code: PaddingTimingCode.WireDataTooLong, payload_len: 0, }; + } + if (class_size < POTC_LEN_PREFIX) { + return PaddingTimingVerdict { code: PaddingTimingCode.WireDataTooShort, payload_len: 0, }; + } + const payload_len32: u32 = read_be32(wire); + const payload_len: usize = @as(usize, payload_len32); + if (payload_len == 0) { + return PaddingTimingVerdict { code: PaddingTimingCode.ZeroPayload, payload_len: 0, }; + } + const max_payload: usize = class_size - POTC_LEN_PREFIX; + if (payload_len > max_payload) { + return PaddingTimingVerdict { code: PaddingTimingCode.PayloadTooLong, payload_len: 0, }; + } + const padding_start: usize = POTC_LEN_PREFIX + payload_len; + for j in padding_start..class_size { + if (wire[j] != 0) { + return PaddingTimingVerdict { code: PaddingTimingCode.NonZeroPadding, payload_len: 0, }; + } + } + return PaddingTimingVerdict { code: PaddingTimingCode.Ok, payload_len: payload_len, }; +} + +// **POTC-01** - a wire shorter than the class rejected before any +// byte is read. +test potc_01_wire_short_rejected { + var wire: [32]u8; + for j in 0..32 { + wire[j] = 0; + } + const r = validate_padded_envelope(&wire, POTC_CLASS_64); + assert(r.code == PaddingTimingCode.WireDataTooShort); +} + +// **POTC-02** - a wire longer than the class rejected. +test potc_02_wire_long_rejected { + var wire: [65]u8; + for j in 0..65 { + wire[j] = 0; + } + const r = validate_padded_envelope(&wire, POTC_CLASS_64); + assert(r.code == PaddingTimingCode.WireDataTooLong); +} + +// **POTC-03** - a payload prefix claiming the whole class +// rejected: sixty-four of a maximum sixty. +test potc_03_payload_long_rejected { + var wire: [64]u8; + for j in 0..64 { + wire[j] = 0; + } + wire[3] = 64; + const r = validate_padded_envelope(&wire, POTC_CLASS_64); + assert(r.code == PaddingTimingCode.PayloadTooLong); +} + +// **POTC-04** - a non-zero byte in the padding region rejected: +// the two-byte payload leaves the region starting at six, and its +// first byte carries 0x42. +test potc_04_nonzero_padding_rejected { + var wire: [64]u8; + for j in 0..64 { + wire[j] = 0; + } + wire[3] = 2; + wire[4] = 104; + wire[5] = 105; + wire[6] = 66; + const r = validate_padded_envelope(&wire, POTC_CLASS_64); + assert(r.code == PaddingTimingCode.NonZeroPadding); +} + +// **POTC-05** - a zero payload prefix rejected: the whole wire is +// zeros, the declared length is zero. +test potc_05_zero_payload_rejected { + var wire: [64]u8; + for j in 0..64 { + wire[j] = 0; + } + const r = validate_padded_envelope(&wire, POTC_CLASS_64); + assert(r.code == PaddingTimingCode.ZeroPayload); +} + +// **POTC-06** - the valid envelope accepted: "hello world", eleven +// bytes, padded to the class. +test potc_06_valid_accepted { + var wire: [64]u8; + for j in 0..64 { + wire[j] = 0; + } + wire[3] = 11; + wire[4] = 104; + wire[5] = 101; + wire[6] = 108; + wire[7] = 108; + wire[8] = 111; + wire[9] = 32; + wire[10] = 119; + wire[11] = 111; + wire[12] = 114; + wire[13] = 108; + wire[14] = 100; + const r = validate_padded_envelope(&wire, POTC_CLASS_64); + assert(r.code == PaddingTimingCode.Ok); + assert(r.payload_len == 11); +} + +// **POTC-07** - the exact maximum payload accepted: sixty bytes of +// 0xAA filling the whole payload region of the sixty-four class. +test potc_07_exact_max_payload_accepted { + var wire: [64]u8; + for j in 0..64 { + wire[j] = 0; + } + wire[3] = 60; + for j in 4..64 { + wire[j] = 170; + } + const r = validate_padded_envelope(&wire, POTC_CLASS_64); + assert(r.code == PaddingTimingCode.Ok); + assert(r.payload_len == 60); +} + +// **POTC-08** - a single-byte payload accepted. +test potc_08_single_byte_accepted { + var wire: [64]u8; + for j in 0..64 { + wire[j] = 0; + } + wire[3] = 1; + wire[4] = 88; + const r = validate_padded_envelope(&wire, POTC_CLASS_64); + assert(r.code == PaddingTimingCode.Ok); + assert(r.payload_len == 1); +} + +// **POTC-09** - the larger class accepted: "test payload", twelve +// bytes, padded to the hundred-twenty-eight class. +test potc_09_larger_class_accepted { + var wire: [128]u8; + for j in 0..128 { + wire[j] = 0; + } + wire[3] = 12; + wire[4] = 116; + wire[5] = 101; + wire[6] = 115; + wire[7] = 116; + wire[8] = 32; + wire[9] = 112; + wire[10] = 97; + wire[11] = 121; + wire[12] = 108; + wire[13] = 111; + wire[14] = 97; + wire[15] = 100; + const r = validate_padded_envelope(&wire, POTC_CLASS_128); + assert(r.code == PaddingTimingCode.Ok); + assert(r.payload_len == 12); +} + +// **POTC-10** - the all-ones length prefix rejected: the u32 +// maximum as a payload length is far over the sixty-byte ceiling. +test potc_10_len_overflow_rejected { + var wire: [64]u8; + for j in 0..64 { + wire[j] = 0; + } + wire[0] = 255; + wire[1] = 255; + wire[2] = 255; + wire[3] = 255; + const r = validate_padded_envelope(&wire, POTC_CLASS_64); + assert(r.code == PaddingTimingCode.PayloadTooLong); +} + +// The helper has a direct test (coverage: Untested 0). +test read_be32_answers { + var four: [4]u8 = [4]u8{0, 0, 0, 60,}; + assert(read_be32(&four) == 60); + var ones: [4]u8 = [4]u8{255, 255, 255, 255,}; + assert(read_be32(&ones) == 4294967295); + var span: [4]u8 = [4]u8{0, 0, 15, 160,}; + assert(read_be32(&span) == 4000); +} + +// Rule order is the original's: the wire-length floor before the +// prefix is read, the class-size floor before the payload probe, +// and the payload ceiling before the padding scan. +test rule_order_matches_original { + var short_hot: [32]u8; + for j in 0..32 { + short_hot[j] = 255; + } + const v1 = validate_padded_envelope(&short_hot, POTC_CLASS_64); + assert(v1.code == PaddingTimingCode.WireDataTooShort); + + var tiny: [2]u8; + for j in 0..2 { + tiny[j] = 0; + } + const v2 = validate_padded_envelope(&tiny, 2); + assert(v2.code == PaddingTimingCode.WireDataTooShort); + + var long_claim_garbage: [64]u8; + for j in 0..64 { + long_claim_garbage[j] = 255; + } + long_claim_garbage[0] = 0; + long_claim_garbage[1] = 0; + long_claim_garbage[2] = 0; + long_claim_garbage[3] = 61; + const v3 = validate_padded_envelope(&long_claim_garbage, POTC_CLASS_64); + assert(v3.code == PaddingTimingCode.PayloadTooLong); +} diff --git a/specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/safety_number.t27 b/specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/safety_number.t27 new file mode 100644 index 0000000000..040773e087 --- /dev/null +++ b/specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/safety_number.t27 @@ -0,0 +1,237 @@ +module port::trios::crates::trios-chat::rings::CR-CHAT-04::src::safety_number; + +// Port of gHashTag/trios crates/trios-chat/rings/CR-CHAT-04/src/safety_number.rs +// (CR-CHAT-04 - Safety-number / OOB identity verification, +// Wave-14 Lane A, L-CHAT-2-oob, requirement R-CHAT-4). +// +// A MITM owning the routing layer swaps one party's identity key +// during the handshake and all in-band traffic then authenticates +// under the swapped key. The safety number is the out-of-band +// fingerprint: a deterministic, commutative digest of both +// identity keys, displayed to the user and compared OOB - the +// bytewise-smaller key hashes first, so both parties compute the +// same value off either argument order. +// +// The module's logic ports whole; the hash does not. t27 carries +// no bitwise primitives, so SHA-256 stays with the caller: the +// spec's safety_number takes both hash orderings and selects the +// one its canonical key ordering dictates - commutativity is the +// ordering logic's own property and the port proves it. The +// render re-hash likewise arrives as a caller-computed 32-byte +// block; the display arithmetic is the module's own and ports +// exactly - the original's (lo << 8) | hi | (tail << 16) ORs +// disjoint byte positions, so the t27 form is the equal sum +// lo * 256 + hi + tail * 65536. +// +// SNV-03 and SNV-06 of the original pin SHA-256's collision +// resistance - a property of the hash function, not of this +// module's logic: a swapped key or a flipped bit changes the +// digest because the caller's hash says so. They stay with the +// caller's SHA-256 and are not carried into the spec; the +// port tests the ordering, the selection, the display +// arithmetic and the constant-time compare. +// +// The original's verify returns Result with an Invariant carrying +// the "safety_number_mismatch" message; the port's verdict is +// the code alone (the lane convention - the message is opaque). +// The constant-time compare folds the absolute difference of +// all thirty bytes - every byte read, no early exit. + +// Identity key length (Ed25519 / X25519 compatible). +pub const SN_ID_KEY_LEN: usize = 32; + +// Safety-number digest length: the first thirty bytes of the hash. +pub const SN_DIGEST_LEN: usize = 30; + +// Display groups per digest. +pub const SN_GROUPS: usize = 12; + +// The modulus of one display group: five decimal digits. +pub const SN_GROUP_MOD: u32 = 100000; + +// Verdict codes of the out-of-band compare. +pub enum VerifyCode { + Ok, + Mismatch, +} + +// The verdict of the safety-number compare. The original's error +// carries only an opaque message, so the code is the whole +// verdict. +pub struct VerifyVerdict { + code: VerifyCode, +} + +// Bytewise lexicographic a <= b: the first differing byte +// decides, equal keys compare true. +pub fn key_lte(a: [32]u8, b: [32]u8) -> bool { + for i in 0..32 { + if (a[i] != b[i]) { + if (a[i] < b[i]) { + return true; + } + return false; + } + } + return true; +} + +// The canonical safety-number digest for two identity keys: the +// bytewise-smaller key hashes first, so the caller's two hash +// orderings reduce to one selection - and either argument order +// selects the same digest. +pub fn safety_number(a: [32]u8, b: [32]u8, hash_ab: [30]u8, hash_ba: [30]u8) -> [30]u8 { + if (key_lte(a, b)) { + return hash_ab; + } + return hash_ba; +} + +// Render the display groups off the caller's re-hash of the +// digest: twelve groups, each (lo * 256 + hi + tail * 65536) +// modulo a hundred thousand - the original's shift-and-OR over +// disjoint byte positions as the equal sum. +pub fn render(r: [32]u8) -> [12]u32 { + var groups: [12]u32 = [12]u32{0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,}; + var lo: u32 = 0; + var hi: u32 = 0; + var tail: u32 = 0; + for i in 0..12 { + lo = @as(u32, r[2 * i]); + hi = @as(u32, r[2 * i + 1]); + tail = @as(u32, r[24 + (i % 8)]); + groups[i] = (lo * 256 + hi + tail * 65536) % SN_GROUP_MOD; + } + return groups; +} + +// Compare a received safety number against the locally computed +// one in constant time: the absolute difference of every digest +// byte accumulates, the sum zero exactly on a match. +pub fn verify(local: [30]u8, remote: [30]u8) -> VerifyVerdict { + var dl: usize = 0; + var dr: usize = 0; + var diff: usize = 0; + for i in 0..30 { + dl = @as(usize, local[i]); + dr = @as(usize, remote[i]); + if (dl > dr) { + diff = diff + (dl - dr); + } else { + diff = diff + (dr - dl); + } + } + if (diff == 0) { + return VerifyVerdict { code: VerifyCode.Ok, }; + } + return VerifyVerdict { code: VerifyCode.Mismatch, }; +} + +// The identity keys of the fixtures, one leading byte set - the +// original's k(seed) helper, entry by entry. +pub const KEY_01: [32]u8 = [32]u8{1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,}; +pub const KEY_02: [32]u8 = [32]u8{2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,}; +pub const KEY_10: [32]u8 = [32]u8{16, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,}; +pub const KEY_20: [32]u8 = [32]u8{32, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,}; +pub const KEY_30: [32]u8 = [32]u8{48, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,}; + +// The caller's hash orderings of the fixtures - the digests the +// canonical ordering selects between. +pub const DIGEST_AB: [30]u8 = [30]u8{1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30,}; +pub const DIGEST_BA: [30]u8 = [30]u8{30, 29, 28, 27, 26, 25, 24, 23, 22, 21, 20, 19, 18, 17, 16, 15, 14, 13, 12, 11, 10, 9, 8, 7, 6, 5, 4, 3, 2, 1,}; +pub const DIGEST_AC: [30]u8 = [30]u8{51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79, 80,}; + +// The caller's re-hash of the display fixture: the bytes 0..31. +pub const REHASH_32: [32]u8 = [32]u8{0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31,}; + +// **SNV-01** - commutativity: either argument order selects the +// same digest, because the bytewise-smaller key hashes first. +test snv_01_commutative { + const ab = safety_number(KEY_01, KEY_02, DIGEST_AB, DIGEST_BA); + const ba = safety_number(KEY_02, KEY_01, DIGEST_BA, DIGEST_AB); + const equal = verify(ab, ba); + assert(equal.code == VerifyCode.Ok); +} + +// **SNV-02** - determinism and display: identical inputs render +// identically; the display carries twelve groups, each a +// five-digit value under a hundred thousand. +test snv_02_deterministic_display { + const g1 = render(REHASH_32); + const g2 = render(REHASH_32); + var same: bool = true; + for i in 0..12 { + if (g1[i] != g2[i]) { + same = false; + } + } + assert(same); + assert(g1[0] == 72865); + assert(g1[1] == 38915); + assert(g1[2] == 4965); + assert(g1[3] == 71015); + assert(g1[4] == 37065); + assert(g1[5] == 3115); + assert(g1[6] == 69165); + assert(g1[7] == 35215); + assert(g1[8] == 76977); + assert(g1[9] == 43027); + assert(g1[10] == 9077); + assert(g1[11] == 75127); + var bounded: bool = true; + for i in 0..12 { + if (g1[i] >= SN_GROUP_MOD) { + bounded = false; + } + } + assert(bounded); +} + +// **SNV-04** - verify accepts the swapped-order digest: both +// parties computed the same safety number off either side. +test snv_04_verify_accepts_match { + const local = safety_number(KEY_10, KEY_20, DIGEST_AB, DIGEST_BA); + const remote = safety_number(KEY_20, KEY_10, DIGEST_BA, DIGEST_AB); + const v = verify(local, remote); + assert(v.code == VerifyCode.Ok); +} + +// **SNV-05** - verify rejects a mismatched digest: the caller's +// hashes for a swapped key differ, and the compare answers +// Mismatch - the application must refuse plaintext until the +// human re-confirms out of band. +test snv_05_verify_rejects_mismatch { + const local = safety_number(KEY_10, KEY_20, DIGEST_AB, DIGEST_BA); + const remote = safety_number(KEY_10, KEY_30, DIGEST_AC, DIGEST_BA); + const v = verify(local, remote); + assert(v.code == VerifyCode.Mismatch); +} + +// The helper has direct tests (coverage: Untested 0). +test key_lte_answers { + assert(key_lte(KEY_01, KEY_02)); + assert(!key_lte(KEY_02, KEY_01)); + assert(key_lte(KEY_01, KEY_01)); + assert(!key_lte(KEY_20, KEY_10)); + assert(key_lte(KEY_10, KEY_20)); +} + +// The ordering boundary: equal keys select the first ordering +// both ways, and a differing deep byte decides the order. +test ordering_boundary_answers { + const both = safety_number(KEY_01, KEY_01, DIGEST_AB, DIGEST_BA); + const mirror = safety_number(KEY_01, KEY_01, DIGEST_BA, DIGEST_AB); + const v = verify(both, mirror); + assert(v.code == VerifyCode.Mismatch); + + var deep_a: [32]u8; + var deep_b: [32]u8; + for i in 0..32 { + deep_a[i] = 0; + deep_b[i] = 0; + } + deep_a[31] = 5; + deep_b[31] = 3; + assert(key_lte(deep_b, deep_a)); + assert(!key_lte(deep_a, deep_b)); +}