code wiki / _hdl_build / nx_recycler_bounds_gate.nx
`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"
8
9func gp(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 }
10func have_file(p: *u8) -> i64 { let fd: i64=sys_openat_rd(p); if fd<0 { return 0 } sys_close(fd); return 1 }
11
12func main() -> i64 {
13    gp("=== nx_recycler_bounds_gate: Heartbleed (CVE-2014-0160) recycled into a bounds primitive ===\n" as *u8)
14    var pass: i64=0; var fail: i64=0
15
16    // a 10-byte received record, with a poisoned tail so an over-read would be visible
17    let src: *u8 = sys_mmap(65536)
18    var i: i64=0; while i<10 { src[i]=(65+i) as u8; i=i+1 }            // "ABCDEFGHIJ"
19    while i<65536 { src[i]=0x7e as u8; i=i+1 }                          // adjacent "secret" memory (~)
20    let dst: *u8 = sys_mmap(65536)
21
22    // KAT1 THE HEARTBLEED ATTACK: claim 10000 against 10 available -> must move only 10 (no over-read)
23    let n1: i64 = rb_bounded_copy(dst, 65536, src, 10, 10000)
24    if n1 == 10 { pass=pass+1 } else { fail=fail+1; gp("  FAIL kat1-overread n=" as *u8); gn(n1); gp("\n" as *u8) }
25    // and the copied bytes are exactly the 10 real ones, no leaked 0x7e
26    var leaked: i64=0; var j: i64=0; while j<n1 { if dst[j]!=src[j]{leaked=1} j=j+1 }
27    if leaked==0 { pass=pass+1 } else { fail=fail+1; gp("  FAIL kat1-garbage-copied\n" as *u8) }
28    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 }
29    // the detector flags the over-claim
30    if rb_is_overclaim(10, 10000)==1 { pass=pass+1 } else { fail=fail+1; gp("  FAIL kat1-detector-missed\n" as *u8) }
31
32    // KAT2 honest claim within bounds -> moves exactly the claimed amount
33    let n2: i64 = rb_bounded_copy(dst, 65536, src, 10, 5)
34    if n2 == 5 { pass=pass+1 } else { fail=fail+1; gp("  FAIL kat2 n=" as *u8); gn(n2); gp("\n" as *u8) }
35    if rb_is_overclaim(10, 5)==0 { pass=pass+1 } else { fail=fail+1; gp("  FAIL kat2-false-overclaim\n" as *u8) }
36
37    // KAT3 destination capacity clamp -> never writes past dstcap
38    let n3: i64 = rb_bounded_copy(dst, 16, src, 100, 100)
39    if n3 == 16 { pass=pass+1 } else { fail=fail+1; gp("  FAIL kat3-cap n=" as *u8); gn(n3); gp("\n" as *u8) }
40
41    // KAT4 grounding: the recycled bug really exists on disk as a fetched artifact (not asserted from thin air)
42    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) }
43
44    gp("RECYCLER-BOUNDS-GATE pass=" as *u8); gn(pass); gp(" fail=" as *u8); gn(fail)
45    if fail==0 { gp(" verdict=GREEN (Heartbleed-style over-claim 10000-vs-10 -> 10 moved, 0 over-read; recycled from a real fetched artifact)\n" as *u8); sys_exit(0); return 0 }
46    gp(" verdict=RED\n" as *u8); sys_exit(1); return 1
47}
nx_recycler_bounds_gate.nx source

`nx_recycler_bounds_gate.nx` source
