nx_fw_safeflash_gate.nx source

1// nx_fw_safeflash_gate.nx -- THE REFEREE for the never-brick firmware flash. 2// 3// Proves fw_safe_flash upholds the NEVER-BRICK invariant (active is BOOTABLE after every flash) 4// against deliberate failures, AND that each guard actually fires (no-fabricated-green): 5// 6// T1 good-flash : valid new image, clean write -> FW_OK + active bootable 7// N1 reject-bad : the SOURCE image is corrupt -> FW_REJECTED_PRE + active bootable (untouched) 8// N2 mid-corrupt : write injected with corruption -> FW_RECOVERED + active bootable (from golden) 9// N3 no-anchor : golden (recovery copy) is corrupt -> FW_REFUSED_NO_ANCHOR + active bootable (untouched) 10// N4 host-path : active path is NOT under /tmp/ -> FW_SANDBOX_VIOLATION (cannot touch host) 11// INV never-brick : active is BOOTABLE after T1,N1,N2,N3 (the headline guarantee) 12// 13// GREEN only if all six hold. Evidence -> knowledge/status/fw_safeflash_gate.log. 14// Sovereign: imports the organ + nx_framed_append + nx_syscalls (no gcc). license_tier: ORIGINAL 15import "nx_fw_safeflash.nx" 16import "nx_framed_append.nx" 17import "nx_syscalls.nx" 18 19const FWSF_LOG: *u8 = "knowledge/status/fw_safeflash_gate.log" 20const FWSF_GOOD: *u8 = "GOLDEN-ANCHOR-firmware-v1-immutable-recovery-copy" 21const FWSF_NEW: *u8 = "NEW-firmware-v2-candidate-image-being-flashed-in" 22 23func et_len(s: *u8) -> i64 { var i: i64 = 0; while s[i] != 0 as u8 { i = i + 1 } return i } 24 25func et_row(name: *u8, pass: i64) -> i64 { 26 let buf: *u8 = sys_mmap(528) 27 var o: i64 = 0 28 o = fw_cat(buf, o, "FWSF row=\x00" as *u8) 29 o = fw_cat(buf, o, name) 30 if pass == 1 { o = fw_cat(buf, o, " verdict=PASS\x00" as *u8) } else { o = fw_cat(buf, o, " verdict=FAIL\x00" as *u8) } 31 buf[o] = 0 as u8 32 fa_appendz(FWSF_LOG, buf, 512) 33 fw_puts(" "); fw_puts(name) 34 if pass == 1 { fw_puts(" PASS\n") } else { fw_puts(" FAIL\n") } 35 return 0 36} 37 38func main() -> i64 { 39 let epoch: i64 = sys_now_realtime_sec() 40 let pid: i64 = __syscall(39, 0, 0, 0, 0, 0, 0) 41 let gl: i64 = et_len(FWSF_GOOD) 42 let nl: i64 = et_len(FWSF_NEW) 43 44 let g: *u8 = sys_mmap(256); let a: *u8 = sys_mmap(256); let nw: *u8 = sys_mmap(256) 45 46 // ---- T1 good-flash ---- 47 fw_path(g, "/tmp/fwsf_t1g." as *u8, epoch, pid); fw_path(a, "/tmp/fwsf_t1a." as *u8, epoch, pid); fw_path(nw, "/tmp/fwsf_t1n." as *u8, epoch, pid) 48 fw_make(g, FWSF_GOOD, gl); fw_make(a, FWSF_GOOD, gl); fw_make(nw, FWSF_NEW, nl) 49 let s1: i64 = fw_safe_flash(a, g, nw, 0) 50 let b1: i64 = fw_bootable(a) 51 var t1: i64 = 0; if s1 == FW_OK { if b1 == 1 { t1 = 1 } } 52 53 // ---- N1 reject-bad-source ---- 54 fw_path(g, "/tmp/fwsf_n1g." as *u8, epoch, pid); fw_path(a, "/tmp/fwsf_n1a." as *u8, epoch, pid); fw_path(nw, "/tmp/fwsf_n1n." as *u8, epoch, pid) 55 fw_make(g, FWSF_GOOD, gl); fw_make(a, FWSF_GOOD, gl); fw_make(nw, FWSF_NEW, nl) 56 fw_corrupt_byte(nw) // the image we are asked to flash is bad 57 let s2: i64 = fw_safe_flash(a, g, nw, 0) 58 let b2: i64 = fw_bootable(a) 59 var n1: i64 = 0; if s2 == FW_REJECTED_PRE { if b2 == 1 { n1 = 1 } } 60 61 // ---- N2 mid-flash-corruption-recovered ---- 62 fw_path(g, "/tmp/fwsf_n2g." as *u8, epoch, pid); fw_path(a, "/tmp/fwsf_n2a." as *u8, epoch, pid); fw_path(nw, "/tmp/fwsf_n2n." as *u8, epoch, pid) 63 fw_make(g, FWSF_GOOD, gl); fw_make(a, FWSF_GOOD, gl); fw_make(nw, FWSF_NEW, nl) 64 let s3: i64 = fw_safe_flash(a, g, nw, 1) // inject corruption during the write 65 let b3: i64 = fw_bootable(a) 66 var n2: i64 = 0; if s3 == FW_RECOVERED { if b3 == 1 { n2 = 1 } } 67 68 // ---- N3 no-recovery-anchor (golden corrupt) ---- 69 fw_path(g, "/tmp/fwsf_n3g." as *u8, epoch, pid); fw_path(a, "/tmp/fwsf_n3a." as *u8, epoch, pid); fw_path(nw, "/tmp/fwsf_n3n." as *u8, epoch, pid) 70 fw_make(g, FWSF_GOOD, gl); fw_make(a, FWSF_GOOD, gl); fw_make(nw, FWSF_NEW, nl) 71 fw_corrupt_byte(g) // the recovery anchor is gone 72 let s4: i64 = fw_safe_flash(a, g, nw, 0) 73 let b4: i64 = fw_bootable(a) 74 var n3: i64 = 0; if s4 == FW_REFUSED_NO_ANCHOR { if b4 == 1 { n3 = 1 } } 75 76 // ---- N4 host-path refused (sandbox guard) ---- 77 let ahost: *u8 = sys_mmap(256); fw_path(ahost, "knowledge/fwsf_n4_HOST." as *u8, epoch, pid) 78 fw_path(g, "/tmp/fwsf_n4g." as *u8, epoch, pid); fw_path(nw, "/tmp/fwsf_n4n." as *u8, epoch, pid) 79 fw_make(g, FWSF_GOOD, gl); fw_make(nw, FWSF_NEW, nl) 80 let s5: i64 = fw_safe_flash(ahost, g, nw, 0) 81 var n4: i64 = 0; if s5 == FW_SANDBOX_VIOLATION { n4 = 1 } 82 83 // ---- INVARIANT: active bootable after every (sandboxed) scenario ---- 84 var inv: i64 = 0 85 if b1 == 1 { if b2 == 1 { if b3 == 1 { if b4 == 1 { inv = 1 } } } } 86 87 var passes: i64 = 0 88 if t1 == 1 { passes = passes + 1 } 89 if n1 == 1 { passes = passes + 1 } 90 if n2 == 1 { passes = passes + 1 } 91 if n3 == 1 { passes = passes + 1 } 92 if n4 == 1 { passes = passes + 1 } 93 if inv == 1 { passes = passes + 1 } 94 var green: i64 = 0 95 if passes == 6 { green = 1 } 96 97 fw_puts("fw-safeflash gate (never-brick invariant + 5 adversarial flashes)\n") 98 et_row("T1-good-flash-ok \x00" as *u8, t1) 99 et_row("N1-bad-source-rejected \x00" as *u8, n1) 100 et_row("N2-midflash-recovered \x00" as *u8, n2) 101 et_row("N3-no-anchor-refused \x00" as *u8, n3) 102 et_row("N4-host-path-refused \x00" as *u8, n4) 103 et_row("INV-active-never-bricked\x00" as *u8, inv) 104 105 let vb: *u8 = sys_mmap(528) 106 var o: i64 = 0 107 o = fw_cat(vb, o, "FW-SAFEFLASH verdict=\x00" as *u8) 108 if green == 1 { o = fw_cat(vb, o, "GREEN\x00" as *u8) } else { o = fw_cat(vb, o, "RED\x00" as *u8) } 109 o = fw_cat(vb, o, " passes=\x00" as *u8); o = fw_catn(vb, o, passes); o = fw_cat(vb, o, "/6 END\x00" as *u8) 110 vb[o] = 0 as u8 111 fa_appendz(FWSF_LOG, vb, 512) 112 fw_puts(vb as *u8); fw_puts("\n") 113 114 if green == 1 { return 0 } 115 return 1 116}