nx_mls_group_gate.nx source
↩ module page · 260 lines · 13150 B
1// nx_mls_group_gate.nx -- REFEREE for C7 (nx_mls_group, contract mls_epoch_advance). END-TO-END:
2// keygens three members, creates a group, commits a REMOVAL, and forks the PROMOTED elf to prove the
3// pre-declared done-rule: member removal forces an epoch advance, the removed member CANNOT decrypt
4// the next frame (negative control), with forward-secrecy and post-compromise teeth.
5// EVERYTHING is proven by forking the real elf; convergence is checked via the epoch-secret
6// COMMITMENT (sha256 of the secret) that each member prints -- the secret itself never leaves a file.
7// license_tier: ORIGINAL expect_exit: 0
8import "nx_syscalls.nx"
9import "nx_tool_run.nx"
10import "nx_gate_verdict.nx"
11const MGG_CAP: i64 = 65536
12func mgg_len(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } return n }
13func mgg_count(buf: *u8, n: i64, needle: *u8) -> i64 {
14 let m: i64 = mgg_len(needle)
15 if m <= 0 { return 0 }
16 var c: i64 = 0
17 var i: i64 = 0
18 while i + m <= n {
19 var k: i64 = 0
20 var hit: i64 = 1
21 while k < m { if buf[i+k] != needle[k] { hit = 0; k = m } else { k = k + 1 } }
22 if hit == 1 { c = c + 1; i = i + m } else { i = i + 1 }
23 }
24 return c
25}
26// copy the hex token that FOLLOWS the last occurrence of `after` (up to whitespace/newline) into out
27func mgg_after(buf: *u8, n: i64, after: *u8, out: *u8) -> i64 {
28 let m: i64 = mgg_len(after)
29 var pos: i64 = 0 - 1
30 var i: i64 = 0
31 while i + m <= n {
32 var k: i64 = 0
33 var hit: i64 = 1
34 while k < m { if buf[i+k] != after[k] { hit = 0; k = m } else { k = k + 1 } }
35 if hit == 1 { pos = i + m }
36 i = i + 1
37 }
38 if pos < 0 { out[0] = 0 as u8; return 0 - 1 }
39 var o: i64 = 0
40 while pos < n { let c: i64 = buf[pos] as i64; if c <= 32 { break } out[o] = buf[pos] as u8; o = o + 1; pos = pos + 1 }
41 out[o] = 0 as u8
42 return o
43}
44func mgg_run(elf: *u8, av: *i64, out: *u8, ol: *i64) -> i64 { return tr_run_capture(elf, av, out, MGG_CAP, ol) }
45func main(argc: i64, argv: *i64) -> i64 {
46 let ctr: *i64 = gv_ctr()
47 gv_head("nx_mls_group -- removal forces an epoch advance; a removed member cannot open the next frame; FS + PCS + tamper controls" as *u8)
48 let ELF: *u8 = "/volume1/homes/elderwesto/nishihost/nx_mls_group.elf" as *u8
49 sys_mkdir("/tmp/mgg" as *u8, 493)
50 let out: *u8 = sys_mmap(MGG_CAP)
51 let ol: *i64 = sys_mmap(16) as *i64
52 let av: *i64 = sys_mmap(64) as *i64
53 let pubA: *u8 = sys_mmap(256)
54 let pubB: *u8 = sys_mmap(256)
55 let pubC: *u8 = sys_mmap(256)
56 // ---- T1 keygen three members (deterministic seeds) ----------------------------------------
57 av[0] = ELF as i64
58 av[1] = "keygen" as i64
59 av[2] = "/tmp/mgg/a.priv" as i64
60 av[3] = "11111111" as i64
61 av[4] = 0
62 let k1: i64 = mgg_run(ELF, av, out, ol)
63 mgg_after(out, ol[0], "PUB " as *u8, pubA)
64 av[2] = "/tmp/mgg/b.priv" as i64
65 av[3] = "22222222" as i64
66 let k2: i64 = mgg_run(ELF, av, out, ol)
67 mgg_after(out, ol[0], "PUB " as *u8, pubB)
68 av[2] = "/tmp/mgg/c.priv" as i64
69 av[3] = "33333333" as i64
70 let k3: i64 = mgg_run(ELF, av, out, ol)
71 mgg_after(out, ol[0], "PUB " as *u8, pubC)
72 var t1: i64 = 0
73 if k1 == 0 { if k2 == 0 { if k3 == 0 { if mgg_len(pubA) == 64 { if mgg_len(pubB) == 64 { if mgg_len(pubC) == 64 { t1 = 1 } } } } } }
74 gv_check("T1 BITE: three X25519 member keypairs generated, each a 64-hex pubkey" as *u8, t1, ctr)
75 // roster A,B,C
76 let roster3: *u8 = sys_mmap(1024)
77 var ro: i64 = 0
78 var q: i64 = 0
79 while pubA[q] != (0 as u8) { roster3[ro] = pubA[q]; ro = ro + 1; q = q + 1 }
80 roster3[ro] = 44 as u8
81 ro = ro + 1
82 q = 0
83 while pubB[q] != (0 as u8) { roster3[ro] = pubB[q]; ro = ro + 1; q = q + 1 }
84 roster3[ro] = 44 as u8
85 ro = ro + 1
86 q = 0
87 while pubC[q] != (0 as u8) { roster3[ro] = pubC[q]; ro = ro + 1; q = q + 1 }
88 roster3[ro] = 0 as u8
89 // ---- T2 create + all three join to the SAME epoch-0 commitment -----------------------------
90 av[1] = "create" as i64
91 av[2] = "fam" as i64
92 av[3] = "deadbeefcafe" as i64
93 av[4] = "44444444444444444444444444444444444444444444444444444444444444aa" as i64
94 av[5] = "/tmp/mgg/welcome" as i64
95 av[6] = roster3 as i64
96 av[7] = 0
97 let cr: i64 = mgg_run(ELF, av, out, ol)
98 var t2a: i64 = 0
99 if cr == 0 { if mgg_count(out, ol[0], "MLS-CREATE-OK" as *u8) == 1 { if mgg_count(out, ol[0], "members=3" as *u8) == 1 { t2a = 1 } } }
100 gv_check("T2a create wraps epoch-0 to all three members" as *u8, t2a, ctr)
101 let commA: *u8 = sys_mmap(256)
102 let commB: *u8 = sys_mmap(256)
103 let commC: *u8 = sys_mmap(256)
104 av[1] = "join" as i64
105 av[2] = "/tmp/mgg/welcome" as i64
106 av[3] = "/tmp/mgg/a.priv" as i64
107 av[4] = "/tmp/mgg/a.st0" as i64
108 av[5] = 0
109 let j1: i64 = mgg_run(ELF, av, out, ol)
110 mgg_after(out, ol[0], "commit=" as *u8, commA)
111 av[3] = "/tmp/mgg/b.priv" as i64
112 av[4] = "/tmp/mgg/b.st0" as i64
113 let j2: i64 = mgg_run(ELF, av, out, ol)
114 mgg_after(out, ol[0], "commit=" as *u8, commB)
115 av[3] = "/tmp/mgg/c.priv" as i64
116 av[4] = "/tmp/mgg/c.st0" as i64
117 let j3: i64 = mgg_run(ELF, av, out, ol)
118 mgg_after(out, ol[0], "commit=" as *u8, commC)
119 var t2: i64 = 0
120 if j1 == 0 { if j2 == 0 { if j3 == 0 {
121 if mgg_len(commA) == 64 { if mgg_count(commA, 64, commB) == 1 { if mgg_count(commA, 64, commC) == 1 { t2 = 1 } } }
122 } } }
123 gv_check("T2 CONVERGENCE: all three members independently derive the SAME epoch-0 secret (equal commitments)" as *u8, t2, ctr)
124 // ---- roster A,C (B removed) ----------------------------------------------------------------
125 let roster2: *u8 = sys_mmap(1024)
126 ro = 0
127 q = 0
128 while pubA[q] != (0 as u8) { roster2[ro] = pubA[q]; ro = ro + 1; q = q + 1 }
129 roster2[ro] = 44 as u8
130 ro = ro + 1
131 q = 0
132 while pubC[q] != (0 as u8) { roster2[ro] = pubC[q]; ro = ro + 1; q = q + 1 }
133 roster2[ro] = 0 as u8
134 // ---- T3 A commits the removal of B ---------------------------------------------------------
135 av[1] = "commit" as i64
136 av[2] = "/tmp/mgg/a.st0" as i64
137 av[3] = "5555555555555555555555555555555555555555555555555555555555555566" as i64
138 av[4] = roster2 as i64
139 av[5] = "/tmp/mgg/commit1" as i64
140 av[6] = "/tmp/mgg/a.st1" as i64
141 av[7] = 0
142 let cm: i64 = mgg_run(ELF, av, out, ol)
143 let commA1: *u8 = sys_mmap(256)
144 mgg_after(out, ol[0], "commit=" as *u8, commA1)
145 var t3: i64 = 0
146 if cm == 0 { if mgg_count(out, ol[0], "MLS-COMMIT-OK epoch=1" as *u8) == 1 { if mgg_count(out, ol[0], "new_members=2" as *u8) == 1 { t3 = 1 } } }
147 gv_check("T3 removal is a COMMIT that advances the epoch to 1 over the 2-member roster" as *u8, t3, ctr)
148 // ---- T4 C applies and converges with A on epoch 1 ------------------------------------------
149 av[1] = "apply" as i64
150 av[2] = "/tmp/mgg/commit1" as i64
151 av[3] = "/tmp/mgg/c.priv" as i64
152 av[4] = "/tmp/mgg/c.st0" as i64
153 av[5] = "/tmp/mgg/c.st1" as i64
154 av[6] = 0
155 let ap: i64 = mgg_run(ELF, av, out, ol)
156 let commC1: *u8 = sys_mmap(256)
157 mgg_after(out, ol[0], "commit=" as *u8, commC1)
158 var t4: i64 = 0
159 if ap == 0 { if mgg_len(commC1) == 64 { if mgg_count(commA1, 64, commC1) == 1 { t4 = 1 } } }
160 gv_check("T4 the remaining member C applies the commit and converges with A on the SAME epoch-1 secret" as *u8, t4, ctr)
161 // ---- T5 THE MONEY TOOTH: removed member B CANNOT advance ------------------------------------
162 av[1] = "apply" as i64
163 av[2] = "/tmp/mgg/commit1" as i64
164 av[3] = "/tmp/mgg/b.priv" as i64
165 av[4] = "/tmp/mgg/b.st0" as i64
166 av[5] = "/tmp/mgg/b.st1" as i64
167 av[6] = 0
168 let apb: i64 = mgg_run(ELF, av, out, ol)
169 var t5: i64 = 0
170 if apb != 0 { if mgg_count(out, ol[0], "MLS-REMOVED cannot-advance" as *u8) == 1 { t5 = 1 } }
171 gv_check("T5 REMOVAL NEG-CONTROL: the removed member B, holding the OLD epoch secret, CANNOT apply the commit -- no wrap is addressed to it" as *u8, t5, ctr)
172 // ---- T6 epoch-1 frame: A seals, C opens ----------------------------------------------------
173 av[1] = "seal" as i64
174 av[2] = "/tmp/mgg/a.st1" as i64
175 av[3] = "7" as i64
176 av[4] = "after B is gone" as i64
177 av[5] = "/tmp/mgg/frame1" as i64
178 av[6] = 0
179 let sl: i64 = mgg_run(ELF, av, out, ol)
180 av[1] = "open" as i64
181 av[2] = "/tmp/mgg/c.st1" as i64
182 av[3] = "/tmp/mgg/frame1" as i64
183 av[4] = 0
184 let op: i64 = mgg_run(ELF, av, out, ol)
185 var t6: i64 = 0
186 if sl == 0 { if op == 0 { if mgg_count(out, ol[0], "MLS-OPEN-OK" as *u8) == 1 { if mgg_count(out, ol[0], "plaintext=after B is gone" as *u8) == 1 { t6 = 1 } } } }
187 gv_check("T6 the two remaining members share a real ChaCha20 frame at epoch 1: A seals, C opens byte-identical" as *u8, t6, ctr)
188 // ---- T7 THE E2E DENIAL: B (still at epoch-0 secret) CANNOT open the epoch-1 frame -----------
189 av[1] = "open" as i64
190 av[2] = "/tmp/mgg/b.st0" as i64
191 av[3] = "/tmp/mgg/frame1" as i64
192 av[4] = 0
193 let opb: i64 = mgg_run(ELF, av, out, ol)
194 var t7: i64 = 0
195 if opb != 0 { if mgg_count(out, ol[0], "MLS-OPEN-DENIED" as *u8) == 1 { if mgg_count(out, ol[0], "after B is gone" as *u8) == 0 { t7 = 1 } } }
196 gv_check("T7 E2E DENIAL: removed member B cannot open the epoch-1 frame -- the MAC fails under its stale secret and NOTHING is decrypted (the done-rule, end to end)" as *u8, t7, ctr)
197 // ---- T8 FORWARD SECRECY: an epoch-0 frame is not openable with the epoch-1 secret ----------
198 av[1] = "seal" as i64
199 av[2] = "/tmp/mgg/a.st0" as i64
200 av[3] = "3" as i64
201 av[4] = "epoch zero message" as i64
202 av[5] = "/tmp/mgg/frame0" as i64
203 av[6] = 0
204 let sl0: i64 = mgg_run(ELF, av, out, ol)
205 av[1] = "open" as i64
206 av[2] = "/tmp/mgg/a.st1" as i64
207 av[3] = "/tmp/mgg/frame0" as i64
208 av[4] = 0
209 let op0: i64 = mgg_run(ELF, av, out, ol)
210 var t8: i64 = 0
211 if sl0 == 0 { if op0 != 0 { if mgg_count(out, ol[0], "MLS-OPEN-DENIED" as *u8) == 1 { t8 = 1 } } }
212 gv_check("T8 FORWARD SECRECY: the epoch-1 secret cannot open an epoch-0 frame -- advancing discards reach to the old key (one-way HKDF chain)" as *u8, t8, ctr)
213 // ---- T9 anti-vacuity: A CAN still open its own epoch-0 frame -------------------------------
214 av[1] = "open" as i64
215 av[2] = "/tmp/mgg/a.st0" as i64
216 av[3] = "/tmp/mgg/frame0" as i64
217 av[4] = 0
218 let op0a: i64 = mgg_run(ELF, av, out, ol)
219 var t9: i64 = 0
220 if op0a == 0 { if mgg_count(out, ol[0], "plaintext=epoch zero message" as *u8) == 1 { t9 = 1 } }
221 gv_check("T9 anti-vacuity: the epoch-0 secret DOES open the epoch-0 frame -- open is not refusing everything (T7/T8 carry information)" as *u8, t9, ctr)
222 // ---- T10 POST-COMPROMISE: a fresh commit (no membership change) rotates past a leaked secret
223 av[1] = "commit" as i64
224 av[2] = "/tmp/mgg/a.st1" as i64
225 av[3] = "6666666666666666666666666666666666666666666666666666666666666677" as i64
226 av[4] = roster2 as i64
227 av[5] = "/tmp/mgg/commit2" as i64
228 av[6] = "/tmp/mgg/a.st2" as i64
229 av[7] = 0
230 let cm2: i64 = mgg_run(ELF, av, out, ol)
231 let commA2: *u8 = sys_mmap(256)
232 mgg_after(out, ol[0], "commit=" as *u8, commA2)
233 var t10: i64 = 0
234 if cm2 == 0 { if mgg_len(commA2) == 64 { if mgg_count(commA1, 64, commA2) == 0 { t10 = 1 } } }
235 gv_check("T10 POST-COMPROMISE: an update commit rotates to a NEW epoch-2 secret (commitment differs from epoch 1) -- a passively-leaked old secret does not yield the new one, because commit_secret is fresh and ECDH-wrapped" as *u8, t10, ctr)
236 // ---- T11 TAMPER: flip a byte of the wrapped commit -> apply MAC fails -----------------------
237 let cbuf: *u8 = sys_mmap(MGG_CAP)
238 let cfd: i64 = sys_openat_rd("/tmp/mgg/commit1" as *u8)
239 var cn: i64 = 0
240 if cfd >= 0 { cn = sys_read(cfd, cbuf, MGG_CAP); sys_close(cfd) }
241 // corrupt the first hex char after the last 'to|' blob pipe region: flip a char in the middle
242 var mid: i64 = cn - 40
243 if mid < 0 { mid = 0 }
244 if cbuf[mid] == (97 as u8) { cbuf[mid] = 98 as u8 } else { cbuf[mid] = 97 as u8 }
245 let tfd: i64 = sys_openat_wr("/tmp/mgg/commit1_bad" as *u8, 420)
246 var tw: i64 = 0
247 while tw < cn { let r: i64 = sys_write(tfd, (cbuf as i64 + tw) as *u8, cn - tw); if r <= 0 { break } tw = tw + r }
248 sys_close(tfd)
249 av[1] = "apply" as i64
250 av[2] = "/tmp/mgg/commit1_bad" as i64
251 av[3] = "/tmp/mgg/c.priv" as i64
252 av[4] = "/tmp/mgg/c.st0" as i64
253 av[5] = "/tmp/mgg/c.stbad" as i64
254 av[6] = 0
255 let apbad: i64 = mgg_run(ELF, av, out, ol)
256 var t11: i64 = 0
257 if apbad != 0 { if mgg_count(out, ol[0], "mac-fail" as *u8) == 1 { t11 = 1 } }
258 gv_check("T11 TAMPER NEG-CONTROL: a single flipped byte in the wrapped commit is caught by the HMAC and apply REFUSES -- the wrap is authenticated, not just encrypted" as *u8, t11, ctr)
259 return gv_verdict("MLS-GROUP-GATE" as *u8, ctr, "removal forces an epoch advance and denies the removed member the next frame end-to-end; forward secrecy, post-compromise and authenticated wraps all proven by forking the real elf" as *u8)
260}