diff --git a/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-04::src::padding_class_oracle.json b/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-04::src::padding_class_oracle.json new file mode 100644 index 0000000000..562ad45f2d --- /dev/null +++ b/.trinity/seals/src_port::trios::crates::trios-chat::rings::CR-CHAT-04::src::padding_class_oracle.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:cc9413a13eeaf04dcddd6f855aa01b1663aa62ac0e54bd1b65d804234d89a788", + "gen_hash_rust": "sha256:dd7a7bfdca6601de0e95917ea5b8078bab805f272a563bb12d0c77c58cd2eb7c", + "gen_hash_verilog": "sha256:299e43e643b8aec8ccc0bb3a7b67126fb358d59b83bff7a5e347085e40c70108", + "gen_hash_zig": "sha256:f8d332d8935bf810ab1749133540bf35335a6923c3de5a32e9a9a44c68247fda", + "module": "port::trios::crates::trios-chat::rings::CR-CHAT-04::src::padding_class_oracle", + "ring": 12, + "seal_schema": 2, + "sealed_at": "2026-10-15T22:30:24Z", + "sealed_by": "t27c-bootstrap@0.5.2", + "spec_hash": "sha256:c509382357add2b258c35348556e52b621c0bf735e546d17531eec4dbbde7b3e", + "spec_path": "specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_class_oracle.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/docs/reports/t27b_expectations.json b/docs/reports/t27b_expectations.json index 3483595ccc..4805dd6bac 100644 --- a/docs/reports/t27b_expectations.json +++ b/docs/reports/t27b_expectations.json @@ -859,6 +859,7 @@ {"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/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_class_oracle.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/padding_class_oracle.t27 b/specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_class_oracle.t27 new file mode 100644 index 0000000000..5165dcd4a0 --- /dev/null +++ b/specs/port/trios/crates/trios-chat/rings/CR-CHAT-04/src/padding_class_oracle.t27 @@ -0,0 +1,313 @@ +module port::trios::crates::trios-chat::rings::CR-CHAT-04::src::padding_class_oracle; + +// Port of gHashTag/trios crates/trios-chat/rings/CR-CHAT-04/src/padding_class_oracle.rs +// (CR-CHAT-04 - padding-class oracle guard, Wave-18 Lane A, +// L-CHAT-6-cls, requirement R-CHAT-6). +// +// The padding scheme buckets every payload into one of four canonical +// classes, and the oracle guard holds the line inside one class: the +// encoder must pick exactly the smallest fitting class (an over-pad is +// a covert channel, an under-pad a truncation), the receiver must +// reject every malformed envelope before it inspects any plaintext +// byte - a truncated envelope, a non-class size, a declared length +// beyond the buffer, and a polluted padding tail. +// +// The original returns Result<(), PaddingOracleError> (and its +// crate-wide Error for the encoder-side paths). This port carries the +// verdict as a named struct (owner decision D5): Ok first, then the +// six error variants in the original's declaration order - +// NonClassSize, TruncatedTooShort, DeclaredLengthOverflow, +// ClassUpgrade, ClassDowngrade, NonZeroPaddingSuffix. No variant +// carries a payload, so the verdict is the code alone. +// +// The original's pad_class/unpad round trips are ported as the same +// layout arithmetic over a fixed envelope the caller fills: the length +// prefix is four big-endian bytes, the payload follows, the tail reads +// zero. The original's Error string matching in CLS-05/06 becomes +// direct code asserts - the strings are formatting plumbing and are +// not ported. The green_summary test of the original is a tautology +// (counting its own constant) and is not transcribed; every real +// invariant it waved at is transcribed below. + +// The four canonical padding classes, ascending. +pub const ORACLE_CLASSES: [4]usize = [4]usize{256, 1024, 4096, 16384}; + +// The length-prefix size. +pub const ORACLE_PREFIX: usize = 4; + +// Maximum payload size: the largest class minus the prefix. +pub const ORACLE_MAX_PAYLOAD: usize = 16384 - 4; + +// Verdict codes: Ok(()) and PaddingOracleError's variants, in declaration order. +pub enum PaddingOracleCode { + Ok, + NonClassSize, + TruncatedTooShort, + DeclaredLengthOverflow, + ClassUpgrade, + ClassDowngrade, + NonZeroPaddingSuffix, +} + +// The verdict of the oracle guard. No variant of the original's error +// carries a payload, so the code is the whole verdict. +pub struct PaddingOracleVerdict { + code: PaddingOracleCode, +} + +// The smallest class that fits payload_len bytes plus the four-byte +// length prefix - the original's const ladder, verbatim. +pub fn smallest_class(payload_len: usize) -> usize { + const needed: usize = ORACLE_PREFIX + payload_len; + if (needed <= ORACLE_CLASSES[0]) { + return ORACLE_CLASSES[0]; + } + if (needed <= ORACLE_CLASSES[1]) { + return ORACLE_CLASSES[1]; + } + if (needed <= ORACLE_CLASSES[2]) { + return ORACLE_CLASSES[2]; + } + return ORACLE_CLASSES[3]; +} + +// Whether the length is one of the four canonical classes - the +// original's CLASSES.contains, answered by a scan. +pub fn is_class(len: usize) -> bool { + for c in ORACLE_CLASSES { + if (c == len) { + return true; + } + } + return false; +} + +// [VERIFIED] Accept-or-reject: is chosen_class exactly the smallest +// class that fits payload_len? An over-pad is a covert channel, an +// under-pad a truncation; both are distinguishing oracles. Checked in +// the original's order: the payload ceiling, then the class ladder. +pub fn check_class_choice(payload_len: usize, chosen_class: usize) -> PaddingOracleVerdict { + if (payload_len > ORACLE_MAX_PAYLOAD) { + return PaddingOracleVerdict { code: PaddingOracleCode.DeclaredLengthOverflow, }; + } + const smallest: usize = smallest_class(payload_len); + if (chosen_class < smallest) { + return PaddingOracleVerdict { code: PaddingOracleCode.ClassDowngrade, }; + } + if (chosen_class > smallest) { + return PaddingOracleVerdict { code: PaddingOracleCode.ClassUpgrade, }; + } + return PaddingOracleVerdict { code: PaddingOracleCode.Ok, }; +} + +// [VERIFIED] The strict guard over an inbound envelope of a canonical +// class size: rejects before any plaintext byte is observed, checked in +// the original's order - the truncation floor, the class membership, +// the declared-length ceiling, and the zero tail. The envelope is a +// fixed 256-byte record: declared is its four big-endian prefix bytes, +// payload is the tail after the prefix; the non-zero probe reads the +// bytes past the declared payload. +pub fn validate_envelope_256(env: [256]u8) -> PaddingOracleVerdict { + // a 256-byte envelope is never truncated and always a class; + // those two rules are exercised by the length-level tests below + var prefix: [4]u8 = [4]u8{0, 0, 0, 0,}; + for i in 0..4 { + prefix[i] = env[i]; + } + const declared: usize = ORACLE_BE_PREFIX(prefix); + if (ORACLE_PREFIX + declared > 256) { + return PaddingOracleVerdict { code: PaddingOracleCode.DeclaredLengthOverflow, }; + } + for i in 0..256 { + if (i >= ORACLE_PREFIX + declared) { + if (env[i] != 0) { + return PaddingOracleVerdict { code: PaddingOracleCode.NonZeroPaddingSuffix, }; + } + } + } + return PaddingOracleVerdict { code: PaddingOracleCode.Ok, }; +} + +// The strict guard over an envelope of any length: the truncation and +// class rules first, then the same interior checks the 256-byte form +// runs, over the prefix bytes the caller hands in and the tail probe +// as a bit the caller computed (a true tail probe needs the whole +// buffer; the bit carries it). +pub fn validate_envelope(len: usize, prefix: [4]u8, tail_clean: bool) -> PaddingOracleVerdict { + if (len < ORACLE_PREFIX) { + return PaddingOracleVerdict { code: PaddingOracleCode.TruncatedTooShort, }; + } + if (!is_class(len)) { + return PaddingOracleVerdict { code: PaddingOracleCode.NonClassSize, }; + } + const declared: usize = ORACLE_BE_PREFIX(prefix); + if (ORACLE_PREFIX + declared > len) { + return PaddingOracleVerdict { code: PaddingOracleCode.DeclaredLengthOverflow, }; + } + if (!tail_clean) { + return PaddingOracleVerdict { code: PaddingOracleCode.NonZeroPaddingSuffix, }; + } + return PaddingOracleVerdict { code: PaddingOracleCode.Ok, }; +} + +// The declared length a four-byte big-endian prefix carries. +pub fn ORACLE_BE_PREFIX(prefix: [4]u8) -> usize { + const b0: usize = @as(usize, prefix[0]); + const b1: usize = @as(usize, prefix[1]); + const b2: usize = @as(usize, prefix[2]); + const b3: usize = @as(usize, prefix[3]); + return ((b0 * 256 + b1) * 256 + b2) * 256 + b3; +} + +// **CLS-01** - a well-formed envelope accepts: the smallest class of a +// 25-byte payload is 256, the declared prefix is 25, and the zeroed +// tail is clean. +test cls_01_well_formed_envelope_accepts { + const v1 = check_class_choice(25, 256); + assert(v1.code == PaddingOracleCode.Ok); + + var env: [256]u8; + for i in 0..256 { + env[i] = 0; + } + env[3] = 25; + const v2 = validate_envelope_256(env); + assert(v2.code == PaddingOracleCode.Ok); + + var prefix: [4]u8 = [4]u8{0, 0, 0, 25,}; + const v3 = validate_envelope(256, prefix, true); + assert(v3.code == PaddingOracleCode.Ok); +} + +// **CLS-02** - non-class size rejected before any payload byte is +// inspected: 300 is not one of the four classes. +test cls_02_non_class_size_rejected { + var prefix: [4]u8 = [4]u8{0, 0, 0, 0,}; + const v = validate_envelope(300, prefix, true); + assert(v.code == PaddingOracleCode.NonClassSize); +} + +// **CLS-03** - truncated envelope (2 bytes) rejected as +// TruncatedTooShort, not NonClassSize - the two arms must not collide. +test cls_03_truncated_too_short_rejected { + var prefix: [4]u8 = [4]u8{0, 0, 0, 0,}; + const v = validate_envelope(2, prefix, true); + assert(v.code == PaddingOracleCode.TruncatedTooShort); +} + +// **CLS-04** - declared length overflow rejected: the prefix declares +// 1000, which exceeds a 256-byte class buffer by far. +test cls_04_declared_length_overflow_rejected { + var env: [256]u8; + for i in 0..256 { + env[i] = 0; + } + env[0] = 0; + env[1] = 0; + env[2] = 3; + env[3] = 232; + const v = validate_envelope_256(env); + assert(v.code == PaddingOracleCode.DeclaredLengthOverflow); + + var prefix: [4]u8 = [4]u8{0, 0, 3, 232,}; + const v2 = validate_envelope(256, prefix, true); + assert(v2.code == PaddingOracleCode.DeclaredLengthOverflow); +} + +// **CLS-05** - class downgrade rejected: 252 bytes fit class 256 and +// 128 is below it; 1020 bytes fit class 1024 and 256 is below it. +test cls_05_class_downgrade_rejected { + const v1 = check_class_choice(252, 128); + assert(v1.code == PaddingOracleCode.ClassDowngrade); + const v2 = check_class_choice(1020, 256); + assert(v2.code == PaddingOracleCode.ClassDowngrade); +} + +// **CLS-06** - class upgrade rejected - the covert-channel attack: 100 +// bytes fit class 256 and 4096 over-pads; 500 bytes fit class 1024 +// and 16384 over-pads; the legitimate choices accept. +test cls_06_class_upgrade_rejected { + const v1 = check_class_choice(100, 4096); + assert(v1.code == PaddingOracleCode.ClassUpgrade); + const v2 = check_class_choice(500, 16384); + assert(v2.code == PaddingOracleCode.ClassUpgrade); + const v3 = check_class_choice(100, 256); + assert(v3.code == PaddingOracleCode.Ok); + const v4 = check_class_choice(500, 1024); + assert(v4.code == PaddingOracleCode.Ok); +} + +// **CLS bonus** - a polluted padding tail rejected: the prefix declares +// 5, five payload bytes follow, and byte 200 of the tail is non-zero. +test cls_bonus_non_zero_suffix_rejected { + var env: [256]u8; + for i in 0..256 { + env[i] = 0; + } + env[3] = 5; + env[4] = 'h'; + env[5] = 'e'; + env[6] = 'l'; + env[7] = 'l'; + env[8] = 'o'; + env[200] = 66; + const v = validate_envelope_256(env); + assert(v.code == PaddingOracleCode.NonZeroPaddingSuffix); +} + +// **CLS bonus** - an oversize payload rejected up front: MAX_PAYLOAD+1 +// is above the ceiling before any allocation. +test cls_bonus_oversize_payload_rejected { + const v = check_class_choice(ORACLE_MAX_PAYLOAD + 1, 16384); + assert(v.code == PaddingOracleCode.DeclaredLengthOverflow); +} + +// **CLS bonus** - smallest_class answers the ladder at every boundary: +// the four classes and the exact fit edges around them. +test cls_bonus_smallest_class_ladder { + assert(smallest_class(0) == 256); + assert(smallest_class(1) == 256); + assert(smallest_class(100) == 256); + assert(smallest_class(252) == 256); + assert(smallest_class(253) == 1024); + assert(smallest_class(1020) == 1024); + assert(smallest_class(1021) == 4096); + assert(smallest_class(4092) == 4096); + assert(smallest_class(4093) == 16384); + assert(smallest_class(ORACLE_MAX_PAYLOAD) == 16384); +} + +// The three helpers have direct tests (coverage: Untested 0). +test is_class_answers { + assert(is_class(256)); + assert(is_class(1024)); + assert(is_class(4096)); + assert(is_class(16384)); + assert(!is_class(300)); + assert(!is_class(0)); +} + +test oracle_be_prefix_answers { + assert(ORACLE_BE_PREFIX([4]u8{0, 0, 0, 25,}) == 25); + assert(ORACLE_BE_PREFIX([4]u8{0, 0, 3, 232,}) == 1000); + assert(ORACLE_BE_PREFIX([4]u8{0, 0, 0, 0,}) == 0); +} + +// Rule order is the original's: the truncation floor before the class +// membership, the class membership before the declared-length ceiling, +// the payload ceiling before the class ladder, and the downgrade before +// the upgrade. +test rule_order_matches_original { + var prefix: [4]u8 = [4]u8{0, 0, 3, 232,}; + const v1 = validate_envelope(2, prefix, false); + assert(v1.code == PaddingOracleCode.TruncatedTooShort); + const v2 = validate_envelope(300, prefix, false); + assert(v2.code == PaddingOracleCode.NonClassSize); + const v3 = validate_envelope(256, prefix, false); + assert(v3.code == PaddingOracleCode.DeclaredLengthOverflow); + + const v4 = check_class_choice(ORACLE_MAX_PAYLOAD + 1, 128); + assert(v4.code == PaddingOracleCode.DeclaredLengthOverflow); + const v5 = check_class_choice(252, 4096); + assert(v5.code == PaddingOracleCode.ClassUpgrade); +}