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).
6	import Base
7	import ./text.bend as X
8	import ./glob.bend as G
9	import ./perm.bend as P
10	import ./token.bend as T
11	import ./error.bend as E
12	import ./rule.bend as R
13	
14	type 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)
18	type AaPtraceQuery is Data:
19	  AaPtraceQuery{req: P.AaPerms, peer: List<&2, U32>}
20	
21	def AaPtrace.read() -> Nat:
22	  0n
23	
24	def AaPtrace.trace() -> Nat:
25	  1n
26	
27	def AaPtrace.readby() -> Nat:
28	  2n
29	
30	def AaPtrace.tracedby() -> Nat:
31	  3n
32	
33	def 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	
36	type AaPtB is Data:
37	  AaPtB{perms: Maybe<&2, P.AaPerms>, peer: Maybe<&2, G.AaGlob>}
38	
39	def 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	
52	def 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	
65	def 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	
74	def 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	
79	def 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	
82	def 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	
93	def 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	
102	def 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	
107	def 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`
117	def 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	
122	def 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	
129	def 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	
136	def 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	
143	def 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	
152	def AaPtraceRule.grants(rs: List<&2, AaPtraceRule>, +q: AaPtraceQuery) -> List<&2, P.AaGrant>:
153	  AaPtraceRule.grants.of(AaPtraceRule.matching(rs, q))
154	
155	def 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	
162	def AaPtraceQuery.req(q: AaPtraceQuery) -> P.AaPerms:
163	  match q:
164	    case AaPtraceQuery{r, p}:
165	      r