code wiki / _hdl_build / nx_share_plane_gate.nx
nx_share_plane_gate.nx source
↩ module page · 285 lines · 14500 B
1// nx_share_plane_gate.nx -- the regression proof for the share plane. Every tooth is stated as the ATTACK
2// it blocks, because a sharing plane's job is refusal: the failure mode is not "the feature is missing",
3// it is "someone saw something they should not have", and that failure is silent.
4// license_tier: ORIGINAL expect_exit: 0
5import "nx_syscalls.nx"
6import "nx_share_plane.nx"
7
8const SG_CAP: i64 = 64
9const SG_ALICE: i64 = 1001
10const SG_BOB: i64 = 1002
11const SG_CARA: i64 = 1003
12const SG_DAN: i64 = 1004
13const SG_ALBUM: i64 = 7001
14const SG_CARD: i64 = 7002
15
16func g_w(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 }
17func g_n(v: i64) -> i64 {
18 let bb: *u8=sys_mmap(28); var m: i64=v
19 if m<0 { m=0-m; sys_write(1,"-" as *u8,1) }
20 let t: *u8=sys_mmap(28); var k: i64=0
21 if m==0 { t[0]=48 as u8; k=1 }
22 while m>0 { t[k]=(48+(m%10)) as u8; m=m/10; k=k+1 }
23 var i: i64=0
24 while i<k { bb[i]=t[k-1-i]; i=i+1 }
25 sys_write(1,bb,k); return 0
26}
27func g_t(pass: i64, label: *u8, fails: *i64) -> i64 {
28 g_w(" " as *u8); g_w(label); g_w(": " as *u8)
29 if pass==1 { g_w("PASS\n" as *u8) } else { g_w("FAIL\n" as *u8); fails[0]=fails[0]+1 }
30 return 0
31}
32func fresh() -> *i64 {
33 let a: *i64 = sys_mmap(8*sp_slots_needed(SG_CAP)) as *i64
34 sp_init(a, SG_CAP)
35 return a
36}
37
38func main() -> i64 {
39 let fails: *i64 = sys_mmap(16) as *i64
40 fails[0]=0
41 g_w("=== nx_share_plane_gate -- a sharing plane is judged by what it REFUSES ===\n" as *u8)
42
43 // T1 deny by default: an unclaimed resource grants nothing to anybody, including its future owner
44 let a1: *i64 = fresh()
45 var t1: i64=0
46 if sp_may(a1, SG_ALICE, SP_C_ALBUM, SG_ALBUM, SP_VIEW)==0 {
47 if sp_may(a1, SG_BOB, SP_C_ALBUM, SG_ALBUM, SP_VIEW)==0 { t1=1 }
48 }
49 g_t(t1, "T1 DENY BY DEFAULT nothing is visible on an unclaimed resource" as *u8, fails)
50
51 // T2 the owner sees their own resource without any grant row existing
52 let a2: *i64 = fresh()
53 sp_claim(a2, SG_ALICE, SP_C_ALBUM, SG_ALBUM)
54 var t2: i64=0
55 if sp_may(a2, SG_ALICE, SP_C_ALBUM, SG_ALBUM, SP_VIEW)==1 {
56 if sp_may(a2, SG_BOB, SP_C_ALBUM, SG_ALBUM, SP_VIEW)==0 { t2=1 }
57 }
58 g_t(t2, "T2 the owner sees their own album and a stranger still does not" as *u8, fails)
59
60 // T3 a grant is what makes a stranger a viewer -- and only for the bits granted
61 let a3: *i64 = fresh()
62 sp_claim(a3, SG_ALICE, SP_C_ALBUM, SG_ALBUM)
63 let g3: i64 = sp_grant(a3, SG_ALICE, SG_BOB, SP_C_ALBUM, SG_ALBUM, SP_VIEW)
64 var t3: i64=0
65 if g3>0 {
66 if sp_may(a3, SG_BOB, SP_C_ALBUM, SG_ALBUM, SP_VIEW)==1 {
67 if sp_may(a3, SG_BOB, SP_C_ALBUM, SG_ALBUM, SP_ADD)==0 { t3=1 }
68 }
69 }
70 g_t(t3, "T3 a VIEW grant grants VIEW and nothing else (ADD stays refused)" as *u8, fails)
71
72 // T4 ATTACK: a viewer re-shares to a third party. VIEW must not carry the right to pass VIEW on.
73 let a4: *i64 = fresh()
74 sp_claim(a4, SG_ALICE, SP_C_ALBUM, SG_ALBUM)
75 sp_grant(a4, SG_ALICE, SG_BOB, SP_C_ALBUM, SG_ALBUM, SP_VIEW)
76 let escal: i64 = sp_grant(a4, SG_BOB, SG_CARA, SP_C_ALBUM, SG_ALBUM, SP_VIEW)
77 var t4: i64=0
78 if escal==SP_E_NOTOWNER { if sp_may(a4, SG_CARA, SP_C_ALBUM, SG_ALBUM, SP_VIEW)==0 { t4=1 } }
79 g_t(t4, "T4 ATTACK a viewer cannot re-share; no transitive escalation from VIEW" as *u8, fails)
80
81 // T5 ADMIN is the ONE bit that may re-share, and it is explicit
82 let a5: *i64 = fresh()
83 sp_claim(a5, SG_ALICE, SP_C_ALBUM, SG_ALBUM)
84 sp_grant(a5, SG_ALICE, SG_BOB, SP_C_ALBUM, SG_ALBUM, SP_VIEW+SP_ADMIN)
85 let ok5: i64 = sp_grant(a5, SG_BOB, SG_CARA, SP_C_ALBUM, SG_ALBUM, SP_VIEW)
86 var t5: i64=0
87 if ok5>0 { if sp_may(a5, SG_CARA, SP_C_ALBUM, SG_ALBUM, SP_VIEW)==1 { t5=1 } }
88 g_t(t5, "T5 an explicit ADMIN grant is the only way a non-owner re-shares" as *u8, fails)
89
90 // T6 revocation is total and immediate, and the plane still GREW (nothing was erased)
91 let a6: *i64 = fresh()
92 sp_claim(a6, SG_ALICE, SP_C_ALBUM, SG_ALBUM)
93 sp_grant(a6, SG_ALICE, SG_BOB, SP_C_ALBUM, SG_ALBUM, SP_VIEW+SP_ADD)
94 let before: i64 = sp_count(a6)
95 sp_revoke(a6, SG_ALICE, SG_BOB, SP_C_ALBUM, SG_ALBUM)
96 let after: i64 = sp_count(a6)
97 var t6: i64=0
98 if sp_may(a6, SG_BOB, SP_C_ALBUM, SG_ALBUM, SP_VIEW)==0 {
99 if sp_may(a6, SG_BOB, SP_C_ALBUM, SG_ALBUM, SP_ADD)==0 {
100 if after>before { t6=1 }
101 }
102 }
103 g_w(" rows before revoke=" as *u8); g_n(before); g_w(" after=" as *u8); g_n(after); g_w("\n" as *u8)
104 g_t(t6, "T6 revoke kills every capability AND appends rather than erasing (history survives)" as *u8, fails)
105
106 // T7 re-granting after a revoke works, and the LATEST record is the one that counts
107 let a7: *i64 = fresh()
108 sp_claim(a7, SG_ALICE, SP_C_ALBUM, SG_ALBUM)
109 sp_grant(a7, SG_ALICE, SG_BOB, SP_C_ALBUM, SG_ALBUM, SP_VIEW)
110 sp_revoke(a7, SG_ALICE, SG_BOB, SP_C_ALBUM, SG_ALBUM)
111 sp_grant(a7, SG_ALICE, SG_BOB, SP_C_ALBUM, SG_ALBUM, SP_VIEW)
112 g_t(sp_may(a7, SG_BOB, SP_C_ALBUM, SG_ALBUM, SP_VIEW)==1,
113 "T7 grant-revoke-grant resolves to the LAST thing that happened" as *u8, fails)
114
115 // T8 an owner cannot grant to themselves -- otherwise a later revoke could lock them out of their own
116 let a8: *i64 = fresh()
117 sp_claim(a8, SG_ALICE, SP_C_ALBUM, SG_ALBUM)
118 let self8: i64 = sp_grant(a8, SG_ALICE, SG_ALICE, SP_C_ALBUM, SG_ALBUM, SP_VIEW)
119 var t8: i64=0
120 if self8==SP_E_SELF { if sp_may(a8, SG_ALICE, SP_C_ALBUM, SG_ALBUM, SP_VIEW)==1 { t8=1 } }
121 g_t(t8, "T8 a self-grant is REFUSED and the owner still sees their own resource" as *u8, fails)
122
123 // T9 a claimed resource cannot be re-claimed by someone else (no silent ownership theft), and
124 // re-claiming your own is idempotent
125 let a9: *i64 = fresh()
126 sp_claim(a9, SG_ALICE, SP_C_ALBUM, SG_ALBUM)
127 let n9a: i64 = sp_count(a9)
128 let again: i64 = sp_claim(a9, SG_ALICE, SP_C_ALBUM, SG_ALBUM)
129 let n9b: i64 = sp_count(a9)
130 let steal: i64 = sp_claim(a9, SG_BOB, SP_C_ALBUM, SG_ALBUM)
131 var t9: i64=0
132 if steal==SP_E_NOTOWNER { if again==0 { if n9a==n9b { t9=1 } } }
133 g_t(t9, "T9 claim is idempotent for the owner and REFUSED for anyone else" as *u8, fails)
134
135 // T10 A GIFT MOVES OWNERSHIP. The giver stops being the owner -- this is what makes it a gift rather
136 // than a share, and it is the tooth that would catch a "gift" implemented as a copy.
137 let a10: *i64 = fresh()
138 sp_claim(a10, SG_ALICE, SP_C_GIFT, SG_CARD)
139 let gift: i64 = sp_gift(a10, SG_ALICE, SG_BOB, SP_C_GIFT, SG_CARD)
140 var t10: i64=0
141 if gift>0 {
142 if sp_owner_of(a10, SP_C_GIFT, SG_CARD)==SG_BOB {
143 if sp_may(a10, SG_BOB, SP_C_GIFT, SG_CARD, SP_VIEW)==1 {
144 if sp_may(a10, SG_ALICE, SP_C_GIFT, SG_CARD, SP_VIEW)==0 { t10=1 }
145 }
146 }
147 }
148 g_t(t10, "T10 a gift TRANSFERS ownership: the receiver gains it and the giver loses it" as *u8, fails)
149
150 // T11 provenance survives the whole chain: alice -> bob -> cara, all three names recoverable
151 let a11: *i64 = fresh()
152 sp_claim(a11, SG_ALICE, SP_C_GIFT, SG_CARD)
153 sp_gift(a11, SG_ALICE, SG_BOB, SP_C_GIFT, SG_CARD)
154 sp_gift(a11, SG_BOB, SG_CARA, SP_C_GIFT, SG_CARD)
155 let plen: i64 = sp_provenance_len(a11, SP_C_GIFT, SG_CARD)
156 var t11: i64=0
157 if plen==3 {
158 if sp_provenance_at(a11,SP_C_GIFT,SG_CARD,0)==SG_ALICE {
159 if sp_provenance_at(a11,SP_C_GIFT,SG_CARD,1)==SG_BOB {
160 if sp_provenance_at(a11,SP_C_GIFT,SG_CARD,2)==SG_CARA { t11=1 }
161 }
162 }
163 }
164 g_w(" provenance hops=" as *u8); g_n(plen); g_w("\n" as *u8)
165 g_t(t11, "T11 the gift chain is fully recoverable (alice -> bob -> cara), nothing rewritten" as *u8, fails)
166
167 // T12 ATTACK: a former owner gifts something they already gave away
168 let a12: *i64 = fresh()
169 sp_claim(a12, SG_ALICE, SP_C_GIFT, SG_CARD)
170 sp_gift(a12, SG_ALICE, SG_BOB, SP_C_GIFT, SG_CARD)
171 let regift: i64 = sp_gift(a12, SG_ALICE, SG_CARA, SP_C_GIFT, SG_CARD)
172 var t12: i64=0
173 if regift==SP_E_NOTOWNER { if sp_owner_of(a12, SP_C_GIFT, SG_CARD)==SG_BOB { t12=1 } }
174 g_t(t12, "T12 ATTACK a former owner cannot re-gift what they already gave away" as *u8, fails)
175
176 // T13 the WHO CAN SEE THIS panel is computed from the log, and a revoked viewer disappears from it
177 let a13: *i64 = fresh()
178 sp_claim(a13, SG_ALICE, SP_C_ALBUM, SG_ALBUM)
179 sp_grant(a13, SG_ALICE, SG_BOB, SP_C_ALBUM, SG_ALBUM, SP_VIEW)
180 sp_grant(a13, SG_ALICE, SG_CARA, SP_C_ALBUM, SG_ALBUM, SP_VIEW)
181 sp_grant(a13, SG_ALICE, SG_DAN, SP_C_ALBUM, SG_ALBUM, SP_VIEW)
182 sp_revoke(a13, SG_ALICE, SG_CARA, SP_C_ALBUM, SG_ALBUM)
183 let seen: *i64 = sys_mmap(8*SG_CAP) as *i64
184 let nv: i64 = sp_viewers(a13, SP_C_ALBUM, SG_ALBUM, seen, SG_CAP)
185 var has_cara: i64 = 0
186 var i: i64 = 0
187 while i<nv { if seen[i]==SG_CARA { has_cara=1 } i=i+1 }
188 var t13: i64=0
189 if nv==2 { if has_cara==0 { t13=1 } }
190 g_w(" live viewers=" as *u8); g_n(nv); g_w(" (bob + dan; cara was revoked)\n" as *u8)
191 g_t(t13, "T13 the viewer list is recomputed from the log so a revoked person vanishes from it" as *u8, fails)
192
193 // T14 classes are isolated: a grant on the album must not leak into the contact card
194 let a14: *i64 = fresh()
195 sp_claim(a14, SG_ALICE, SP_C_ALBUM, SG_ALBUM)
196 sp_claim(a14, SG_ALICE, SP_C_CONTACT, SG_ALBUM)
197 sp_grant(a14, SG_ALICE, SG_BOB, SP_C_ALBUM, SG_ALBUM, SP_VIEW)
198 var t14: i64=0
199 if sp_may(a14, SG_BOB, SP_C_ALBUM, SG_ALBUM, SP_VIEW)==1 {
200 if sp_may(a14, SG_BOB, SP_C_CONTACT, SG_ALBUM, SP_VIEW)==0 { t14=1 }
201 }
202 g_t(t14, "T14 the same id in a different class is a different resource (album grant does not leak to the contact card)" as *u8, fails)
203
204 // T15 BOUNDED AND LOUD: past capacity the plane REFUSES instead of silently dropping the row. A
205 // silently dropped REVOKE is access that should have ended and did not.
206 let small: *i64 = sys_mmap(8*sp_slots_needed(2)) as *i64
207 sp_init(small, 2)
208 sp_claim(small, SG_ALICE, SP_C_ALBUM, SG_ALBUM)
209 let fill: i64 = sp_grant(small, SG_ALICE, SG_BOB, SP_C_ALBUM, SG_ALBUM, SP_VIEW)
210 let over: i64 = sp_grant(small, SG_ALICE, SG_CARA, SP_C_ALBUM, SG_ALBUM, SP_VIEW)
211 var t15: i64=0
212 if fill>0 { if over==SP_E_FULL { if sp_may(small, SG_CARA, SP_C_ALBUM, SG_ALBUM, SP_VIEW)==0 { t15=1 } } }
213 g_t(t15, "T15 at capacity the plane refuses loudly and the refused grant did NOT take effect" as *u8, fails)
214
215 // T16 NEG-CONTROL on the gate itself: prove sp_may can actually answer NO for a live viewer asking for
216 // a bit they were never given. If this tooth ever passes trivially, T3's ADD check proves nothing.
217 let a16: *i64 = fresh()
218 sp_claim(a16, SG_ALICE, SP_C_ALBUM, SG_ALBUM)
219 sp_grant(a16, SG_ALICE, SG_BOB, SP_C_ALBUM, SG_ALBUM, SP_ADD)
220 var t16: i64=0
221 if sp_may(a16, SG_BOB, SP_C_ALBUM, SG_ALBUM, SP_ADD)==1 {
222 if sp_may(a16, SG_BOB, SP_C_ALBUM, SG_ALBUM, SP_ADMIN)==0 {
223 if sp_may(a16, SG_BOB, SP_C_ALBUM, SG_ALBUM, SP_VIEW)==0 { t16=1 }
224 }
225 }
226 g_t(t16, "T16 NEG-CONTROL bits are independent: ADD alone grants neither VIEW nor ADMIN" as *u8, fails)
227
228 // T17 COMPOSITE REQUESTS. Found by reading the first GREEN run rather than trusting it: the original
229 // check divided by `want` and read the low bit, which is only meaningful for a single power of two. A
230 // caller asking "may they VIEW AND ADD" got an arithmetic accident. On a permission check that is an
231 // access-control bug, so this tooth pins the subset rule: holding VIEW+ADD answers yes to VIEW, to ADD
232 // and to VIEW+ADD, but NO to VIEW+ADMIN -- a bit that was never granted cannot be smuggled in beside
233 // one that was.
234 let a17: *i64 = fresh()
235 sp_claim(a17, SG_ALICE, SP_C_ALBUM, SG_ALBUM)
236 sp_grant(a17, SG_ALICE, SG_BOB, SP_C_ALBUM, SG_ALBUM, SP_VIEW+SP_ADD)
237 var t17: i64=0
238 if sp_may(a17, SG_BOB, SP_C_ALBUM, SG_ALBUM, SP_VIEW)==1 {
239 if sp_may(a17, SG_BOB, SP_C_ALBUM, SG_ALBUM, SP_ADD)==1 {
240 if sp_may(a17, SG_BOB, SP_C_ALBUM, SG_ALBUM, SP_VIEW+SP_ADD)==1 {
241 if sp_may(a17, SG_BOB, SP_C_ALBUM, SG_ALBUM, SP_VIEW+SP_ADMIN)==0 {
242 if sp_may(a17, SG_BOB, SP_C_ALBUM, SG_ALBUM, SP_CAPMAX)==0 { t17=1 }
243 }
244 }
245 }
246 }
247 g_t(t17, "T17 a COMPOSITE capability request is a subset test: VIEW+ADD yes, VIEW+ADMIN no" as *u8, fails)
248
249 // T18 an out-of-range capability request is refused rather than wrapped into something meaningful
250 let a18: *i64 = fresh()
251 sp_claim(a18, SG_ALICE, SP_C_ALBUM, SG_ALBUM)
252 sp_grant(a18, SG_ALICE, SG_BOB, SP_C_ALBUM, SG_ALBUM, SP_CAPMAX)
253 var t18: i64=0
254 if sp_may(a18, SG_BOB, SP_C_ALBUM, SG_ALBUM, SP_CAPMAX+1)==0 {
255 if sp_may(a18, SG_BOB, SP_C_ALBUM, SG_ALBUM, 0-1)==0 {
256 if sp_may(a18, SG_BOB, SP_C_ALBUM, SG_ALBUM, SP_CAPMAX)==1 { t18=1 }
257 }
258 }
259 g_t(t18, "T18 an out-of-range or negative capability request is refused, not wrapped" as *u8, fails)
260
261 // T19 THE EXACT ESCALATION THE OLD ARITHMETIC ALLOWED. held = VIEW+ADMIN (5), want = VIEW+ADD (3).
262 // The divide-and-read-low-bit version computed 5/3 = 1, low bit 1, and answered YES -- handing ADD to
263 // somebody who was never granted ADD. This is not a hypothetical: it is the bug that was in the file
264 // when the gate first went 16/16 green, which is exactly why a green run is not evidence of
265 // correctness. If this tooth ever regresses, that escalation is back.
266 let a19: *i64 = fresh()
267 sp_claim(a19, SG_ALICE, SP_C_ALBUM, SG_ALBUM)
268 sp_grant(a19, SG_ALICE, SG_BOB, SP_C_ALBUM, SG_ALBUM, SP_VIEW+SP_ADMIN)
269 var t19: i64=0
270 if sp_may(a19, SG_BOB, SP_C_ALBUM, SG_ALBUM, SP_VIEW+SP_ADD)==0 {
271 if sp_may(a19, SG_BOB, SP_C_ALBUM, SG_ALBUM, SP_ADD)==0 {
272 if sp_may(a19, SG_BOB, SP_C_ALBUM, SG_ALBUM, SP_VIEW+SP_ADMIN)==1 { t19=1 }
273 }
274 }
275 g_t(t19, "T19 REGRESSION holding VIEW+ADMIN must NOT satisfy a VIEW+ADD request (the escalation the old bit test allowed)" as *u8, fails)
276
277 g_w(" fails=" as *u8); g_n(fails[0]); g_w("\n" as *u8)
278 if fails[0]==0 {
279 g_w("VERDICT: verdict=GREEN (19/19 -- deny by default, no escalation, revocation total, gifts move ownership, history intact, composite requests are subset tests)\n" as *u8)
280 sys_exit(0)
281 }
282 g_w("VERDICT: RED\n" as *u8)
283 sys_exit(1)
284 return 1
285}