nx_neverbrick_gate.nx source
↩ module page · 113 lines · 6698 B
1// nx_neverbrick_gate.nx -- proves the Rule-26 reversibility classifier actually discriminates, and that
2// it fails CLOSED. Rule 26 says never-brick must be proven mechanically, never asserted; this is the
3// proof, and it calls the SHIPPING functions in nx_mcu_brick.nx so it cannot drift from what a real
4// write chokepoint runs.
5//
6// NON-VACUITY IS THE POINT. Two failure modes would make this gate a liar, so both have controls:
7// - a classifier that returns RED for EVERYTHING passes every safety test and blocks the product.
8// T4 and T8 are the positive controls: the real esp32-ai flash workload MUST come back GREEN.
9// - a classifier that returns GREEN for everything would sail through the positive tests. T1/T2 are
10// the negative controls: undeclared and null namespaces MUST come back RED.
11// - T7 is the neg-control on T6's READER: if nb_efuse_kills_recovery returned 1 unconditionally, T6
12// would pass while measuring nothing. A check and its own neg-control failing together means the
13// instrument is broken.
14//
15// T5 is the keystone assertion: the same flash write that is GREEN with the ROM download path intact
16// MUST be RED once DIS_DOWNLOAD_MODE is burned. Flash reversibility is conditional, not intrinsic.
17// license_tier: ORIGINAL No hw writes (Rule 26). expect_exit: 0
18import "nx_syscalls.nx"
19import "nx_mcu_brick.nx"
20
21func nbg_len(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } return n }
22func nbg_p(s: *u8) -> i64 { sys_write(1, s, nbg_len(s)); return 0 }
23func nbg_pn(v: i64) -> i64 {
24 let t: *u8 = sys_mmap(32)
25 var m: i64 = v
26 if m < 0 { sys_write(1, "-" as *u8, 1); m = 0 - m }
27 var k: i64 = 0
28 if m == 0 { t[0] = 48 as u8; k = 1 }
29 while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 }
30 let o: *u8 = sys_mmap(32)
31 var i: i64 = 0
32 while i < k { o[i] = t[k-1-i]; i = i + 1 }
33 sys_write(1, o, k)
34 return 0
35}
36func nbg_ck(name: *u8, c: i64) -> i64 {
37 if c == 1 { nbg_p(" PASS " as *u8) } else { nbg_p(" FAIL " as *u8) }
38 nbg_p(name); nbg_p("\n" as *u8)
39 return c
40}
41
42func main() -> i64 {
43 nbg_p("=== nx_neverbrick_gate -- can any MCU write path reach an irreversible operation? ===\n" as *u8)
44 var pass: i64 = 0
45 var total: i64 = 0
46
47 // T1 NEG-CONTROL: an undeclared namespace must be REFUSED. If this fails, every GREEN below is
48 // meaningless because the classifier would be admitting things it has never heard of.
49 var t1: i64 = 0
50 if nb_verdict("vbios" as *u8, NB_DL_INTACT) == NB_RED { t1 = 1 }
51 pass = pass + nbg_ck("T1 NEG-CONTROL: an UNDECLARED namespace is REFUSED (fail-closed is reachable)" as *u8, t1); total = total + 1
52
53 // T2 NEG-CONTROL: a null namespace pointer must also be refused, not crash and not sail through.
54 var t2: i64 = 0
55 if nb_verdict(0 as *u8, NB_DL_INTACT) == NB_RED { t2 = 1 }
56 pass = pass + nbg_ck("T2 NEG-CONTROL: a NULL namespace is REFUSED, not admitted" as *u8, t2); total = total + 1
57
58 // T3 the OTP class itself: eFuse writes are irreversible by construction and must never be GREEN.
59 var t3: i64 = 0
60 if nb_verdict("efuse" as *u8, NB_DL_INTACT) == NB_RED { t3 = 1 }
61 pass = pass + nbg_ck("T3 an eFuse-namespace write is REFUSED even with recovery intact (OTP is OTP)" as *u8, t3); total = total + 1
62
63 // T4 POSITIVE CONTROL: the gate must still permit the capability we are actually building. A guard
64 // that refuses every write is not safety, it is a product that does not exist.
65 var t4: i64 = 0
66 if nb_verdict("flash" as *u8, NB_DL_INTACT) == NB_GREEN { t4 = 1 }
67 pass = pass + nbg_ck("T4 POS-CONTROL: a flash write with the ROM download path intact is PERMITTED" as *u8, t4); total = total + 1
68
69 // T5 KEYSTONE: the identical write flips to REFUSED once the recovery path is burned away.
70 var t5: i64 = 0
71 if nb_verdict("flash" as *u8, NB_DL_BURNED) == NB_RED { t5 = 1 }
72 pass = pass + nbg_ck("T5 KEYSTONE: the SAME flash write is REFUSED once download mode is burned" as *u8, t5); total = total + 1
73
74 // T6 every field that destroys the recovery path is recognised as doing so.
75 var t6: i64 = 1
76 if nb_efuse_kills_recovery("DIS_DOWNLOAD_MODE" as *u8) != 1 { t6 = 0 }
77 if nb_efuse_kills_recovery("DIS_LEGACY_SPI_BOOT" as *u8) != 1 { t6 = 0 }
78 if nb_efuse_kills_recovery("DIS_DIRECT_BOOT" as *u8) != 1 { t6 = 0 }
79 if nb_efuse_kills_recovery("DIS_USB_SERIAL_JTAG" as *u8) != 1 { t6 = 0 }
80 if nb_efuse_kills_recovery("DIS_PAD_JTAG" as *u8) != 1 { t6 = 0 }
81 if nb_efuse_kills_recovery("SECURE_BOOT_EN" as *u8) != 1 { t6 = 0 }
82 if nb_efuse_kills_recovery("SPI_BOOT_CRYPT_CNT" as *u8) != 1 { t6 = 0 }
83 if nb_efuse_kills_recovery("WR_DIS" as *u8) != 1 { t6 = 0 }
84 if nb_efuse_kills_recovery("RD_DIS" as *u8) != 1 { t6 = 0 }
85 pass = pass + nbg_ck("T6 all 9 recovery-destroying eFuse fields are recognised" as *u8, t6); total = total + 1
86
87 // T7 NEG-CONTROL ON T6's READER: an unrelated field must NOT be flagged. Without this, a reader
88 // that returns 1 for every input would make T6 pass while measuring nothing at all.
89 var t7: i64 = 0
90 if nb_efuse_kills_recovery("USER_DATA" as *u8) == 0 { t7 = 1 }
91 pass = pass + nbg_ck("T7 NEG-CONTROL: an unrelated eFuse field is NOT flagged (the reader discriminates)" as *u8, t7); total = total + 1
92
93 // T8 POSITIVE CONTROL on the real workload: every partition esp32-ai actually writes -- nvs,
94 // factory app, the 15.6MB model region, coredump -- is flash-class, so the whole deployment is
95 // admitted while recovery lives. This is what makes the gate about our product and not a toy.
96 var t8: i64 = 1
97 if nb_verdict("flash" as *u8, NB_DL_INTACT) != NB_GREEN { t8 = 0 }
98 if nb_class_of_ns("flash" as *u8) != NB_REVERSIBLE { t8 = 0 }
99 if nb_class_of_ns("psram" as *u8) != NB_VOLATILE { t8 = 0 }
100 if nb_class_of_ns("ram" as *u8) != NB_VOLATILE { t8 = 0 }
101 pass = pass + nbg_ck("T8 POS-CONTROL: the real esp32-ai partition workload is ADMITTED (flash+PSRAM+SRAM)" as *u8, t8); total = total + 1
102
103 // T9 even a benign eFuse burn is refused. OTP is OTP: a field that does not kill recovery is still
104 // a one-way door, so the eFuse verdict does not depend on which field it is.
105 var t9: i64 = 0
106 if nb_verdict_efuse("USER_DATA" as *u8) == NB_RED { t9 = 1 }
107 pass = pass + nbg_ck("T9 a BENIGN eFuse burn is still REFUSED (one-way doors are refused as a class)" as *u8, t9); total = total + 1
108
109 nbg_p("=== nx_neverbrick_gate " as *u8); nbg_pn(pass); nbg_p("/" as *u8); nbg_pn(total)
110 if pass == total { nbg_p(" VERDICT GREEN ===\n" as *u8); return 0 }
111 nbg_p(" VERDICT RED ===\n" as *u8)
112 return 1
113}