1	# Pure authorization policies: deny-overrides, default deny, intersection, and fail-closed missing context.
2	import Base
3	
4	# What a policy may ask about one request. A `None` field is missing information:
5	# the caller did not authenticate a subject, load roles, or find the owner.
6	type Request is Data:
7	  Request{subject: Maybe<&2, String>, roles: Maybe<&2, List<&2, String>>, owner: Maybe<&2, String>, action: String, resource: String}
8	
9	# A target answers Yes, No, or Unknown when it needs a missing field.
10	type Tri is Data:
11	  Yes{}
12	  No{}
13	  Unknown{}
14	
15	type Target is Data:
16	  Everyone{}
17	  Nobody{}
18	  Action{name: String}
19	  Resource{name: String}
20	  Subject{name: String}
21	  Role{name: String}
22	  Owner{}
23	  AllOf{a: Target, b: Target}
24	
25	# Abstain means that no rule applies. `granted` treats it as a denial.
26	type Decision is Data:
27	  Allow{}
28	  Deny{}
29	  Abstain{}
30	
31	type Policy is Data:
32	  Permit{target: Target}
33	  Forbid{target: Target}
34	  DenyOverrides{a: Policy, b: Policy}
35	  Intersect{a: Policy, b: Policy}
36	
37	def tri(b: Bool) -> Tri:
38	  match b:
39	    case True{}:
40	      Yes{}
41	    case False{}:
42	      No{}
43	
44	def has(+name: String, xs: List<&2, String>) -> Bool:
45	  match xs:
46	    case Nil{}:
47	      False{}
48	    case x <> rest:
49	      String.eq(x, name) || has(name, rest)
50	
51	def subject.is(name: String, s: Maybe<&2, String>) -> Tri:
52	  match s:
53	    case None{}:
54	      Unknown{}
55	    case Some{x}:
56	      tri(String.eq(x, name))
57	
58	def role.is(name: String, r: Maybe<&2, List<&2, String>>) -> Tri:
59	  match r:
60	    case None{}:
61	      Unknown{}
62	    case Some{xs}:
63	      tri(has(name, xs))
64	
65	def owner.is(x: String, o: Maybe<&2, String>) -> Tri:
66	  match o:
67	    case None{}:
68	      Unknown{}
69	    case Some{y}:
70	      tri(String.eq(x, y))
71	
72	def owner.of(s: Maybe<&2, String>, o: Maybe<&2, String>) -> Tri:
73	  match s:
74	    case None{}:
75	      Unknown{}
76	    case Some{x}:
77	      owner.is(x, o)
78	
79	# Kleene conjunction: No wins, then Unknown.
80	def all(a: Tri, b: Tri) -> Tri:
81	  match a:
82	    case No{}:
83	      No{}
84	    case Yes{}:
85	      b
86	    case Unknown{}:
87	      match b:
88	        case No{}:
89	          No{}
90	        case Yes{}:
91	          Unknown{}
92	        case Unknown{}:
93	          Unknown{}
94	
95	def matches(t: Target, +req: Request) -> Tri:
96	  match t:
97	    case Everyone{}:
98	      Yes{}
99	    case Nobody{}:
100	      No{}
101	    case Action{name}:
102	      Request{s, r, o, action, resource} = req
103	      tri(String.eq(action, name))
104	    case Resource{name}:
105	      Request{s, r, o, action, resource} = req
106	      tri(String.eq(resource, name))
107	    case Subject{name}:
108	      Request{s, r, o, action, resource} = req
109	      subject.is(name, s)
110	    case Role{name}:
111	      Request{s, r, o, action, resource} = req
112	      role.is(name, r)
113	    case Owner{}:
114	      Request{s, r, o, action, resource} = req
115	      owner.of(s, o)
116	    case AllOf{a, b}:
117	      all(matches(a, req), matches(b, req))
118	
119	# A permit grants only on Yes. Unknown cannot grant.
120	def permit(m: Tri) -> Decision:
121	  match m:
122	    case Yes{}:
123	      Allow{}
124	    case No{}:
125	      Abstain{}
126	    case Unknown{}:
127	      Abstain{}
128	
129	# A forbid denies on Yes and on Unknown: it fails closed.
130	def forbid(m: Tri) -> Decision:
131	  match m:
132	    case Yes{}:
133	      Deny{}
134	    case No{}:
135	      Abstain{}
136	    case Unknown{}:
137	      Deny{}
138	
139	# Deny wins, then Allow, then Abstain.
140	def deny_overrides(a: Decision, b: Decision) -> Decision:
141	  match a:
142	    case Deny{}:
143	      Deny{}
144	    case Abstain{}:
145	      b
146	    case Allow{}:
147	      match b:
148	        case Deny{}:
149	          Deny{}
150	        case Allow{}:
151	          Allow{}
152	        case Abstain{}:
153	          Allow{}
154	
155	# Allow only when both allow. Deny wins over Abstain.
156	def intersect(a: Decision, b: Decision) -> Decision:
157	  match a:
158	    case Deny{}:
159	      Deny{}
160	    case Allow{}:
161	      b
162	    case Abstain{}:
163	      match b:
164	        case Deny{}:
165	          Deny{}
166	        case Allow{}:
167	          Abstain{}
168	        case Abstain{}:
169	          Abstain{}
170	
171	def decide(p: Policy, +req: Request) -> Decision:
172	  match p:
173	    case Permit{t}:
174	      permit(matches(t, req))
175	    case Forbid{t}:
176	      forbid(matches(t, req))
177	    case DenyOverrides{a, b}:
178	      deny_overrides(decide(a, req), decide(b, req))
179	    case Intersect{a, b}:
180	      intersect(decide(a, req), decide(b, req))
181	
182	def allowed(d: Decision) -> Bool:
183	  match d:
184	    case Allow{}:
185	      True{}
186	    case Deny{}:
187	      False{}
188	    case Abstain{}:
189	      False{}
190	
191	# Default deny: only Allow grants.
192	def granted(p: Policy, +req: Request) -> Bool:
193	  allowed(decide(p, req))