nx_fw_uefi_capsule_gate.nx source

1// nx_fw_uefi_capsule_gate.nx -- proves the real-EFI-header signed capsule. 2// 3// T1 authentic-verifies : a platform-signed UEFI capsule verifies 4// T2 valid-EFI-header : it is a well-formed EFI_CAPSULE_HEADER (Nishi GUID, HeaderSize==28, CapsuleImageSize==total) 5// N1 corrupted-rejected : flip a payload byte -> verify == 0 6// N2 forged-rejected : signed with a different key -> verify == 0 7// N3 wrong-GUID-rejected : corrupt the CapsuleGuid -> verify == 0 8// 9// GREEN only if all five hold. Evidence -> knowledge/status/fw_uefi_capsule_gate.log. 10// Sovereign: imports nx_fw_uefi_capsule (-> nx_fw_capsule -> nx_ed25519) + nx_framed_append + nx_syscalls. license_tier: ORIGINAL 11import "nx_fw_uefi_capsule.nx" 12import "nx_framed_append.nx" 13import "nx_syscalls.nx" 14 15const UCG_LOG: *u8 = "knowledge/status/fw_uefi_capsule_gate.log" 16const UCG_PAY: *u8 = "NISHI-fw-uefi-capsule-payload-image" 17 18func ucg_len(s: *u8) -> i64 { var i: i64 = 0; while s[i] != 0 as u8 { i = i + 1 } return i } 19func uc_copy(src: *u8, dst: *u8) -> i64 { 20 let lb: *i64 = sys_mmap(16) as *i64; lb[0] = 0 21 let b: *u8 = cp_read(src, lb) 22 if (b as i64) == 0 { return 0 - 1 } 23 cp_write(dst, b, lb[0]) 24 return 0 25} 26func ucg_row(name: *u8, pass: i64) -> i64 { 27 let buf: *u8 = sys_mmap(528) 28 var o: i64 = 0 29 o = cp_cat(buf, o, "UCAPG row=\x00" as *u8) 30 o = cp_cat(buf, o, name) 31 if pass == 1 { o = cp_cat(buf, o, " verdict=PASS\x00" as *u8) } else { o = cp_cat(buf, o, " verdict=FAIL\x00" as *u8) } 32 buf[o] = 0 as u8 33 fa_appendz(UCG_LOG, buf, 512) 34 cp_puts(" "); cp_puts(name) 35 if pass == 1 { cp_puts(" PASS\n") } else { cp_puts(" FAIL\n") } 36 return 0 37} 38 39func main() -> i64 { 40 cp_puts("fw-uefi-capsule gate (real EFI_CAPSULE_HEADER + ed25519)\n") 41 let e: i64 = sys_now_realtime_sec() 42 let p: i64 = __syscall(39, 0, 0, 0, 0, 0, 0) 43 let pl: i64 = ucg_len(UCG_PAY) 44 let plat: *u8 = sys_mmap(32); cap_plat_seed(plat) 45 let forged: *u8 = sys_mmap(32); var i: i64 = 0; while i < 32 { forged[i] = ((i * 3 + 99) & 0xff) as u8; i = i + 1 } 46 47 let authcap: *u8 = sys_mmap(256); cap_path(authcap, "/tmp/ucg_auth." as *u8, e, p); uc_make(authcap, UCG_PAY, pl, plat) 48 let forgcap: *u8 = sys_mmap(256); cap_path(forgcap, "/tmp/ucg_forg." as *u8, e, p); uc_make(forgcap, UCG_PAY, pl, forged) 49 50 // T1 authentic 51 var t1: i64 = 0; if uc_verify(authcap) == 1 { t1 = 1 } 52 53 // T2 real EFI_CAPSULE_HEADER 54 let lb: *i64 = sys_mmap(16) as *i64; lb[0] = 0 55 let b: *u8 = cp_read(authcap, lb) 56 var t2: i64 = 0 57 if (b as i64) != 0 { if uc_header_ok(b, lb[0]) == 1 { if cp_rd_u32(b, 16) == 28 { if cp_rd_u32(b, 24) == lb[0] { t2 = 1 } } } } 58 59 // N1 corrupted payload 60 let n1cap: *u8 = sys_mmap(256); cap_path(n1cap, "/tmp/ucg_n1." as *u8, e, p); uc_copy(authcap, n1cap); uc_corrupt(n1cap) 61 var n1: i64 = 0; if uc_verify(n1cap) == 0 { n1 = 1 } 62 63 // N2 forged 64 var n2: i64 = 0; if uc_verify(forgcap) == 0 { n2 = 1 } 65 66 // N3 wrong GUID 67 let n3cap: *u8 = sys_mmap(256); cap_path(n3cap, "/tmp/ucg_n3." as *u8, e, p); uc_copy(authcap, n3cap); uc_flip_guid(n3cap) 68 var n3: i64 = 0; if uc_verify(n3cap) == 0 { n3 = 1 } 69 70 var passes: i64 = 0 71 if t1 == 1 { passes = passes + 1 } 72 if t2 == 1 { passes = passes + 1 } 73 if n1 == 1 { passes = passes + 1 } 74 if n2 == 1 { passes = passes + 1 } 75 if n3 == 1 { passes = passes + 1 } 76 var green: i64 = 0 77 if passes == 5 { green = 1 } 78 79 ucg_row("T1-authentic-verifies \x00" as *u8, t1) 80 ucg_row("T2-valid-EFI-header \x00" as *u8, t2) 81 ucg_row("N1-corrupted-rejected \x00" as *u8, n1) 82 ucg_row("N2-forged-rejected \x00" as *u8, n2) 83 ucg_row("N3-wrong-GUID-rejected \x00" as *u8, n3) 84 85 let vb: *u8 = sys_mmap(528) 86 var o: i64 = 0 87 o = cp_cat(vb, o, "FW-UEFI-CAPSULE verdict=\x00" as *u8) 88 if green == 1 { o = cp_cat(vb, o, "GREEN\x00" as *u8) } else { o = cp_cat(vb, o, "RED\x00" as *u8) } 89 o = cp_cat(vb, o, " passes=\x00" as *u8); o = cp_catn(vb, o, passes); o = cp_cat(vb, o, "/5 END\x00" as *u8) 90 vb[o] = 0 as u8 91 fa_appendz(UCG_LOG, vb, 512) 92 cp_puts(vb); cp_puts("\n") 93 94 if green == 1 { return 0 } 95 return 1 96}