nx_cmos_gate.nx source

1// nx_cmos_gate.nx -- proves the never-brick CMOS config-tweak model. 2// 3// T0 golden-valid : a known-good CMOS image has a consistent checksum 4// T1 safe-tweak-valid : a guarded config tweak keeps the checksum valid + changes the byte 5// N1 raw-corrupt-detected : a raw byte flip (no checksum fix) -> cmos_valid == 0 (BIOS would reject) 6// N2 restore-recovers : restoring the golden snapshot makes it valid again 7// N3 refuse-checksum-byte : cmos_set_safe REFUSES to write the checksum bytes (0x2E/0x2F) 8// N4 refuse-rtc-byte : cmos_set_safe REFUSES to write the RTC/clock/status bytes (<0x10) 9// 10// GREEN only if all six hold. Evidence -> knowledge/status/cmos_gate.log. 11// Sovereign: imports nx_cmos + nx_framed_append + nx_syscalls (no gcc). license_tier: ORIGINAL 12import "nx_cmos.nx" 13import "nx_framed_append.nx" 14import "nx_syscalls.nx" 15 16const CG_LOG: *u8 = "knowledge/status/cmos_gate.log" 17 18func cg_cat(dst: *u8, off: i64, s: *u8) -> i64 { var i: i64 = 0; while s[i] != 0 as u8 { dst[off + i] = s[i]; i = i + 1 } return off + i } 19func cg_catn(dst: *u8, off: i64, v: i64) -> i64 { 20 var m: i64 = v; var o: i64 = off 21 if m < 0 { m = 0 - m } 22 let t: *u8 = sys_mmap(28); var k: i64 = 0 23 if m == 0 { t[0] = 48 as u8; k = 1 } 24 while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 } 25 var i: i64 = 0 26 while i < k { dst[o + i] = t[k - 1 - i]; i = i + 1 } 27 return o + k 28} 29func cg_row(name: *u8, pass: i64) -> i64 { 30 let buf: *u8 = sys_mmap(528) 31 var o: i64 = 0 32 o = cg_cat(buf, o, "CMOSG row=\x00" as *u8) 33 o = cg_cat(buf, o, name) 34 if pass == 1 { o = cg_cat(buf, o, " verdict=PASS\x00" as *u8) } else { o = cg_cat(buf, o, " verdict=FAIL\x00" as *u8) } 35 buf[o] = 0 as u8 36 fa_appendz(CG_LOG, buf, 512) 37 c_puts(" "); c_puts(name) 38 if pass == 1 { c_puts(" PASS\n") } else { c_puts(" FAIL\n") } 39 return 0 40} 41 42func main() -> i64 { 43 c_puts("cmos gate (never-brick config tweak: checksum + golden + range guards)\n") 44 let g: *u8 = sys_mmap(CMOS_SIZE + 16) 45 let w: *u8 = sys_mmap(CMOS_SIZE + 16) 46 cmos_golden(g) 47 48 // T0 golden valid 49 var t0: i64 = 0; if cmos_valid(g) == 1 { t0 = 1 } 50 51 // T1 safe tweak stays valid + byte changed 52 cmos_restore(w, g) 53 let r1: i64 = cmos_set_safe(w, 24, 0x77) 54 var t1: i64 = 0; if r1 == CMOS_OK { if cmos_valid(w) == 1 { if (w[24] as i64) == 0x77 { t1 = 1 } } } 55 56 // N1 raw corruption detected 57 cmos_restore(w, g) 58 cmos_corrupt_raw(w, 20) 59 var n1: i64 = 0; if cmos_valid(w) == 0 { n1 = 1 } 60 61 // N2 restore recovers 62 cmos_restore(w, g) 63 var n2: i64 = 0; if cmos_valid(w) == 1 { n2 = 1 } 64 65 // N3 refuse checksum byte 66 cmos_restore(w, g) 67 let r3: i64 = cmos_set_safe(w, 46, 0) 68 var n3: i64 = 0; if r3 == CMOS_REFUSED { if cmos_valid(w) == 1 { n3 = 1 } } 69 70 // N4 refuse RTC byte 71 cmos_restore(w, g) 72 let r4: i64 = cmos_set_safe(w, 5, 0) 73 var n4: i64 = 0; if r4 == CMOS_REFUSED { if cmos_valid(w) == 1 { n4 = 1 } } 74 75 var passes: i64 = 0 76 if t0 == 1 { passes = passes + 1 } 77 if t1 == 1 { passes = passes + 1 } 78 if n1 == 1 { passes = passes + 1 } 79 if n2 == 1 { passes = passes + 1 } 80 if n3 == 1 { passes = passes + 1 } 81 if n4 == 1 { passes = passes + 1 } 82 var green: i64 = 0 83 if passes == 6 { green = 1 } 84 85 cg_row("T0-golden-valid \x00" as *u8, t0) 86 cg_row("T1-safe-tweak-stays-valid\x00" as *u8, t1) 87 cg_row("N1-raw-corrupt-detected \x00" as *u8, n1) 88 cg_row("N2-restore-recovers \x00" as *u8, n2) 89 cg_row("N3-refuse-checksum-byte \x00" as *u8, n3) 90 cg_row("N4-refuse-rtc-byte \x00" as *u8, n4) 91 92 let vb: *u8 = sys_mmap(528) 93 var o: i64 = 0 94 o = cg_cat(vb, o, "CMOS verdict=\x00" as *u8) 95 if green == 1 { o = cg_cat(vb, o, "GREEN\x00" as *u8) } else { o = cg_cat(vb, o, "RED\x00" as *u8) } 96 o = cg_cat(vb, o, " passes=\x00" as *u8); o = cg_catn(vb, o, passes); o = cg_cat(vb, o, "/6 END\x00" as *u8) 97 vb[o] = 0 as u8 98 fa_appendz(CG_LOG, vb, 512) 99 c_puts(vb); c_puts("\n") 100 101 if green == 1 { return 0 } 102 return 1 103}