rule_ptrace.bend

bend-osdev-apparmor@0.1.0.0 · 165 lines · 25 definitions

1# bend-osdev-apparmor: ptrace rules (apparmor.d(5), "PTRACE RULE", "PTrace
2# rules"): `ptrace [ACCESS] [peer=AARE]`. Permission bits: read 0, trace 1,
3# readby 2, tracedby 3; with no access list all four are implied. The page
4# lists r, w and rw without saying what they stand for; the package reads r
5# as read, w as trace and rw as both (a stated choice; see the README).
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
14type AaPtraceRule is Data:
15  AaPtraceRule{qual: P.AaQual, perms: P.AaPerms, peer: Maybe<&2, G.AaGlob>}
16
17# req: read, trace (of the peer) or readby, tracedby (by the peer)
18type AaPtraceQuery is Data:
19  AaPtraceQuery{req: P.AaPerms, peer: List<&2, U32>}
20
21def AaPtrace.read() -> Nat:
22  0n
23
24def AaPtrace.trace() -> Nat:
25  1n
26
27def AaPtrace.readby() -> Nat:
28  2n
29
30def AaPtrace.tracedby() -> Nat:
31  3n
32
33def AaPtrace.access(+w: List<&2, U32>) -> Maybe<&2, P.AaPerms>:
34  Bool.pick(Maybe<&2, P.AaPerms>, Bool.or(X.AaText.is(w, "read"), X.AaText.is(w, "r")), Some{P.AaPerms.bit(0n)}, Bool.pick(Maybe<&2, P.AaPerms>, Bool.or(X.AaText.is(w, "trace"), X.AaText.is(w, "w")), Some{P.AaPerms.bit(1n)}, Bool.pick(Maybe<&2, P.AaPerms>, X.AaText.is(w, "readby"), Some{P.AaPerms.bit(2n)}, Bool.pick(Maybe<&2, P.AaPerms>, X.AaText.is(w, "tracedby"), Some{P.AaPerms.bit(3n)}, Bool.pick(Maybe<&2, P.AaPerms>, X.AaText.is(w, "rw"), Some{P.AaPerms.of_bits([True{}, True{}])}, None{})))))
35
36type AaPtB is Data:
37  AaPtB{perms: Maybe<&2, P.AaPerms>, peer: Maybe<&2, G.AaGlob>}
38
39def AaPtB.perms(m: Maybe<&2, P.AaPerms>, b: AaPtB, src: E.AaSrc) -> Result<&2, &2, E.AaError, AaPtB>:
40  match m:
41    case None{}:
42      Fail{E.AaSrc.syntax(src)}
43    case Some{p}:
44      match b:
45        case AaPtB{bp, pe}:
46          match bp:
47            case None{}:
48              Done{AaPtB{Some{p}, pe}}
49            case Some{q}:
50              Done{AaPtB{Some{P.AaPerms.union(q, p)}, pe}}
51
52def AaPtB.access_list(xs: List<&2, T.AaTerm>, b: AaPtB, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaPtB>:
53  match xs:
54    case Nil{}:
55      Done{b}
56    case Con{x, rest}:
57      match x:
58        case T.AaTmWord{w}:
59          do Result<&2, &2, E.AaError, AaPtB>:
60            b2 : AaPtB <- AaPtB.perms(AaPtrace.access(w), b, src)
61            AaPtB.access_list(rest, b2, src)
62        case _:
63          Fail{E.AaSrc.syntax(src)}
64
65def AaPtB.set_peer(b: AaPtB, g: G.AaGlob, src: E.AaSrc) -> Result<&2, &2, E.AaError, AaPtB>:
66  match b:
67    case AaPtB{p, pe}:
68      match pe:
69        case None{}:
70          Done{AaPtB{p, Some{g}}}
71        case Some{h}:
72          Fail{E.AaSrc.syntax(src)}
73
74def AaPtB.cond.peer(v: T.AaTerm, b: AaPtB, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaPtB>:
75  do Result<&2, &2, E.AaError, AaPtB>:
76    g : G.AaGlob <- R.AaRule.value_glob(v, src)
77    AaPtB.set_peer(b, g, src)
78
79def AaPtB.cond(+k: List<&2, U32>, +v: T.AaTerm, +b: AaPtB, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaPtB>:
80  Bool.pick(Result<&2, &2, E.AaError, AaPtB>, X.AaText.is(k, "peer"), AaPtB.cond.peer(v, b, src), Fail{E.AaSrc.syntax(src)})
81
82def AaPtB.step(t: T.AaTerm, b: AaPtB, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaPtB>:
83  match t:
84    case T.AaTmWord{w}:
85      AaPtB.perms(AaPtrace.access(w), b, src)
86    case T.AaTmList{xs}:
87      AaPtB.access_list(xs, b, src)
88    case T.AaTmCond{k, v}:
89      AaPtB.cond(k, v, b, src)
90    case _:
91      Fail{E.AaSrc.syntax(src)}
92
93def AaPtB.run(ts: List<&2, T.AaTerm>, b: AaPtB, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaPtB>:
94  match ts:
95    case Nil{}:
96      Done{b}
97    case Con{t, rest}:
98      do Result<&2, &2, E.AaError, AaPtB>:
99        b2 : AaPtB <- AaPtB.step(t, b, src)
100        AaPtB.run(rest, b2, src)
101
102def AaPtB.finish(q: P.AaQual, b: AaPtB) -> AaPtraceRule:
103  match b:
104    case AaPtB{p, pe}:
105      AaPtraceRule{q, Maybe.default(&2, P.AaPerms, p, P.AaPerms.of_bits([True{}, True{}, True{}, True{}])), pe}
106
107def AaPtrace.parse.q(r: Result<&2, &2, E.AaError, P.AaQual>, ts: List<&2, T.AaTerm>, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaPtraceRule>:
108  match r:
109    case Fail{e}:
110      Fail{e}
111    case Done{q}:
112      do Result<&2, &2, E.AaError, AaPtraceRule>:
113        b : AaPtB <- AaPtB.run(ts, AaPtB{None{}, None{}}, src)
114        return AaPtB.finish(q, b)
115
116# the terms after `ptrace`
117def AaPtrace.parse(ts: List<&2, T.AaTerm>, q: P.AaQual, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaPtraceRule>:
118  AaPtrace.parse.q(R.AaRule.no_owner(q, src), ts, src)
119
120# Matching
121
122def AaPtraceRule.matches(r: AaPtraceRule, q: AaPtraceQuery) -> Bool:
123  match r:
124    case AaPtraceRule{qu, p, pe}:
125      match q:
126        case AaPtraceQuery{req, peer}:
127          R.AaRule.opt_match(pe, peer)
128
129def AaPtraceRule.matching.go(hit: Bool, r: AaPtraceRule, rest: List<&2, AaPtraceRule>) -> List<&2, AaPtraceRule>:
130  match hit:
131    case True{}:
132      Con{r, rest}
133    case False{}:
134      rest
135
136def AaPtraceRule.matching(rs: List<&2, AaPtraceRule>, +q: AaPtraceQuery) -> List<&2, AaPtraceRule>:
137  match rs:
138    case Nil{}:
139      Nil{}
140    case Con{+r, t}:
141      AaPtraceRule.matching.go(AaPtraceRule.matches(r, q), r, AaPtraceRule.matching(t, q))
142
143def AaPtraceRule.grants.of(rs: List<&2, AaPtraceRule>) -> List<&2, P.AaGrant>:
144  match rs:
145    case Nil{}:
146      Nil{}
147    case Con{r, t}:
148      match r:
149        case AaPtraceRule{qu, p, pe}:
150          Con{P.AaGrant.of(qu, p), AaPtraceRule.grants.of(t)}
151
152def AaPtraceRule.grants(rs: List<&2, AaPtraceRule>, +q: AaPtraceQuery) -> List<&2, P.AaGrant>:
153  AaPtraceRule.grants.of(AaPtraceRule.matching(rs, q))
154
155def AaPtraceRule.append(xs: List<&2, AaPtraceRule>, ys: List<&2, AaPtraceRule>) -> List<&2, AaPtraceRule>:
156  match xs:
157    case Nil{}:
158      ys
159    case Con{h, t}:
160      Con{h, AaPtraceRule.append(t, ys)}
161
162def AaPtraceQuery.req(q: AaPtraceQuery) -> P.AaPerms:
163  match q:
164    case AaPtraceQuery{r, p}:
165      r