nx_install_attest.nx source
↩ module page · 187 lines · 7376 B
1// nx_install_attest.nx -- defensive primitives around install_hash.
2//
3// Composes nx_install_plan + nx_install_hash with three small
4// utilities that close the human-loop + replay-attestation gap:
5//
6// nx_install_hash_to_hex(digest, out_hex)
7// 32-byte binary digest -> 64 ASCII lowercase hex chars. Human-
8// readable form for logs / audit trails / cross-system transfer.
9//
10// nx_install_hash_from_hex(in_hex, out_digest)
11// Inverse: 64 ASCII hex chars -> 32-byte binary digest. Accepts
12// lowercase a-f, uppercase A-F, and 0-9. Rejects any other byte
13// (including spaces / leading 0x / trailing newlines). Caller
14// is responsible for stripping framing.
15//
16// nx_install_hash_verify_against(plan, expected_digest)
17// Recompute install_hash from plan + compare to expected.
18// Returns NX_ATTEST_VERIFIED on bit-equal, NX_ATTEST_TAMPERED on
19// mismatch, NX_ATTEST_BAD_INPUT on null / canary-stomped plan.
20// This is the replay-attestation loop: "given this attested
21// plan + this attested hash, does the plan still hash to the
22// expected value?"
23//
24// Per [[feedback-end-to-end-bit-traceability-architecture]]: the hex
25// form is what gets written into install_attest.jsonl logs +
26// embedded in audit trails. Binary form stays in memory for
27// internal comparison.
28//
29// V1 scope:
30// - lowercase hex emission ("a..f"); decoder tolerates both cases
31// - exactly NX_INSTALL_HASH_BYTES (32) bytes / 64 hex chars; no
32// length negotiation
33// - no leading "0x" / no separators / no whitespace
34//
35// Deferred per roadmap:
36// - cross-machine attestation (in-toto link metadata with signed
37// install_hash) -- SA-7 remainder
38// - Rekor-class append-only audit log -- SA-7 remainder
39// - Byzantine N-of-M attestation chain (multiple independent
40// compile paths must produce bit-equal install_hash) -- SA-7
41// - PGP / Ed25519 signature wrapping the hex form -- SA-7
42//
43// genealogy_id: rfc4648_base16 + slsa_2021 + in_toto_2018 +
44// sigstore_2021 + cardinal_2026-05-19_self_assembly
45// lineage_id: substrate_install_attest_v1
46//
47// nx_capability_manifest:
48// variant_class: install_attest_helpers
49// variant_id: install_attest_hex_verify_v1
50// requires_isa: [rv64imac, x86_64]
51// requires_syscalls: [mmap]
52// requires_ram_min_b: 4096
53// tier_floor: NX_TIER_MCU
54// tier_ceiling: NX_TIER_HPC
55// cost_model:
56// flops_per_n: 2.0 // ~2 ops per hex char
57// bytes_per_n: 64.0 // hex string size
58// syscalls_per_n: 0.0
59// adversary_class: THREAT_AI_ADVERSARY
60//
61// nx_safety_envelope:
62// intended_use: "Hex codec + replay-attestation for install_hash;
63// closes the human-readable + verifiable loop"
64// sil_target: SIL2
65// evidence: [roundtrip_proven, case_tolerant_decode,
66// bad_char_rejected, tamper_distinguished_from_match]
67// verdict: NOT_YET_EVALUATED
68
69import "nx_syscalls.nx"
70import "nx_install_plan.nx"
71import "nx_install_hash.nx"
72
73// ===== Verdict sealed enum =======================================
74const NX_ATTEST_VERIFIED: i64 = 0
75const NX_ATTEST_TAMPERED: i64 = 1
76const NX_ATTEST_BAD_INPUT: i64 = 2
77const NX_ATTEST_N: i64 = 3
78
79func nx_attest_verdict_is_valid(v: i64) -> i64 {
80 if v < 0 { return 0 }
81 if v >= NX_ATTEST_N { return 0 }
82 return 1
83}
84
85// Hex decode verdict (subset of operations don't reach attest level).
86const NX_HEX_OK: i64 = 0
87const NX_HEX_BAD_CHAR: i64 = 1
88const NX_HEX_BAD_INPUT: i64 = 2
89
90// ===== Nibble encoders ===========================================
91// 0..15 -> ASCII '0'..'9' / 'a'..'f'. Lowercase output.
92func _nibble_to_hex_lower(n: i64) -> i64 {
93 if n < 0 { return 48 } // '0' (safety fallback)
94 if n < 10 { return 48 + n } // '0' + n
95 if n < 16 { return 87 + n } // 'a' - 10 = 87
96 return 48 // safety fallback
97}
98
99// ASCII char -> 0..15, or -1 on invalid. Accepts both cases.
100func _hex_to_nibble(c: i64) -> i64 {
101 let v: i64 = c & 255
102 if v >= 48 {
103 if v <= 57 { return v - 48 } // '0'..'9'
104 }
105 if v >= 97 {
106 if v <= 102 { return (v - 97) + 10 } // 'a'..'f'
107 }
108 if v >= 65 {
109 if v <= 70 { return (v - 65) + 10 } // 'A'..'F'
110 }
111 return -1
112}
113
114// ===== Hex encode ================================================
115// 32-byte binary digest -> 64 ASCII lowercase hex chars.
116// out_hex must be at least 64 bytes; caller-allocated.
117
118func nx_install_hash_to_hex(digest: *u8, out_hex: *u8) -> i64 {
119 if (digest as i64) == 0 { return NX_HEX_BAD_INPUT }
120 if (out_hex as i64) == 0 { return NX_HEX_BAD_INPUT }
121
122 var i: i64 = 0
123 while i < NX_INSTALL_HASH_BYTES {
124 let b: i64 = (digest[i] as i64) & 255
125 let hi: i64 = (b >> 4) & 15
126 let lo: i64 = b & 15
127 out_hex[i * 2 + 0] = (_nibble_to_hex_lower(hi)) as u8
128 out_hex[i * 2 + 1] = (_nibble_to_hex_lower(lo)) as u8
129 i = i + 1
130 }
131 return NX_HEX_OK
132}
133
134// ===== Hex decode ================================================
135// 64 ASCII hex chars -> 32-byte binary digest. out_digest must be
136// at least 32 bytes. Accepts both cases. Rejects any other byte
137// (returns NX_HEX_BAD_CHAR; out_digest may be in partial state).
138
139func nx_install_hash_from_hex(in_hex: *u8, out_digest: *u8) -> i64 {
140 if (in_hex as i64) == 0 { return NX_HEX_BAD_INPUT }
141 if (out_digest as i64) == 0 { return NX_HEX_BAD_INPUT }
142
143 var i: i64 = 0
144 while i < NX_INSTALL_HASH_BYTES {
145 let hi_c: i64 = (in_hex[i * 2 + 0]) as i64
146 let lo_c: i64 = (in_hex[i * 2 + 1]) as i64
147 let hi: i64 = _hex_to_nibble(hi_c)
148 let lo: i64 = _hex_to_nibble(lo_c)
149 if hi < 0 { return NX_HEX_BAD_CHAR }
150 if lo < 0 { return NX_HEX_BAD_CHAR }
151 out_digest[i] = ((hi << 4) | lo) as u8
152 i = i + 1
153 }
154 return NX_HEX_OK
155}
156
157// ===== Replay-attestation verify ================================
158// Recompute install_hash from the plan + compare to expected digest.
159// VERIFIED on bit-equal, TAMPERED on mismatch, BAD_INPUT on
160// null / canary-stomped plan / null expected.
161//
162// This is the racing-line replay loop: caller has an attested plan
163// + attested hash (e.g., from a previous session's install record);
164// nx_install_hash_verify_against asks "does this plan still hash to
165// the same value?" Useful for:
166// - audit trails (compare attested log entries against current
167// plan state)
168// - cross-machine verification (machine A produces plan + hash;
169// machine B re-runs verify_against and confirms)
170// - tamper detection on persisted plans (canary detected;
171// verify_against refuses)
172
173func nx_install_hash_verify_against(plan: *NxInstallPlan,
174 expected_digest: *u8) -> i64 {
175 if (plan as i64) == 0 { return NX_ATTEST_BAD_INPUT }
176 if (expected_digest as i64) == 0 { return NX_ATTEST_BAD_INPUT }
177 if nx_install_plan_is_valid(plan) != 1 { return NX_ATTEST_BAD_INPUT }
178
179 let now_digest: *u8 = sys_mmap(64)
180 let rc: i64 = nx_install_hash_compute(plan, now_digest)
181 if rc != NX_HASH_OK { return NX_ATTEST_BAD_INPUT }
182
183 if nx_install_hash_eq(now_digest, expected_digest) == 1 {
184 return NX_ATTEST_VERIFIED
185 }
186 return NX_ATTEST_TAMPERED
187}