code wiki / _hdl_build / nx_vault_selftest.nx
nx_vault_selftest.nx source
↩ module page · 97 lines · 4833 B
1// nx_vault_selftest.nx -- SECURITY SELF-TEST: the vault's three guarantees re-proven mechanically,
2// so they become a STANDING proof obligation under nx_prove_all (a security property is only real
3// if it is CONTINUOUSLY re-verified, not asserted once). Exercises the REAL bootstrap-built
4// _offc/nx_vault.elf via fork/exec (so this gate stays sovereign-buildable -- no crypto import that
5// hits the nxasm gap). Proves: (1) seal->open ROUNDTRIP recovers the secret; (2) the vault file
6// holds NO plaintext; (3) a WRONG passphrase FAILS CLOSED (no output). Exit 0 iff all three hold.
7// license_tier: ORIGINAL
8import "nx_syscalls.nx"
9const AT_MAGIC_65536: i64 = 65536
10const AT_FDCWD: i64 = 0 - 100
11func _p(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 }
12func vs_run(path: *u8, a1: *u8, a2: *u8) -> i64 {
13 let pid: i64 = sys_fork()
14 if pid == 0 {
15 let argv: *i64 = sys_mmap(64) as *i64
16 argv[0] = path as i64
17 var ai: i64 = 1
18 if (a1 as i64) != 0 { argv[ai] = a1 as i64; ai = ai + 1 }
19 if (a2 as i64) != 0 { argv[ai] = a2 as i64; ai = ai + 1 }
20 argv[ai] = 0
21 let envp: *i64 = sys_mmap(16) as *i64
22 envp[0] = 0
23 sys_execve(path, argv, envp)
24 sys_exit(127)
25 }
26 let st: *i64 = sys_mmap(16) as *i64
27 sys_wait4(pid, st, 0)
28 return (st[0] >> 8) & 0xff
29}
30func vs_write(path: *u8, s: *u8, n: i64) -> i64 {
31 let fd: i64 = sys_openat_wr(path, 0x180)
32 if fd < 0 { return 0 - 1 }
33 sys_write(fd, s, n)
34 sys_close(fd)
35 return 0
36}
37func vs_read(path: *u8, out: *u8, cap: i64, lenbox: *i64) -> i64 {
38 let fd: i64 = sys_openat_rd(path)
39 if fd < 0 { lenbox[0] = 0; return 0 - 1 }
40 var total: i64 = 0
41 var go: i64 = 1
42 while go == 1 { let base: i64 = out as i64; let r: i64 = sys_read(fd, (base + total) as *u8, cap - total); if r <= 0 { go = 0 } else { total = total + r } if total >= cap { go = 0 } }
43 sys_close(fd)
44 lenbox[0] = total
45 return total
46}
47func vs_contains(buf: *u8, n: i64, pat: *u8) -> i64 {
48 var pl: i64 = 0
49 while pat[pl] != (0 as u8) { pl = pl + 1 }
50 var i: i64 = 0
51 while i + pl <= n { var k: i64 = 0; var hit: i64 = 1; while k < pl { if buf[i+k] != pat[k] { hit = 0; k = pl } else { k = k + 1 } } if hit == 1 { return 1 } i = i + 1 }
52 return 0
53}
54func vs_unlink(path: *u8) -> i64 { __syscall(263, AT_FDCWD, path, 0, 0, 0, 0) return 0 }
55func main() -> i64 {
56 _p("=== VAULT SELF-TEST: re-proving the three security guarantees (standing obligation) ===\n" as *u8)
57 let secret: *u8 = "kat-secret-9f3a" as *u8
58 var slen: i64 = 0
59 while secret[slen] != (0 as u8) { slen = slen + 1 }
60 let vpath: *u8 = "/tmp/_vst.nv" as *u8
61 let lenbox: *i64 = sys_mmap(16) as *i64
62 var pass: i64 = 1
63 // SEAL with a known passphrase
64 vs_write("/tmp/nxsecret.in" as *u8, secret, slen)
65 vs_write("/tmp/nxpass" as *u8, "selftest-pass-A" as *u8, 15)
66 if vs_run("_offc/nx_vault.elf" as *u8, "seal" as *u8, vpath) != 0 { _p(" [1] seal FAILED\n" as *u8); pass = 0 }
67 // (2) no plaintext in the vault file
68 let vbuf: *u8 = sys_mmap(AT_MAGIC_65536)
69 vs_read(vpath, vbuf, AT_MAGIC_65536, lenbox)
70 if vs_contains(vbuf, lenbox[0], secret) == 1 { _p(" [2] LEAK: plaintext in vault file\n" as *u8); pass = 0 }
71 else { _p(" [2] no-plaintext-in-file: PASS\n" as *u8) }
72 // (1) roundtrip with the correct passphrase
73 vs_unlink("/tmp/nxsecret.out" as *u8)
74 vs_write("/tmp/nxpass" as *u8, "selftest-pass-A" as *u8, 15)
75 vs_run("_offc/nx_vault.elf" as *u8, "open" as *u8, vpath)
76 let obuf: *u8 = sys_mmap(AT_MAGIC_65536)
77 vs_read("/tmp/nxsecret.out" as *u8, obuf, AT_MAGIC_65536, lenbox)
78 var same: i64 = 1
79 if lenbox[0] != slen { same = 0 } else { var k: i64 = 0; while k < slen { if obuf[k] != secret[k] { same = 0; k = slen } else { k = k + 1 } } }
80 if same == 1 { _p(" [1] roundtrip: PASS\n" as *u8) } else { _p(" [1] roundtrip FAILED\n" as *u8); pass = 0 }
81 // (3) wrong passphrase FAILS CLOSED -- no output produced
82 vs_unlink("/tmp/nxsecret.out" as *u8)
83 vs_write("/tmp/nxpass" as *u8, "WRONG-pass-ZZ" as *u8, 13)
84 vs_run("_offc/nx_vault.elf" as *u8, "open" as *u8, vpath)
85 let rfd: i64 = sys_openat_rd("/tmp/nxsecret.out" as *u8)
86 if rfd >= 0 { sys_close(rfd); _p(" [3] SECURITY-FAIL: output produced on wrong passphrase\n" as *u8); pass = 0 }
87 else { _p(" [3] fail-closed on wrong passphrase: PASS\n" as *u8) }
88 // shred ephemerals
89 vs_unlink("/tmp/nxsecret.in" as *u8)
90 vs_unlink("/tmp/nxpass" as *u8)
91 vs_unlink("/tmp/nxsecret.out" as *u8)
92 vs_unlink(vpath)
93 if pass == 1 { _p(" VAULT SELF-TEST: PASS (encrypted-at-rest + roundtrip + fail-closed all hold)\n" as *u8); sys_exit(0); return 0 }
94 _p(" VAULT SELF-TEST: FAIL\n" as *u8)
95 sys_exit(1)
96 return 1
97}