rule_mount.bend

bend-osdev-apparmor@0.1.0.0 · 305 lines · 41 definitions

1# bend-osdev-apparmor: mount rules (apparmor.d(5), "MOUNT RULE", "Mount
2# Rules"): `mount [CONDS] [SOURCE] [-> MOUNTPOINT]`, `remount [CONDS]
3# MOUNTPOINT`, `umount [CONDS] MOUNTPOINT`. Conditions: fstype (or vfstype)
4# = or in a list of patterns; options = a set (the mount's options must be
5# exactly that set) or in a set (any combination of them). A rule with
6# several options conditions grants each set, as the page documents (its
7# KNOWN BUGS say the parser merges them; the package follows the
8# documented meaning). Unspecified conditions match everything. One
9# permission bit: the operation.
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 AaMountOp is Data:
19  AaMountOpMount{}
20  AaMountOpRemount{}
21  AaMountOpUmount{}
22
23# options = (exact) or options in (not exact)
24type AaMountOpts is Data:
25  AaMountOpts{exact: Bool, flags: List<&2, List<&2, U32>>}
26
27type AaMountRule is Data:
28  AaMountRule{qual: P.AaQual, op: AaMountOp, fstypes: Maybe<&2, List<&2, G.AaGlob>>, options: List<&2, AaMountOpts>, source: Maybe<&2, G.AaGlob>, target: Maybe<&2, G.AaGlob>}
29
30# a mount, remount or umount: the filesystem type, the options (names as
31# mount(8) -o takes them; rw for a read-write mount), the source device and
32# the mountpoint (empty source for remount and umount)
33type AaMountQuery is Data:
34  AaMountQuery{op: AaMountOp, fstype: List<&2, U32>, options: List<&2, List<&2, U32>>, source: List<&2, U32>, target: List<&2, U32>}
35
36def AaMount.flags() -> List<&2, String>:
37  ["ro", "rw", "nosuid", "suid", "nodev", "dev", "noexec", "exec", "sync", "async", "remount", "mand", "nomand", "dirsync", "noatime", "atime", "nodiratime", "diratime", "bind", "rbind", "move", "verbose", "silent", "loud", "acl", "noacl", "unbindable", "runbindable", "private", "rprivate", "slave", "rslave", "shared", "rshared", "relatime", "norelatime", "iversion", "noiversion", "strictatime", "nostrictatime", "lazytime", "nolazytime", "nouser", "user", "symfollow", "nosymfollow"]
38
39def AaMountOp.eq(a: AaMountOp, b: AaMountOp) -> Bool:
40  match a b:
41    case AaMountOpMount{} AaMountOpMount{}:
42      True{}
43    case AaMountOpRemount{} AaMountOpRemount{}:
44      True{}
45    case AaMountOpUmount{} AaMountOpUmount{}:
46      True{}
47    case _ _:
48      False{}
49
50def AaMountOp.is_mount(a: AaMountOp) -> Bool:
51  match a:
52    case AaMountOpMount{}:
53      True{}
54    case _:
55      False{}
56
57# Reading the terms. pend: 0 nothing pending, 1 after the word fstype, 2
58# after options, 3 after fstype in, 4 after options in; arrow: -> seen
59
60type AaMtB is Data:
61  AaMtB{pend: Nat, fstypes: Maybe<&2, List<&2, G.AaGlob>>, opts: List<&2, AaMountOpts>, p1: Maybe<&2, G.AaGlob>, arrow: Bool, p2: Maybe<&2, G.AaGlob>}
62
63def AaMtB.fstypes(b: AaMtB, gs: List<&2, G.AaGlob>) -> AaMtB:
64  match b:
65    case AaMtB{pe, fs, os, p1, ar, p2}:
66      AaMtB{0n, R.AaRule.add_globs(fs, gs), os, p1, ar, p2}
67
68def AaMount.opts_append(xs: List<&2, AaMountOpts>, y: AaMountOpts) -> List<&2, AaMountOpts>:
69  match xs:
70    case Nil{}:
71      [y]
72    case Con{h, t}:
73      Con{h, AaMount.opts_append(t, y)}
74
75def AaMtB.options(b: AaMtB, o: AaMountOpts) -> AaMtB:
76  match b:
77    case AaMtB{pe, fs, os, p1, ar, p2}:
78      AaMtB{0n, fs, AaMount.opts_append(os, o), p1, ar, p2}
79
80def AaMtB.pend(b: AaMtB, n: Nat) -> AaMtB:
81  match b:
82    case AaMtB{pe, fs, os, p1, ar, p2}:
83      AaMtB{n, fs, os, p1, ar, p2}
84
85def AaMtB.pending(b: AaMtB) -> Nat:
86  match b:
87    case AaMtB{pe, fs, os, p1, ar, p2}:
88      pe
89
90def AaMtB.arrow(b: AaMtB, src: E.AaSrc) -> Result<&2, &2, E.AaError, AaMtB>:
91  match b:
92    case AaMtB{pe, fs, os, p1, ar, p2}:
93      match ar:
94        case True{}:
95          Fail{E.AaSrc.syntax(src)}
96        case False{}:
97          Done{AaMtB{pe, fs, os, p1, True{}, p2}}
98
99def AaMtB.path.after(p2: Maybe<&2, G.AaGlob>, pe: Nat, fs: Maybe<&2, List<&2, G.AaGlob>>, os: List<&2, AaMountOpts>, p1: Maybe<&2, G.AaGlob>, g: G.AaGlob, src: E.AaSrc) -> Result<&2, &2, E.AaError, AaMtB>:
100  match p2:
101    case None{}:
102      Done{AaMtB{pe, fs, os, p1, True{}, Some{g}}}
103    case Some{h}:
104      Fail{E.AaSrc.syntax(src)}
105
106def AaMtB.path.before(p1: Maybe<&2, G.AaGlob>, pe: Nat, fs: Maybe<&2, List<&2, G.AaGlob>>, os: List<&2, AaMountOpts>, p2: Maybe<&2, G.AaGlob>, g: G.AaGlob, src: E.AaSrc) -> Result<&2, &2, E.AaError, AaMtB>:
107  match p1:
108    case None{}:
109      Done{AaMtB{pe, fs, os, Some{g}, False{}, p2}}
110    case Some{h}:
111      Fail{E.AaSrc.syntax(src)}
112
113def AaMtB.path(b: AaMtB, g: G.AaGlob, src: E.AaSrc) -> Result<&2, &2, E.AaError, AaMtB>:
114  match b:
115    case AaMtB{pe, fs, os, p1, ar, p2}:
116      match ar:
117        case True{}:
118          AaMtB.path.after(p2, pe, fs, os, p1, g, src)
119        case False{}:
120          AaMtB.path.before(p1, pe, fs, os, p2, g, src)
121
122def AaMtB.cond.fstype(v: T.AaTerm, b: AaMtB, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaMtB>:
123  do Result<&2, &2, E.AaError, AaMtB>:
124    gs : List<&2, G.AaGlob> <- R.AaRule.value_globs(v, src)
125    return AaMtB.fstypes(b, gs)
126
127# the pairs of options that cannot both hold, so cannot both be in an exact
128# set (what apparmor_parser 4.0.1 refuses as "conflicting flags")
129def AaMount.opposed() -> List<&2, String>:
130  ["ro", "rw", "suid", "nosuid", "dev", "nodev", "exec", "noexec", "sync", "async", "mand", "nomand", "atime", "noatime", "diratime", "nodiratime", "iversion", "noiversion", "strictatime", "nostrictatime", "lazytime", "nolazytime", "user", "nouser", "symfollow", "nosymfollow", "acl", "noacl", "silent", "loud"]
131
132def AaMount.clash.go(ps: List<&2, String>, +ns: List<&2, List<&2, U32>>) -> Bool:
133  match ps:
134    case Nil{}:
135      False{}
136    case Con{a, t}:
137      match t:
138        case Nil{}:
139          False{}
140        case Con{b, rest}:
141          Bool.or(Bool.and(X.AaText.member(ns, X.AaText.of_string(a)), X.AaText.member(ns, X.AaText.of_string(b))), AaMount.clash.go(rest, ns))
142
143def AaMount.check(+exact: Bool, +ns: List<&2, List<&2, U32>>, src: E.AaSrc) -> Result<&2, &2, E.AaError, List<&2, List<&2, U32>>>:
144  Bool.pick(Result<&2, &2, E.AaError, List<&2, List<&2, U32>>>, Bool.and(exact, AaMount.clash.go(AaMount.opposed(), ns)), Fail{E.AaSrc.name(src)}, Done{ns})
145
146def AaMtB.cond.options(+exact: Bool, v: T.AaTerm, b: AaMtB, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaMtB>:
147  do Result<&2, &2, E.AaError, AaMtB>:
148    ns0 : List<&2, List<&2, U32>> <- R.AaRule.names(v, AaMount.flags(), src)
149    ns : List<&2, List<&2, U32>> <- AaMount.check(exact, ns0, src)
150    return AaMtB.options(b, AaMountOpts{exact, ns})
151
152def AaMtB.cond(+k: List<&2, U32>, +v: T.AaTerm, +b: AaMtB, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaMtB>:
153  Bool.pick(Result<&2, &2, E.AaError, AaMtB>, Bool.or(X.AaText.is(k, "fstype"), X.AaText.is(k, "vfstype")), AaMtB.cond.fstype(v, b, src), Bool.pick(Result<&2, &2, E.AaError, AaMtB>, X.AaText.is(k, "options"), AaMtB.cond.options(True{}, v, b, src), Fail{E.AaSrc.syntax(src)}))
154
155def AaMtB.free.path(r: Result<&2, &2, E.AaError, G.AaGlob>, b: AaMtB, src: E.AaSrc) -> Result<&2, &2, E.AaError, AaMtB>:
156  match r:
157    case Fail{e}:
158      Fail{e}
159    case Done{g}:
160      AaMtB.path(b, g, src)
161
162# a term with nothing pending
163def AaMtB.free(t: T.AaTerm, +b: AaMtB, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaMtB>:
164  match t:
165    case T.AaTmWord{+w}:
166      Bool.pick(Result<&2, &2, E.AaError, AaMtB>, Bool.or(X.AaText.is(w, "fstype"), X.AaText.is(w, "vfstype")), Done{AaMtB.pend(b, 1n)}, Bool.pick(Result<&2, &2, E.AaError, AaMtB>, X.AaText.is(w, "options"), Done{AaMtB.pend(b, 2n)}, AaMtB.free.path(R.AaRule.glob_text(w, src), b, src)))
167    case T.AaTmQuoted{q}:
168      AaMtB.free.path(R.AaRule.glob_text(q, src), b, src)
169    case T.AaTmCond{k, v}:
170      AaMtB.cond(k, v, b, src)
171    case T.AaTmArrow{}:
172      AaMtB.arrow(b, src)
173    case T.AaTmList{xs}:
174      Fail{E.AaSrc.syntax(src)}
175
176def AaMtB.step(p: Nat, t: T.AaTerm, +b: AaMtB, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaMtB>:
177  match p:
178    case 0n:
179      AaMtB.free(t, b, src)
180    case 1n+p1:
181      match p1:
182        case 0n:
183          Bool.pick(Result<&2, &2, E.AaError, AaMtB>, T.AaTerm.is(t, "in"), Done{AaMtB.pend(b, 3n)}, Fail{E.AaSrc.syntax(src)})
184        case 1n+p2:
185          match p2:
186            case 0n:
187              Bool.pick(Result<&2, &2, E.AaError, AaMtB>, T.AaTerm.is(t, "in"), Done{AaMtB.pend(b, 4n)}, Fail{E.AaSrc.syntax(src)})
188            case 1n+p3:
189              match p3:
190                case 0n:
191                  AaMtB.cond.fstype(t, b, src)
192                case 1n+p4:
193                  AaMtB.cond.options(False{}, t, b, src)
194
195def AaMtB.run(ts: List<&2, T.AaTerm>, +b: AaMtB, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaMtB>:
196  match ts:
197    case Nil{}:
198      Done{b}
199    case Con{t, rest}:
200      do Result<&2, &2, E.AaError, AaMtB>:
201        b2 : AaMtB <- AaMtB.step(AaMtB.pending(b), t, b, src)
202        AaMtB.run(rest, b2, src)
203
204def AaMtB.finish.go(m: Bool, ar: Bool, op: AaMountOp, q: P.AaQual, fs: Maybe<&2, List<&2, G.AaGlob>>, os: List<&2, AaMountOpts>, p1: Maybe<&2, G.AaGlob>, p2: Maybe<&2, G.AaGlob>, src: E.AaSrc) -> Result<&2, &2, E.AaError, AaMountRule>:
205  match m:
206    case True{}:
207      Done{AaMountRule{q, op, fs, os, p1, p2}}
208    case False{}:
209      match ar:
210        case True{}:
211          Fail{E.AaSrc.syntax(src)}
212        case False{}:
213          Done{AaMountRule{q, op, fs, os, None{}, p1}}
214
215# mount: source and mountpoint; remount, umount: one path, the mountpoint, and no arrow
216def AaMtB.finish(+op: AaMountOp, q: P.AaQual, b: AaMtB, src: E.AaSrc) -> Result<&2, &2, E.AaError, AaMountRule>:
217  match b:
218    case AaMtB{pe, fs, os, p1, ar, p2}:
219      match pe:
220        case 0n:
221          AaMtB.finish.go(AaMountOp.is_mount(op), ar, op, q, fs, os, p1, p2, src)
222        case 1n+x:
223          Fail{E.AaSrc.syntax(src)}
224
225def AaMount.parse.q(r: Result<&2, &2, E.AaError, P.AaQual>, +op: AaMountOp, ts: List<&2, T.AaTerm>, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaMountRule>:
226  match r:
227    case Fail{e}:
228      Fail{e}
229    case Done{q}:
230      do Result<&2, &2, E.AaError, AaMountRule>:
231        b : AaMtB <- AaMtB.run(ts, AaMtB{0n, None{}, Nil{}, None{}, False{}, None{}}, src)
232        AaMtB.finish(op, q, b, src)
233
234# the terms after mount, remount or umount
235def AaMount.parse(op: AaMountOp, ts: List<&2, T.AaTerm>, q: P.AaQual, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaMountRule>:
236  AaMount.parse.q(R.AaRule.no_owner(q, src), op, ts, src)
237
238# Matching
239
240# every option of q is one of the flags; and, for an exact condition, the other way round too
241def AaMountOpts.allows(o: AaMountOpts, +q: List<&2, List<&2, U32>>) -> Bool:
242  match o:
243    case AaMountOpts{exact, +fl}:
244      match exact:
245        case True{}:
246          Bool.and(X.AaText.subset(q, fl), X.AaText.subset(fl, q))
247        case False{}:
248          X.AaText.subset(q, fl)
249
250def AaMount.opts_ok(os: List<&2, AaMountOpts>, +q: List<&2, List<&2, U32>>) -> Bool:
251  match os:
252    case Nil{}:
253      False{}
254    case Con{o, t}:
255      Bool.or(AaMountOpts.allows(o, q), AaMount.opts_ok(t, q))
256
257def AaMount.options_ok(os: List<&2, AaMountOpts>, +q: List<&2, List<&2, U32>>) -> Bool:
258  match os:
259    case Nil{}:
260      True{}
261    case Con{o, t}:
262      AaMount.opts_ok(Con{o, t}, q)
263
264def AaMountRule.matches(r: AaMountRule, q: AaMountQuery) -> Bool:
265  match r:
266    case AaMountRule{qu, op, fs, os, so, tg}:
267      match q:
268        case AaMountQuery{qop, qfs, qos, qso, qtg}:
269          Bool.and(AaMountOp.eq(op, qop), Bool.and(R.AaRule.opt_any(fs, qfs), Bool.and(AaMount.options_ok(os, qos), Bool.and(R.AaRule.opt_match(so, qso), R.AaRule.opt_match(tg, qtg)))))
270
271def AaMountRule.matching.go(hit: Bool, r: AaMountRule, rest: List<&2, AaMountRule>) -> List<&2, AaMountRule>:
272  match hit:
273    case True{}:
274      Con{r, rest}
275    case False{}:
276      rest
277
278def AaMountRule.matching(rs: List<&2, AaMountRule>, +q: AaMountQuery) -> List<&2, AaMountRule>:
279  match rs:
280    case Nil{}:
281      Nil{}
282    case Con{+r, t}:
283      AaMountRule.matching.go(AaMountRule.matches(r, q), r, AaMountRule.matching(t, q))
284
285def AaMountRule.grants.of(rs: List<&2, AaMountRule>) -> List<&2, P.AaGrant>:
286  match rs:
287    case Nil{}:
288      Nil{}
289    case Con{r, t}:
290      match r:
291        case AaMountRule{qu, op, fs, os, so, tg}:
292          Con{P.AaGrant.of(qu, P.AaPerms.bit(0n)), AaMountRule.grants.of(t)}
293
294def AaMountRule.grants(rs: List<&2, AaMountRule>, +q: AaMountQuery) -> List<&2, P.AaGrant>:
295  AaMountRule.grants.of(AaMountRule.matching(rs, q))
296
297def AaMountRule.append(xs: List<&2, AaMountRule>, ys: List<&2, AaMountRule>) -> List<&2, AaMountRule>:
298  match xs:
299    case Nil{}:
300      ys
301    case Con{h, t}:
302      Con{h, AaMountRule.append(t, ys)}
303
304def AaMountQuery.req() -> P.AaPerms:
305  P.AaPerms.bit(0n)