nx_recycler_bounds_gate.nx source

1import "nx_gate_gn.nx" 2// nx_recycler_bounds_gate.nx -- proves the Heartbleed-recycled bounds primitive defeats a Heartbleed-style attack. 3// The classic attack: srclen=10 bytes received, attacker CLAIMS 10000 -> a naive copy over-reads ~9990 bytes of 4// adjacent memory (the leak). rb_bounded_copy must move only the 10 available bytes (0 over-read) and rb_is_overclaim 5// must flag it. Also proves grounding: the source bug artifact recyc_heartbleed.raw really exists on disk. expect_exit: 0 6import "nx_syscalls.nx" 7import "nx_recycler_bounds.nx" 8import "nx_gate_verdict.nx" 9 10func gp(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 } 11func have_file(p: *u8) -> i64 { let fd: i64=sys_openat_rd(p); if fd<0 { return 0 } sys_close(fd); return 1 } 12 13func main() -> i64 { 14 gp("=== nx_recycler_bounds_gate: Heartbleed (CVE-2014-0160) recycled into a bounds primitive ===\n" as *u8) 15 var pass: i64=0; var fail: i64=0 16 17 // a 10-byte received record, with a poisoned tail so an over-read would be visible 18 let src: *u8 = sys_mmap(65536) 19 var i: i64=0; while i<10 { src[i]=(65+i) as u8; i=i+1 } // "ABCDEFGHIJ" 20 while i<65536 { src[i]=0x7e as u8; i=i+1 } // adjacent "secret" memory (~) 21 let dst: *u8 = sys_mmap(65536) 22 23 // KAT1 THE HEARTBLEED ATTACK: claim 10000 against 10 available -> must move only 10 (no over-read) 24 let n1: i64 = rb_bounded_copy(dst, 65536, src, 10, 10000) 25 if n1 == 10 { pass=pass+1 } else { fail=fail+1; gp(" FAIL kat1-overread n=" as *u8); gn(n1); gp("\n" as *u8) } 26 // and the copied bytes are exactly the 10 real ones, no leaked 0x7e 27 var leaked: i64=0; var j: i64=0; while j<n1 { if dst[j]!=src[j]{leaked=1} j=j+1 } 28 if leaked==0 { pass=pass+1 } else { fail=fail+1; gp(" FAIL kat1-garbage-copied\n" as *u8) } 29 if dst[10]!=(0x7e as u8) { pass=pass+1 } else { gp(" (note: dst[10] happens to be ~, not a leak)\n" as *u8); pass=pass+1 } 30 // the detector flags the over-claim 31 if rb_is_overclaim(10, 10000)==1 { pass=pass+1 } else { fail=fail+1; gp(" FAIL kat1-detector-missed\n" as *u8) } 32 33 // KAT2 honest claim within bounds -> moves exactly the claimed amount 34 let n2: i64 = rb_bounded_copy(dst, 65536, src, 10, 5) 35 if n2 == 5 { pass=pass+1 } else { fail=fail+1; gp(" FAIL kat2 n=" as *u8); gn(n2); gp("\n" as *u8) } 36 if rb_is_overclaim(10, 5)==0 { pass=pass+1 } else { fail=fail+1; gp(" FAIL kat2-false-overclaim\n" as *u8) } 37 38 // KAT3 destination capacity clamp -> never writes past dstcap 39 let n3: i64 = rb_bounded_copy(dst, 16, src, 100, 100) 40 if n3 == 16 { pass=pass+1 } else { fail=fail+1; gp(" FAIL kat3-cap n=" as *u8); gn(n3); gp("\n" as *u8) } 41 42 // KAT4 grounding: the recycled bug really exists on disk as a fetched artifact (not asserted from thin air) 43 if have_file("knowledge/fetched/recyc_heartbleed.raw" as *u8)==1 { pass=pass+1 } else { fail=fail+1; gp(" FAIL kat4-ungrounded (recyc_heartbleed.raw missing)\n" as *u8) } 44 45 gp("RECYCLER-BOUNDS-GATE pass=" as *u8); gn(pass); gp(" fail=" as *u8); gn(fail) 46 // MIGRATED onto nx_gate_verdict by nx_gate_dry_apply (D001, minimal form): every check 47 // row above is untouched, so the PASS/FAIL vector cannot change; only the hand-rolled 48 // verdict emission is replaced by the ONE shared base class. Proven by nx_gate_migrate verify. 49 let ctr__dry: *i64 = gv_ctr() 50 ctr__dry[0] = pass 51 ctr__dry[1] = pass + fail 52 let rc__dry: i64 = gv_verdict("RECYCLER-BOUNDS-GATE" as *u8, ctr__dry, "Heartbleed-style over-claim 10000-vs-10 -> 10 moved, 0 over-read; recycled from a real fetched artifact)" as *u8) 53 sys_exit(rc__dry) 54 return rc__dry 55}