transitions.bend

bend-osdev-apparmor@0.1.0.0 · 331 lines · 39 definitions

1# bend-osdev-apparmor: exec transitions (apparmor.d(5), "Access Modes",
2# "Directed profile transitions", "Attachment Conditionals").
3#
4# When a confined task executes a path, the profile must grant x on it; the
5# exec mode of the matching allow rules then says where the task goes: ix
6# stays in the profile, ux and Ux leave confinement, px and Px move to the
7# profile named after -> or else to the profile whose attachment best
8# matches the path, cx and Cx do the same among the profile's children; the
9# i and u forms fall back to ix and ux (Ux for PUx and CUx) when no profile
10# is found, and the plain forms fail. Upper case scrubs the environment.
11#
12# Where several allow rules with exec modes match, a rule whose pattern is
13# literal (no wildcard, no braces) decides over pattern rules, and the rules
14# that decide must agree (apparmor_parser 4.0.1 rejects a profile otherwise
15# when it can tell; see the README, "Experiments"); disagreement is a
16# failure here. Among attachments, a literal one wins, then the longest
17# literal prefix; a tie fails ("If the heuristic can not determine a winner
18# between multiple matches the exec will be denied").
19#
20# A task in complain mode whose profile grants no x, or whose x comes from
21# no exec rule (default_allow), stays in its profile. A profile in
22# unconfined mode executes as an unconfined task: the profile whose
23# attachment matches, else unconfined.
24import Base
25import bend-osdev-apparmor@0.1.0.0/text.bend as X
26import bend-osdev-apparmor@0.1.0.0/glob.bend as G
27import bend-osdev-apparmor@0.1.0.0/perm.bend as P
28import bend-osdev-apparmor@0.1.0.0/options.bend as O
29import bend-osdev-apparmor@0.1.0.0/profile.bend as PR
30import bend-osdev-apparmor@0.1.0.0/rule_file.bend as F
31import bend-osdev-apparmor@0.1.0.0/eval.bend as V
32
33type AaTarget is Data:
34  # the same profile
35  AaTStay{}
36  # the profile with this full name
37  AaTProfile{name: List<&2, U32>}
38  # no profile
39  AaTUnconfined{}
40
41type AaExecWhy is Data:
42  # the profile does not grant x on the path (the decision says how it refused)
43  AaExecDenied{decision: V.AaDecision}
44  # px or cx found no profile, and there is no fallback
45  AaExecNoProfile{}
46  # the matching rules give different exec modes or targets
47  AaExecConflict{}
48  # two attachments match equally well
49  AaExecAmbiguous{}
50  # the executing profile is not in the policy
51  AaExecUnknown{}
52
53type AaExecResult is Data:
54  AaExecOk{target: AaTarget, scrub: Bool, decision: V.AaDecision}
55  AaExecErr{why: AaExecWhy}
56
57def AaExecResult.ok(r: AaExecResult) -> Bool:
58  match r:
59    case AaExecOk{t, s, d}:
60      True{}
61    case AaExecErr{w}:
62      False{}
63
64def AaTarget.show(t: AaTarget) -> String:
65  match t:
66    case AaTStay{}:
67      "stay"
68    case AaTProfile{n}:
69      "profile " ++ X.AaText.to_string(n)
70    case AaTUnconfined{}:
71      "unconfined"
72
73def AaExecResult.show(r: AaExecResult) -> String:
74  match r:
75    case AaExecOk{t, s, d}:
76      AaTarget.show(t) ++ Bool.pick(String, s, " scrub", "")
77    case AaExecErr{w}:
78      match w:
79        case AaExecDenied{d}:
80          "denied (" ++ V.AaDecision.show(d) ++ ")"
81        case AaExecNoProfile{}:
82          "no profile"
83        case AaExecConflict{}:
84          "conflict"
85        case AaExecAmbiguous{}:
86          "ambiguous"
87        case AaExecUnknown{}:
88          "unknown profile"
89
90# Attachments
91
92type AaAttach is Data:
93  AaAttachNone{}
94  AaAttachOne{name: List<&2, U32>, rank: U32}
95  AaAttachTie{rank: U32}
96
97def AaAttach.rank(a: AaAttach) -> U32:
98  match a:
99    case AaAttachNone{}:
100      0
101    case AaAttachOne{n, r}:
102      r
103    case AaAttachTie{r}:
104      r
105
106# the better of the best so far and a candidate of rank r
107def AaAttach.better(+best: AaAttach, +r: U32, name: List<&2, U32>) -> AaAttach:
108  +b = AaAttach.rank(best)
109  Bool.pick(AaAttach, U32.is_eq(r, 0), best, Bool.pick(AaAttach, U32.is_gt(r, b), AaAttachOne{name, r}, Bool.pick(AaAttach, U32.is_eq(r, b), AaAttachTie{r}, best)))
110
111def AaAttach.rank_of(m: Maybe<&2, G.AaGlob>, +path: List<&2, U32>) -> U32:
112  match m:
113    case None{}:
114      0
115    case Some{g}:
116      G.AaGlob.rank(g, path)
117
118def AaAttach.join(+prefix: List<&2, U32>, name: List<&2, U32>) -> List<&2, U32>:
119  match prefix:
120    case Nil{}:
121      name
122    case Con{h, t}:
123      X.AaText.append(Con{h, t}, X.AaText.append(X.AaText.of_string("//"), name))
124
125# the profile of the list whose attachment best matches the path; prefix:
126# the full name of the parent, for children
127def AaAttach.best(ps: List<&2, PR.AaProfile>, +path: List<&2, U32>, +prefix: List<&2, U32>, +best: AaAttach) -> AaAttach:
128  match ps:
129    case Nil{}:
130      best
131    case Con{+p, t}:
132      AaAttach.best(t, path, prefix, AaAttach.better(best, AaAttach.rank_of(PR.AaProfile.attach(p), path), AaAttach.join(prefix, PR.AaProfile.name(p))))
133
134# The exec mode the matching rules give
135
136type AaXSel is Data:
137  AaXSel{mode: F.AaXMode, target: Maybe<&2, List<&2, U32>>}
138
139def AaXSel.target_eq(a: Maybe<&2, List<&2, U32>>, b: Maybe<&2, List<&2, U32>>) -> Bool:
140  match a b:
141    case None{} None{}:
142      True{}
143    case Some{x} Some{y}:
144      X.AaText.eq(x, y)
145    case _ _:
146      False{}
147
148def AaXSel.eq(a: AaXSel, b: AaXSel) -> Bool:
149  match a b:
150    case AaXSel{m1, t1} AaXSel{m2, t2}:
151      Bool.and(F.AaXMode.eq(m1, m2), AaXSel.target_eq(t1, t2))
152
153# the exec rules among the matching ones: literal ones and pattern ones
154type AaXSels is Data:
155  AaXSels{literal: List<&2, AaXSel>, pattern: List<&2, AaXSel>}
156
157def AaXSels.add(s: AaXSels, lit: Bool, x: AaXSel) -> AaXSels:
158  match s:
159    case AaXSels{l, p}:
160      match lit:
161        case True{}:
162          AaXSels{Con{x, l}, p}
163        case False{}:
164          AaXSels{l, Con{x, p}}
165
166def AaXSels.rule.go(deny: Bool, s: AaXSels, lit: Bool, x: AaXSel) -> AaXSels:
167  match deny:
168    case True{}:
169      s
170    case False{}:
171      AaXSels.add(s, lit, x)
172
173def AaXSels.rule(s: AaXSels, r: F.AaFileRule) -> AaXSels:
174  match r:
175    case F.AaFileRule{q, txt, g, ps, e, tg}:
176      match e:
177        case None{}:
178          s
179        case Some{m}:
180          AaXSels.rule.go(P.AaQual.deny(q), s, G.AaGlob.is_literal(g), AaXSel{m, tg})
181
182def AaXSels.of(rs: List<&2, F.AaFileRule>, s: AaXSels) -> AaXSels:
183  match rs:
184    case Nil{}:
185      s
186    case Con{r, t}:
187      AaXSels.of(t, AaXSels.rule(s, r))
188
189# every selection agrees with x
190def AaXSel.all_eq(xs: List<&2, AaXSel>, +x: AaXSel) -> Bool:
191  match xs:
192    case Nil{}:
193      True{}
194    case Con{y, t}:
195      Bool.and(AaXSel.eq(y, x), AaXSel.all_eq(t, x))
196
197# the selection the list agrees on: None for an empty list, a conflict otherwise
198type AaXPick is Data:
199  AaXNone{}
200  AaXOne{sel: AaXSel}
201  AaXClash{}
202
203def AaXPick.of(xs: List<&2, AaXSel>) -> AaXPick:
204  match xs:
205    case Nil{}:
206      AaXNone{}
207    case Con{+x, t}:
208      Bool.pick(AaXPick, AaXSel.all_eq(t, x), AaXOne{x}, AaXClash{})
209
210def AaXPick.choose(lit: AaXPick, pat: AaXPick) -> AaXPick:
211  match lit:
212    case AaXNone{}:
213      pat
214    case AaXOne{x}:
215      AaXOne{x}
216    case AaXClash{}:
217      AaXClash{}
218
219def AaXPick.sels(s: AaXSels) -> AaXPick:
220  match s:
221    case AaXSels{l, p}:
222      AaXPick.choose(AaXPick.of(l), AaXPick.of(p))
223
224# the exec mode the matching rules rs give
225def AaXPick.rules(rs: List<&2, F.AaFileRule>) -> AaXPick:
226  AaXPick.sels(AaXSels.of(rs, AaXSels{Nil{}, Nil{}}))
227
228# Applying a mode
229
230def AaTrans.fallback(fb: F.AaXFallback, scrub: Bool, d: V.AaDecision) -> AaExecResult:
231  match fb:
232    case F.AaFbNone{}:
233      AaExecErr{AaExecNoProfile{}}
234    case F.AaFbIx{}:
235      AaExecOk{AaTStay{}, False{}, d}
236    case F.AaFbUx{}:
237      AaExecOk{AaTUnconfined{}, scrub, d}
238
239def AaTrans.attached(a: AaAttach, fb: F.AaXFallback, scrub: Bool, d: V.AaDecision) -> AaExecResult:
240  match a:
241    case AaAttachNone{}:
242      AaTrans.fallback(fb, scrub, d)
243    case AaAttachOne{n, r}:
244      AaExecOk{AaTProfile{n}, scrub, d}
245    case AaAttachTie{r}:
246      AaExecErr{AaExecAmbiguous{}}
247
248def AaTrans.named(m: Maybe<&2, PR.AaProfile>, name: List<&2, U32>, fb: F.AaXFallback, scrub: Bool, d: V.AaDecision) -> AaExecResult:
249  match m:
250    case None{}:
251      AaTrans.fallback(fb, scrub, d)
252    case Some{p}:
253      AaExecOk{AaTProfile{name}, scrub, d}
254
255# px: the profile named, else the best attachment in the namespace
256def AaTrans.px(tg: Maybe<&2, List<&2, U32>>, pol: PR.AaPolicy, +path: List<&2, U32>, scrub: Bool, fb: F.AaXFallback, d: V.AaDecision) -> AaExecResult:
257  match tg:
258    case Some{+t}:
259      AaTrans.named(PR.AaPolicy.lookup(pol, t), t, fb, scrub, d)
260    case None{}:
261      AaTrans.attached(AaAttach.best(PR.AaPolicy.profiles(pol), path, Nil{}, AaAttachNone{}), fb, scrub, d)
262
263# cx: the child named, else the child whose attachment matches best
264def AaTrans.cx(tg: Maybe<&2, List<&2, U32>>, +p: PR.AaProfile, +pname: List<&2, U32>, +path: List<&2, U32>, scrub: Bool, fb: F.AaXFallback, d: V.AaDecision) -> AaExecResult:
265  match tg:
266    case Some{+t}:
267      AaTrans.named(PR.AaProfile.find(PR.AaProfile.children(p), t), AaAttach.join(pname, t), fb, scrub, d)
268    case None{}:
269      AaTrans.attached(AaAttach.best(PR.AaProfile.children(p), path, pname, AaAttachNone{}), fb, scrub, d)
270
271def AaTrans.apply(sel: AaXSel, pol: PR.AaPolicy, p: PR.AaProfile, pname: List<&2, U32>, path: List<&2, U32>, d: V.AaDecision) -> AaExecResult:
272  match sel:
273    case AaXSel{m, tg}:
274      match m:
275        case F.AaXIx{}:
276          AaExecOk{AaTStay{}, False{}, d}
277        case F.AaXUx{s}:
278          AaExecOk{AaTUnconfined{}, s, d}
279        case F.AaXPx{s, fb}:
280          AaTrans.px(tg, pol, path, s, fb, d)
281        case F.AaXCx{s, fb}:
282          AaTrans.cx(tg, p, pname, path, s, fb, d)
283
284# an unconfined task (or a profile in unconfined mode) executing path: the
285# profile whose attachment matches, else unconfined
286def AaTrans.exec_unconfined(pol: PR.AaPolicy, +path: List<&2, U32>) -> AaExecResult:
287  AaTrans.attached(AaAttach.best(PR.AaPolicy.profiles(pol), path, Nil{}, AaAttachNone{}), F.AaFbUx{}, False{}, V.AaAllow{})
288
289def AaTrans.exec.pick(k: AaXPick, pol: PR.AaPolicy, p: PR.AaProfile, pname: List<&2, U32>, path: List<&2, U32>, d: V.AaDecision) -> AaExecResult:
290  match k:
291    case AaXNone{}:
292      AaExecOk{AaTStay{}, False{}, d}
293    case AaXOne{sel}:
294      AaTrans.apply(sel, pol, p, pname, path, d)
295    case AaXClash{}:
296      AaExecErr{AaExecConflict{}}
297
298def AaTrans.exec.granted(ok: Bool, +q: F.AaFileQuery, pol: PR.AaPolicy, +p: PR.AaProfile, pname: List<&2, U32>, path: List<&2, U32>, +d: V.AaDecision) -> AaExecResult:
299  match ok:
300    case True{}:
301      AaTrans.exec.pick(AaXPick.rules(F.AaFileRule.matching(PR.AaRules.files(PR.AaProfile.rules(p)), q)), pol, p, pname, path, d)
302    case False{}:
303      AaExecErr{AaExecDenied{d}}
304
305def AaTrans.is_unconfined(m: PR.AaMode) -> Bool:
306  match m:
307    case PR.AaModeUnconfined{}:
308      True{}
309    case _:
310      False{}
311
312def AaTrans.exec.mode(unc: Bool, opts: O.AaOptions, +pol: PR.AaPolicy, +p: PR.AaProfile, +pname: List<&2, U32>, owner: Bool, +path: List<&2, U32>) -> AaExecResult:
313  match unc:
314    case True{}:
315      AaTrans.exec_unconfined(pol, path)
316    case False{}:
317      +q = {F.AaFileQuery{path, owner, P.AaPerms.bit(6n)} : F.AaFileQuery}
318      +d = {V.AaEval.file(opts, p, q) : V.AaDecision}
319      AaTrans.exec.granted(V.AaDecision.allowed(d), q, pol, p, pname, path, d)
320
321def AaTrans.exec.of(m: Maybe<&2, PR.AaProfile>, opts: O.AaOptions, pol: PR.AaPolicy, pname: List<&2, U32>, owner: Bool, path: List<&2, U32>) -> AaExecResult:
322  match m:
323    case None{}:
324      AaExecErr{AaExecUnknown{}}
325    case Some{+p}:
326      AaTrans.exec.mode(AaTrans.is_unconfined(PR.AaFlags.mode(PR.AaProfile.flags(p))), opts, pol, p, pname, owner, path)
327
328# a task confined by the profile with full name pname executes path (owner:
329# its fsuid owns the file): where it goes, or why it may not
330def AaTrans.exec(opts: O.AaOptions, +pol: PR.AaPolicy, +pname: List<&2, U32>, owner: Bool, path: List<&2, U32>) -> AaExecResult:
331  AaTrans.exec.of(PR.AaPolicy.lookup(pol, pname), opts, pol, pname, owner, path)