rule_dbus.bend

bend-osdev-apparmor@0.1.0.0 · 273 lines · 36 definitions

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.
10import Base
11import bend-osdev-apparmor@0.1.0.0/text.bend as X
12import bend-osdev-apparmor@0.1.0.0/glob.bend as G
13import bend-osdev-apparmor@0.1.0.0/perm.bend as P
14import bend-osdev-apparmor@0.1.0.0/token.bend as T
15import bend-osdev-apparmor@0.1.0.0/error.bend as E
16import bend-osdev-apparmor@0.1.0.0/rule.bend as R
17
18type 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
24type 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
27def AaDbus.send() -> Nat:
28  0n
29
30def AaDbus.receive() -> Nat:
31  1n
32
33def AaDbus.bind() -> Nat:
34  2n
35
36def AaDbus.eavesdrop() -> Nat:
37  3n
38
39def 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
43type AaDbB is Data:
44  AaDbB{perms: Maybe<&2, P.AaPerms>, slots: List<&2, Maybe<&2, G.AaGlob>>}
45
46def 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
50def 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
54def 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
57def 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
65def 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
84def 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
91def 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
100def 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
113def 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
126def 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=( ... )
132def 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
145def 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
152def 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
155def 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
166def 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
175def AaDbus.is_some(m: Maybe<&2, G.AaGlob>) -> Bool:
176  match m:
177    case None{}:
178      False{}
179    case Some{g}:
180      True{}
181
182def 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
198def 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
206def 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
215def 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`
225def 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
230def 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
237def 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
244def 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
251def 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
260def AaDbusRule.grants(rs: List<&2, AaDbusRule>, +q: AaDbusQuery) -> List<&2, P.AaGrant>:
261  AaDbusRule.grants.of(AaDbusRule.matching(rs, q))
262
263def 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
270def AaDbusQuery.req(q: AaDbusQuery) -> P.AaPerms:
271  match q:
272    case AaDbusQuery{r, b, p, i, m, n, pn, pl}:
273      r