code wiki / (root) / nx_tls13_transcript_snapkat_tamper_test.nx

nx_tls13_transcript_snapkat_tamper_test.nx source

↩ module page · 85 lines · 2613 B

1// nx_tls13_transcript_snapkat_tamper_test.nx -- NEGATIVE CONTROL for the 2// X-TLS-SNAPKAT-001 anti-regression KAT. Proves the KAT DISCRIMINATES: 3// under the OLD shallow-copy snapshot (the pre-BL-015 bug), continue-after- 4// snapshot DIVERGES from the one-shot at the lethal idx in {57..63}. 5// 6// This file deliberately reintroduces the bug LOCALLY (shallow_snapshot: 7// flat 256-byte ctx copy that duplicates bufptr's pointer VALUE -> the clone 8// shares the live partial block; sha256_final clobbers it). It does NOT 9// touch the production organ. It asserts the bug is REPRODUCED (both lethal 10// cases diverge), so the real KAT's "must equal one-shot" assertion would 11// have gone RED. Pair it with nx_tls13_transcript_snapkat_test (GREEN on the 12// fixed organ) for pos+NEG discrimination. 13// 14// expect_exit: 0 // 0 == both lethal cases diverged == gate discriminates 15// license_tier: ORIGINAL 16 17import "nx_syscalls.nx" 18import "nx_sha256.nx" 19 20func tnew() -> *u8 { 21 let r: *u8 = sys_mmap(256) 22 sha256_init(r as *Sha256) 23 return r 24} 25 26func tupdate(st: *u8, msg: *u8, n: i64) -> i64 { 27 sha256_update(st as *Sha256, msg, n) 28 return 0 29} 30 31// BUGGY snapshot: flat byte-copy of the ctx, sharing bufptr (no deep copy). 32func shallow_snapshot(st: *u8, out: *u8) -> i64 { 33 let clone: *u8 = sys_mmap(256) 34 var i: i64 = 0 35 while i < 256 { 36 clone[i] = st[i] 37 i = i + 1 38 } 39 sha256_final(clone as *Sha256, out) 40 return 0 41} 42 43func tfill(buf: *u8, n: i64) -> i64 { 44 var i: i64 = 0 45 while i < n { 46 buf[i] = (i * 7 + 3) & 0xff 47 i = i + 1 48 } 49 return 0 50} 51 52// Returns 1 if continue-after-shallow-snapshot DIVERGES from the one-shot 53// (i.e., the bug corrupted the live transcript), 0 if it matched. 54func diverges(s: i64, extra: i64) -> i64 { 55 let total: i64 = s + extra 56 let buf: *u8 = sys_mmap(total + 64) 57 tfill(buf, total) 58 59 let st: *u8 = tnew() 60 tupdate(st, buf, s) 61 let snap: *u8 = sys_mmap(64) 62 shallow_snapshot(st, snap) 63 64 let tail: *u8 = ((buf as i64) + s) as *u8 65 tupdate(st, tail, extra) 66 let cont: *u8 = sys_mmap(64) 67 shallow_snapshot(st, cont) 68 69 let ref_cont: *u8 = sys_mmap(64) 70 sha256_digest(buf, total, ref_cont) 71 72 var i: i64 = 0 73 while i < 32 { 74 if (cont[i] & 0xff) != (ref_cont[i] & 0xff) { return 1 } 75 i = i + 1 76 } 77 return 0 78} 79 80func main() -> i64 { 81 // Lethal idx in {57..63}: shallow-copy MUST corrupt the continuation. 82 if diverges(57, 80) != 1 { return 57 } // bug failed to reproduce -> control invalid 83 if diverges(63, 80) != 1 { return 63 } 84 return 0 85}