rule_signal.bend

bend-osdev-apparmor@0.1.0.0 · 218 lines · 32 definitions

1# bend-osdev-apparmor: signal rules (apparmor.d(5), "SIGNAL RULE", "Signal
2# rules"): `signal [ACCESS] [set=(SIGNALS)] [peer=AARE]`, the conditions in
3# any order. Permission bits: send 0, receive 1; with no access list both
4# are implied. r and read are receive, w and write send, rw both (the page
5# gives these synonyms for dbus; the package reads signal's the same way).
6import Base
7import bend-osdev-apparmor@0.1.0.0/text.bend as X
8import bend-osdev-apparmor@0.1.0.0/glob.bend as G
9import bend-osdev-apparmor@0.1.0.0/perm.bend as P
10import bend-osdev-apparmor@0.1.0.0/token.bend as T
11import bend-osdev-apparmor@0.1.0.0/error.bend as E
12import bend-osdev-apparmor@0.1.0.0/rule.bend as R
13
14# signals: None for every signal; peer: None for every peer
15type AaSignalRule is Data:
16  AaSignalRule{qual: P.AaQual, perms: P.AaPerms, signals: Maybe<&2, List<&2, List<&2, U32>>>, peer: Maybe<&2, G.AaGlob>}
17
18# a signal sent or received (req: send and/or receive), by name (hup, int,
19# ..., rtmin+N) and the peer's profile name
20type AaSignalQuery is Data:
21  AaSignalQuery{req: P.AaPerms, signal: List<&2, U32>, peer: List<&2, U32>}
22
23def AaSignal.send() -> Nat:
24  0n
25
26def AaSignal.receive() -> Nat:
27  1n
28
29def AaSignal.names() -> List<&2, String>:
30  ["hup", "int", "quit", "ill", "trap", "abrt", "bus", "fpe", "kill", "usr1", "segv", "usr2", "pipe", "alrm", "term", "stkflt", "chld", "cont", "stop", "stp", "ttin", "ttou", "urg", "xcpu", "xfsz", "vtalrm", "prof", "winch", "io", "pwr", "sys", "emt", "exists"]
31
32# the digits of xs as a number, if every character is a digit (at most 3)
33def AaSignal.num.go(xs: List<&2, U32>, +acc: U32, +n: Nat) -> Maybe<&2, U32>:
34  match xs:
35    case Nil{}:
36      Bool.pick(Maybe<&2, U32>, Nat.is_eq(n, 0n), None{}, Some{acc})
37    case Con{+h, t}:
38      Bool.pick(Maybe<&2, U32>, Bool.and(Bool.and(U32.is_ge(h, 48), U32.is_le(h, 57)), Nat.is_lt(n, 3n)), AaSignal.num.go(t, U32.add(U32.mul(acc, 10), U32.sub(h, 48)), 1n+n), None{})
39
40def AaSignal.rt.go(m: Maybe<&2, U32>) -> Bool:
41  match m:
42    case None{}:
43      False{}
44    case Some{v}:
45      U32.is_le(v, 32)
46
47# rtmin+0 ... rtmin+32
48def AaSignal.is_rt(+w: List<&2, U32>) -> Bool:
49  Bool.and(X.AaText.starts(w, "rtmin+"), AaSignal.rt.go(AaSignal.num.go(X.AaText.drop(6n, w), 0, 0n)))
50
51def AaSignal.valid(+w: List<&2, U32>) -> Bool:
52  Bool.or(X.AaText.one_of(AaSignal.names(), w), AaSignal.is_rt(w))
53
54def AaSignal.check(xs: List<&2, List<&2, U32>>, +src: E.AaSrc) -> Result<&2, &2, E.AaError, List<&2, List<&2, U32>>>:
55  match xs:
56    case Nil{}:
57      Done{Nil{}}
58    case Con{+x, rest}:
59      R.AaRule.check_names.go(AaSignal.valid(x), x, AaSignal.check(rest, src), src)
60
61# the bits of an access word
62def AaSignal.access(+w: List<&2, U32>) -> Maybe<&2, P.AaPerms>:
63  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, "rw"), Some{P.AaPerms.of_bits([True{}, True{}])}, None{})))
64
65# Reading the conditions: the permissions so far (None: none given yet)
66
67type AaSigB is Data:
68  AaSigB{perms: Maybe<&2, P.AaPerms>, signals: Maybe<&2, List<&2, List<&2, U32>>>, peer: Maybe<&2, G.AaGlob>}
69
70def AaSigB.perms(m: Maybe<&2, P.AaPerms>, b: AaSigB, src: E.AaSrc) -> Result<&2, &2, E.AaError, AaSigB>:
71  match m:
72    case None{}:
73      Fail{E.AaSrc.syntax(src)}
74    case Some{p}:
75      match b:
76        case AaSigB{bp, s, pe}:
77          match bp:
78            case None{}:
79              Done{AaSigB{Some{p}, s, pe}}
80            case Some{q}:
81              Done{AaSigB{Some{P.AaPerms.union(q, p)}, s, pe}}
82
83def AaSigB.access_list(xs: List<&2, T.AaTerm>, b: AaSigB, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaSigB>:
84  match xs:
85    case Nil{}:
86      Done{b}
87    case Con{x, rest}:
88      match x:
89        case T.AaTmWord{w}:
90          do Result<&2, &2, E.AaError, AaSigB>:
91            b2 : AaSigB <- AaSigB.perms(AaSignal.access(w), b, src)
92            AaSigB.access_list(rest, b2, src)
93        case _:
94          Fail{E.AaSrc.syntax(src)}
95
96def AaSigB.add_signals(b: AaSigB, xs: List<&2, List<&2, U32>>) -> AaSigB:
97  match b:
98    case AaSigB{p, s, pe}:
99      match s:
100        case None{}:
101          AaSigB{p, Some{xs}, pe}
102        case Some{ys}:
103          AaSigB{p, Some{X.AaText.lappend(ys, xs)}, pe}
104
105def AaSigB.set_peer(b: AaSigB, g: G.AaGlob, src: E.AaSrc) -> Result<&2, &2, E.AaError, AaSigB>:
106  match b:
107    case AaSigB{p, s, pe}:
108      match pe:
109        case None{}:
110          Done{AaSigB{p, s, Some{g}}}
111        case Some{h}:
112          Fail{E.AaSrc.syntax(src)}
113
114def AaSigB.cond.set(v: T.AaTerm, b: AaSigB, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaSigB>:
115  do Result<&2, &2, E.AaError, AaSigB>:
116    xs : List<&2, List<&2, U32>> <- R.AaRule.texts(T.AaTerm.texts(v), src)
117    ys : List<&2, List<&2, U32>> <- AaSignal.check(xs, src)
118    return AaSigB.add_signals(b, ys)
119
120def AaSigB.cond.peer(v: T.AaTerm, b: AaSigB, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaSigB>:
121  do Result<&2, &2, E.AaError, AaSigB>:
122    g : G.AaGlob <- R.AaRule.value_glob(v, src)
123    AaSigB.set_peer(b, g, src)
124
125def AaSigB.cond(+k: List<&2, U32>, +v: T.AaTerm, +b: AaSigB, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaSigB>:
126  Bool.pick(Result<&2, &2, E.AaError, AaSigB>, X.AaText.is(k, "set"), AaSigB.cond.set(v, b, src), Bool.pick(Result<&2, &2, E.AaError, AaSigB>, X.AaText.is(k, "peer"), AaSigB.cond.peer(v, b, src), Fail{E.AaSrc.syntax(src)}))
127
128def AaSigB.step(t: T.AaTerm, b: AaSigB, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaSigB>:
129  match t:
130    case T.AaTmWord{w}:
131      AaSigB.perms(AaSignal.access(w), b, src)
132    case T.AaTmList{xs}:
133      AaSigB.access_list(xs, b, src)
134    case T.AaTmCond{k, v}:
135      AaSigB.cond(k, v, b, src)
136    case _:
137      Fail{E.AaSrc.syntax(src)}
138
139def AaSigB.run(ts: List<&2, T.AaTerm>, b: AaSigB, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaSigB>:
140  match ts:
141    case Nil{}:
142      Done{b}
143    case Con{t, rest}:
144      do Result<&2, &2, E.AaError, AaSigB>:
145        b2 : AaSigB <- AaSigB.step(t, b, src)
146        AaSigB.run(rest, b2, src)
147
148def AaSigB.finish(q: P.AaQual, b: AaSigB) -> AaSignalRule:
149  match b:
150    case AaSigB{p, s, pe}:
151      AaSignalRule{q, Maybe.default(&2, P.AaPerms, p, P.AaPerms.of_bits([True{}, True{}])), s, pe}
152
153def AaSignal.parse.q(r: Result<&2, &2, E.AaError, P.AaQual>, ts: List<&2, T.AaTerm>, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaSignalRule>:
154  match r:
155    case Fail{e}:
156      Fail{e}
157    case Done{q}:
158      do Result<&2, &2, E.AaError, AaSignalRule>:
159        b : AaSigB <- AaSigB.run(ts, AaSigB{None{}, None{}, None{}}, src)
160        return AaSigB.finish(q, b)
161
162# the terms after `signal`
163def AaSignal.parse(ts: List<&2, T.AaTerm>, q: P.AaQual, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaSignalRule>:
164  AaSignal.parse.q(R.AaRule.no_owner(q, src), ts, src)
165
166# Matching
167
168def AaSignal.opt_member(m: Maybe<&2, List<&2, List<&2, U32>>>, +x: List<&2, U32>) -> Bool:
169  match m:
170    case None{}:
171      True{}
172    case Some{xs}:
173      X.AaText.member(xs, x)
174
175def AaSignalRule.matches(r: AaSignalRule, q: AaSignalQuery) -> Bool:
176  match r:
177    case AaSignalRule{qu, p, s, pe}:
178      match q:
179        case AaSignalQuery{req, sig, peer}:
180          Bool.and(AaSignal.opt_member(s, sig), R.AaRule.opt_match(pe, peer))
181
182def AaSignalRule.matching.go(hit: Bool, r: AaSignalRule, rest: List<&2, AaSignalRule>) -> List<&2, AaSignalRule>:
183  match hit:
184    case True{}:
185      Con{r, rest}
186    case False{}:
187      rest
188
189def AaSignalRule.matching(rs: List<&2, AaSignalRule>, +q: AaSignalQuery) -> List<&2, AaSignalRule>:
190  match rs:
191    case Nil{}:
192      Nil{}
193    case Con{+r, t}:
194      AaSignalRule.matching.go(AaSignalRule.matches(r, q), r, AaSignalRule.matching(t, q))
195
196def AaSignalRule.grants.of(rs: List<&2, AaSignalRule>) -> List<&2, P.AaGrant>:
197  match rs:
198    case Nil{}:
199      Nil{}
200    case Con{r, t}:
201      match r:
202        case AaSignalRule{qu, p, s, pe}:
203          Con{P.AaGrant.of(qu, p), AaSignalRule.grants.of(t)}
204
205def AaSignalRule.grants(rs: List<&2, AaSignalRule>, +q: AaSignalQuery) -> List<&2, P.AaGrant>:
206  AaSignalRule.grants.of(AaSignalRule.matching(rs, q))
207
208def AaSignalRule.append(xs: List<&2, AaSignalRule>, ys: List<&2, AaSignalRule>) -> List<&2, AaSignalRule>:
209  match xs:
210    case Nil{}:
211      ys
212    case Con{h, t}:
213      Con{h, AaSignalRule.append(t, ys)}
214
215def AaSignalQuery.req(q: AaSignalQuery) -> P.AaPerms:
216  match q:
217    case AaSignalQuery{r, s, p}:
218      r