1	# bend-osdev-apparmor: dbus rules (apparmor.d(5), "DBUS RULE", "DBus
2	# rules"): message rules (path, interface, member, peer=(name label)),
3	# service rules (name) and eavesdrop rules (bus only), each with an
4	# optional bus=. Permission bits: send 0, receive 1, bind 2, eavesdrop 3.
5	# r and read are receive, w and write send, rw both. bind is not allowed in
6	# message rules, send and receive not in service rules, eavesdrop only with
7	# a bus condition. With no access list a message rule implies send and
8	# receive, a service rule bind, and a rule with neither kind of condition
9	# all four.
10	import Base
11	import ./text.bend as X
12	import ./glob.bend as G
13	import ./perm.bend as P
14	import ./token.bend as T
15	import ./error.bend as E
16	import ./rule.bend as R
17	
18	type AaDbusRule is Data:
19	  AaDbusRule{qual: P.AaQual, perms: P.AaPerms, bus: Maybe<&2, G.AaGlob>, path: Maybe<&2, G.AaGlob>, iface: Maybe<&2, G.AaGlob>, member: Maybe<&2, G.AaGlob>, name: Maybe<&2, G.AaGlob>, peer_name: Maybe<&2, G.AaGlob>, peer_label: Maybe<&2, G.AaGlob>}
20	
21	# a dbus operation: req (send, receive, bind, eavesdrop), the bus (system,
22	# session, ...), the object path, interface and member, the name bound (for
23	# bind), and the peer's bus name and profile name
24	type AaDbusQuery is Data:
25	  AaDbusQuery{req: P.AaPerms, bus: List<&2, U32>, path: List<&2, U32>, iface: List<&2, U32>, member: List<&2, U32>, name: List<&2, U32>, peer_name: List<&2, U32>, peer_label: List<&2, U32>}
26	
27	def AaDbus.send() -> Nat:
28	  0n
29	
30	def AaDbus.receive() -> Nat:
31	  1n
32	
33	def AaDbus.bind() -> Nat:
34	  2n
35	
36	def AaDbus.eavesdrop() -> Nat:
37	  3n
38	
39	def AaDbus.access(+w: List<&2, U32>) -> Maybe<&2, P.AaPerms>:
40	  Bool.pick(Maybe<&2, P.AaPerms>, Bool.or(X.AaText.is(w, "send"), Bool.or(X.AaText.is(w, "w"), X.AaText.is(w, "write"))), Some{P.AaPerms.bit(0n)}, Bool.pick(Maybe<&2, P.AaPerms>, Bool.or(X.AaText.is(w, "receive"), Bool.or(X.AaText.is(w, "r"), X.AaText.is(w, "read"))), Some{P.AaPerms.bit(1n)}, Bool.pick(Maybe<&2, P.AaPerms>, X.AaText.is(w, "bind"), Some{P.AaPerms.bit(2n)}, Bool.pick(Maybe<&2, P.AaPerms>, X.AaText.is(w, "eavesdrop"), Some{P.AaPerms.bit(3n)}, Bool.pick(Maybe<&2, P.AaPerms>, X.AaText.is(w, "rw"), Some{P.AaPerms.of_bits([True{}, True{}])}, None{})))))
41	
42	# The builder: one slot per condition, each set at most once
43	type AaDbB is Data:
44	  AaDbB{perms: Maybe<&2, P.AaPerms>, slots: List<&2, Maybe<&2, G.AaGlob>>}
45	
46	def AaDbB.empty() -> AaDbB:
47	  AaDbB{None{}, [None{}, None{}, None{}, None{}, None{}, None{}, None{}]}
48	
49	# the slot of a condition key: bus 0, path 1, interface 2, member 3, name 4
50	def AaDbus.slot(+k: List<&2, U32>) -> Maybe<&2, Nat>:
51	  Bool.pick(Maybe<&2, Nat>, X.AaText.is(k, "bus"), Some{0n}, Bool.pick(Maybe<&2, Nat>, X.AaText.is(k, "path"), Some{1n}, Bool.pick(Maybe<&2, Nat>, X.AaText.is(k, "interface"), Some{2n}, Bool.pick(Maybe<&2, Nat>, X.AaText.is(k, "member"), Some{3n}, Bool.pick(Maybe<&2, Nat>, X.AaText.is(k, "name"), Some{4n}, None{})))))
52	
53	# a peer condition's key: name 5, label 6
54	def AaDbus.peer_slot(+k: List<&2, U32>) -> Maybe<&2, Nat>:
55	  Bool.pick(Maybe<&2, Nat>, X.AaText.is(k, "name"), Some{5n}, Bool.pick(Maybe<&2, Nat>, X.AaText.is(k, "label"), Some{6n}, None{}))
56	
57	def AaDbus.set.cons(x: Maybe<&2, G.AaGlob>, r: Maybe<&2, List<&2, Maybe<&2, G.AaGlob>>>) -> Maybe<&2, List<&2, Maybe<&2, G.AaGlob>>>:
58	  match r:
59	    case None{}:
60	      None{}
61	    case Some{xs}:
62	      Some{Con{x, xs}}
63	
64	# slot i of the list set to g; None if it is set already
65	def AaDbus.set(n: Nat, xs: List<&2, Maybe<&2, G.AaGlob>>, g: G.AaGlob) -> Maybe<&2, List<&2, Maybe<&2, G.AaGlob>>>:
66	  match n:
67	    case 0n:
68	      match xs:
69	        case Nil{}:
70	          None{}
71	        case Con{x, rest}:
72	          match x:
73	            case None{}:
74	              Some{Con{Some{g}, rest}}
75	            case Some{h}:
76	              None{}
77	    case 1n+m:
78	      match xs:
79	        case Nil{}:
80	          None{}
81	        case Con{x, rest}:
82	          AaDbus.set.cons(x, AaDbus.set(m, rest, g))
83	
84	def AaDbB.put.go(r: Maybe<&2, List<&2, Maybe<&2, G.AaGlob>>>, p: Maybe<&2, P.AaPerms>, src: E.AaSrc) -> Result<&2, &2, E.AaError, AaDbB>:
85	  match r:
86	    case None{}:
87	      Fail{E.AaSrc.syntax(src)}
88	    case Some{xs}:
89	      Done{AaDbB{p, xs}}
90	
91	def AaDbB.put(m: Maybe<&2, Nat>, b: AaDbB, g: G.AaGlob, src: E.AaSrc) -> Result<&2, &2, E.AaError, AaDbB>:
92	  match m:
93	    case None{}:
94	      Fail{E.AaSrc.syntax(src)}
95	    case Some{n}:
96	      match b:
97	        case AaDbB{p, xs}:
98	          AaDbB.put.go(AaDbus.set(n, xs, g), p, src)
99	
100	def AaDbB.perms(m: Maybe<&2, P.AaPerms>, b: AaDbB, src: E.AaSrc) -> Result<&2, &2, E.AaError, AaDbB>:
101	  match m:
102	    case None{}:
103	      Fail{E.AaSrc.syntax(src)}
104	    case Some{p}:
105	      match b:
106	        case AaDbB{bp, xs}:
107	          match bp:
108	            case None{}:
109	              Done{AaDbB{Some{p}, xs}}
110	            case Some{q}:
111	              Done{AaDbB{Some{P.AaPerms.union(q, p)}, xs}}
112	
113	def AaDbB.access_list(xs: List<&2, T.AaTerm>, b: AaDbB, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaDbB>:
114	  match xs:
115	    case Nil{}:
116	      Done{b}
117	    case Con{x, rest}:
118	      match x:
119	        case T.AaTmWord{w}:
120	          do Result<&2, &2, E.AaError, AaDbB>:
121	            b2 : AaDbB <- AaDbB.perms(AaDbus.access(w), b, src)
122	            AaDbB.access_list(rest, b2, src)
123	        case _:
124	          Fail{E.AaSrc.syntax(src)}
125	
126	def AaDbB.cond.one(m: Maybe<&2, Nat>, v: T.AaTerm, b: AaDbB, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaDbB>:
127	  do Result<&2, &2, E.AaError, AaDbB>:
128	    g : G.AaGlob <- R.AaRule.value_glob(v, src)
129	    AaDbB.put(m, b, g, src)
130	
131	# the conditions inside peer=( ... )
132	def AaDbB.peer(xs: List<&2, T.AaTerm>, b: AaDbB, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaDbB>:
133	  match xs:
134	    case Nil{}:
135	      Done{b}
136	    case Con{x, rest}:
137	      match x:
138	        case T.AaTmCond{k, v}:
139	          do Result<&2, &2, E.AaError, AaDbB>:
140	            b2 : AaDbB <- AaDbB.cond.one(AaDbus.peer_slot(k), v, b, src)
141	            AaDbB.peer(rest, b2, src)
142	        case _:
143	          Fail{E.AaSrc.syntax(src)}
144	
145	def AaDbB.cond.peer(v: T.AaTerm, b: AaDbB, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaDbB>:
146	  match v:
147	    case T.AaTmList{xs}:
148	      AaDbB.peer(xs, b, src)
149	    case _:
150	      Fail{E.AaSrc.syntax(src)}
151	
152	def AaDbB.cond(+k: List<&2, U32>, +v: T.AaTerm, +b: AaDbB, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaDbB>:
153	  Bool.pick(Result<&2, &2, E.AaError, AaDbB>, X.AaText.is(k, "peer"), AaDbB.cond.peer(v, b, src), AaDbB.cond.one(AaDbus.slot(k), v, b, src))
154	
155	def AaDbB.step(t: T.AaTerm, b: AaDbB, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaDbB>:
156	  match t:
157	    case T.AaTmWord{w}:
158	      AaDbB.perms(AaDbus.access(w), b, src)
159	    case T.AaTmList{xs}:
160	      AaDbB.access_list(xs, b, src)
161	    case T.AaTmCond{k, v}:
162	      AaDbB.cond(k, v, b, src)
163	    case _:
164	      Fail{E.AaSrc.syntax(src)}
165	
166	def AaDbB.run(ts: List<&2, T.AaTerm>, b: AaDbB, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaDbB>:
167	  match ts:
168	    case Nil{}:
169	      Done{b}
170	    case Con{t, rest}:
171	      do Result<&2, &2, E.AaError, AaDbB>:
172	        b2 : AaDbB <- AaDbB.step(t, b, src)
173	        AaDbB.run(rest, b2, src)
174	
175	def AaDbus.is_some(m: Maybe<&2, G.AaGlob>) -> Bool:
176	  match m:
177	    case None{}:
178	      False{}
179	    case Some{g}:
180	      True{}
181	
182	def AaDbus.nth(n: Nat, xs: List<&2, Maybe<&2, G.AaGlob>>) -> Maybe<&2, G.AaGlob>:
183	  match n:
184	    case 0n:
185	      match xs:
186	        case Nil{}:
187	          None{}
188	        case Con{x, rest}:
189	          x
190	    case 1n+m:
191	      match xs:
192	        case Nil{}:
193	          None{}
194	        case Con{x, rest}:
195	          AaDbus.nth(m, rest)
196	
197	# the permissions given, checked against the kind of rule, or the implied ones
198	def AaDbus.perms(m: Maybe<&2, P.AaPerms>, +msg: Bool, +svc: Bool, src: E.AaSrc) -> Result<&2, &2, E.AaError, P.AaPerms>:
199	  match m:
200	    case None{}:
201	      Done{Bool.pick(P.AaPerms, msg, P.AaPerms.of_bits([True{}, True{}]), Bool.pick(P.AaPerms, svc, P.AaPerms.bit(2n), P.AaPerms.of_bits([True{}, True{}, True{}, True{}])))}
202	    case Some{+p}:
203	      +bad = Bool.or(Bool.and(msg, svc), Bool.or(Bool.and(msg, P.AaPerms.has(p, 2n)), Bool.or(Bool.and(svc, Bool.or(P.AaPerms.has(p, 0n), P.AaPerms.has(p, 1n))), Bool.and(Bool.or(msg, svc), P.AaPerms.has(p, 3n)))))
204	      Bool.pick(Result<&2, &2, E.AaError, P.AaPerms>, bad, Fail{E.AaSrc.syntax(src)}, Done{p})
205	
206	def AaDbB.finish(q: P.AaQual, b: AaDbB, src: E.AaSrc) -> Result<&2, &2, E.AaError, AaDbusRule>:
207	  match b:
208	    case AaDbB{p, +xs}:
209	      +msg = Bool.or(AaDbus.is_some(AaDbus.nth(1n, xs)), Bool.or(AaDbus.is_some(AaDbus.nth(2n, xs)), Bool.or(AaDbus.is_some(AaDbus.nth(3n, xs)), Bool.or(AaDbus.is_some(AaDbus.nth(5n, xs)), AaDbus.is_some(AaDbus.nth(6n, xs))))))
210	      +svc = AaDbus.is_some(AaDbus.nth(4n, xs))
211	      do Result<&2, &2, E.AaError, AaDbusRule>:
212	        ps : P.AaPerms <- AaDbus.perms(p, msg, svc, src)
213	        return AaDbusRule{q, ps, AaDbus.nth(0n, xs), AaDbus.nth(1n, xs), AaDbus.nth(2n, xs), AaDbus.nth(3n, xs), AaDbus.nth(4n, xs), AaDbus.nth(5n, xs), AaDbus.nth(6n, xs)}
214	
215	def AaDbus.parse.q(r: Result<&2, &2, E.AaError, P.AaQual>, ts: List<&2, T.AaTerm>, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaDbusRule>:
216	  match r:
217	    case Fail{e}:
218	      Fail{e}
219	    case Done{q}:
220	      do Result<&2, &2, E.AaError, AaDbusRule>:
221	        b : AaDbB <- AaDbB.run(ts, AaDbB.empty(), src)
222	        AaDbB.finish(q, b, src)
223	
224	# the terms after `dbus`
225	def AaDbus.parse(ts: List<&2, T.AaTerm>, q: P.AaQual, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaDbusRule>:
226	  AaDbus.parse.q(R.AaRule.no_owner(q, src), ts, src)
227	
228	# Matching
229	
230	def AaDbusRule.matches(r: AaDbusRule, q: AaDbusQuery) -> Bool:
231	  match r:
232	    case AaDbusRule{qu, p, bus, path, iface, member, name, pn, pl}:
233	      match q:
234	        case AaDbusQuery{req, qbus, qpath, qiface, qmember, qname, qpn, qpl}:
235	          Bool.and(R.AaRule.opt_match(bus, qbus), Bool.and(R.AaRule.opt_match(path, qpath), Bool.and(R.AaRule.opt_match(iface, qiface), Bool.and(R.AaRule.opt_match(member, qmember), Bool.and(R.AaRule.opt_match(name, qname), Bool.and(R.AaRule.opt_match(pn, qpn), R.AaRule.opt_match(pl, qpl)))))))
236	
237	def AaDbusRule.matching.go(hit: Bool, r: AaDbusRule, rest: List<&2, AaDbusRule>) -> List<&2, AaDbusRule>:
238	  match hit:
239	    case True{}:
240	      Con{r, rest}
241	    case False{}:
242	      rest
243	
244	def AaDbusRule.matching(rs: List<&2, AaDbusRule>, +q: AaDbusQuery) -> List<&2, AaDbusRule>:
245	  match rs:
246	    case Nil{}:
247	      Nil{}
248	    case Con{+r, t}:
249	      AaDbusRule.matching.go(AaDbusRule.matches(r, q), r, AaDbusRule.matching(t, q))
250	
251	def AaDbusRule.grants.of(rs: List<&2, AaDbusRule>) -> List<&2, P.AaGrant>:
252	  match rs:
253	    case Nil{}:
254	      Nil{}
255	    case Con{r, t}:
256	      match r:
257	        case AaDbusRule{qu, p, bus, path, iface, member, name, pn, pl}:
258	          Con{P.AaGrant.of(qu, p), AaDbusRule.grants.of(t)}
259	
260	def AaDbusRule.grants(rs: List<&2, AaDbusRule>, +q: AaDbusQuery) -> List<&2, P.AaGrant>:
261	  AaDbusRule.grants.of(AaDbusRule.matching(rs, q))
262	
263	def AaDbusRule.append(xs: List<&2, AaDbusRule>, ys: List<&2, AaDbusRule>) -> List<&2, AaDbusRule>:
264	  match xs:
265	    case Nil{}:
266	      ys
267	    case Con{h, t}:
268	      Con{h, AaDbusRule.append(t, ys)}
269	
270	def AaDbusQuery.req(q: AaDbusQuery) -> P.AaPerms:
271	  match q:
272	    case AaDbusQuery{r, b, p, i, m, n, pn, pl}:
273	      r