1	# bend-osdev-apparmor: change_profile rules (apparmor.d(5), "CHANGE_PROFILE
2	# RULE", "change_profile rules"): `change_profile [[safe|unsafe] EXEC_COND]
3	# [-> PROFILE NAME]`, which profiles a task may move to through the
4	# change_profile API, optionally only when it executes a matching program.
5	# safe (the default) and unsafe say whether the environment is scrubbed; an
6	# exec mode needs an exec condition. One permission bit: change.
7	import Base
8	import ./text.bend as X
9	import ./glob.bend as G
10	import ./perm.bend as P
11	import ./token.bend as T
12	import ./error.bend as E
13	import ./rule.bend as R
14	
15	# exec: None for any (or no) exec; target: None for every profile
16	type AaChangeRule is Data:
17	  AaChangeRule{qual: P.AaQual, exec: Maybe<&2, G.AaGlob>, safe: Bool, target: Maybe<&2, G.AaGlob>}
18	
19	# a change to the profile named target, now (exec None) or when the program
20	# exec is executed
21	type AaChangeQuery is Data:
22	  AaChangeQuery{exec: Maybe<&2, List<&2, U32>>, target: List<&2, U32>}
23	
24	# the builder: mode word seen (0 none, 1 safe, 2 unsafe), exec condition,
25	# arrow seen, target
26	type AaChB is Data:
27	  AaChB{mode: Nat, exec: Maybe<&2, G.AaGlob>, arrow: Bool, target: Maybe<&2, G.AaGlob>}
28	
29	def AaChange.is_path(t: T.AaTerm) -> Bool:
30	  match t:
31	    case T.AaTmWord{+w}:
32	      Bool.or(U32.is_eq(X.AaText.head(w), 47), U32.is_eq(X.AaText.head(w), 123))
33	    case T.AaTmQuoted{q}:
34	      True{}
35	    case _:
36	      False{}
37	
38	def AaChB.set_target(b: AaChB, g: G.AaGlob, src: E.AaSrc) -> Result<&2, &2, E.AaError, AaChB>:
39	  match b:
40	    case AaChB{m, e, ar, tg}:
41	      match ar:
42	        case False{}:
43	          Fail{E.AaSrc.syntax(src)}
44	        case True{}:
45	          match tg:
46	            case None{}:
47	              Done{AaChB{m, e, True{}, Some{g}}}
48	            case Some{h}:
49	              Fail{E.AaSrc.syntax(src)}
50	
51	def AaChB.set_exec(b: AaChB, g: G.AaGlob, src: E.AaSrc) -> Result<&2, &2, E.AaError, AaChB>:
52	  match b:
53	    case AaChB{m, e, ar, tg}:
54	      match e:
55	        case None{}:
56	          match ar:
57	            case False{}:
58	              Done{AaChB{m, Some{g}, False{}, tg}}
59	            case True{}:
60	              Fail{E.AaSrc.syntax(src)}
61	        case Some{h}:
62	          Fail{E.AaSrc.syntax(src)}
63	
64	# a pattern: the target after the arrow, else the exec condition
65	def AaChB.glob(b: AaChB, g: G.AaGlob, src: E.AaSrc) -> Result<&2, &2, E.AaError, AaChB>:
66	  match b:
67	    case AaChB{m, e, +ar, tg}:
68	      match ar:
69	        case True{}:
70	          AaChB.set_target(AaChB{m, e, ar, tg}, g, src)
71	        case False{}:
72	          AaChB.set_exec(AaChB{m, e, ar, tg}, g, src)
73	
74	def AaChB.arrow(b: AaChB, src: E.AaSrc) -> Result<&2, &2, E.AaError, AaChB>:
75	  match b:
76	    case AaChB{m, e, ar, tg}:
77	      match ar:
78	        case True{}:
79	          Fail{E.AaSrc.syntax(src)}
80	        case False{}:
81	          Done{AaChB{m, e, True{}, tg}}
82	
83	# safe or unsafe, before anything else
84	def AaChB.mode(b: AaChB, n: Nat, src: E.AaSrc) -> Result<&2, &2, E.AaError, AaChB>:
85	  match b:
86	    case AaChB{m, e, ar, tg}:
87	      match m:
88	        case 0n:
89	          match e:
90	            case None{}:
91	              match ar:
92	                case False{}:
93	                  Done{AaChB{n, None{}, False{}, tg}}
94	                case True{}:
95	                  Fail{E.AaSrc.syntax(src)}
96	            case Some{h}:
97	              Fail{E.AaSrc.syntax(src)}
98	        case 1n+k:
99	          Fail{E.AaSrc.syntax(src)}
100	
101	def AaChB.term.glob(r: Result<&2, &2, E.AaError, G.AaGlob>, b: AaChB, src: E.AaSrc) -> Result<&2, &2, E.AaError, AaChB>:
102	  match r:
103	    case Fail{e}:
104	      Fail{e}
105	    case Done{g}:
106	      AaChB.glob(b, g, src)
107	
108	def AaChB.step(t: T.AaTerm, +b: AaChB, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaChB>:
109	  match t:
110	    case T.AaTmWord{+w}:
111	      Bool.pick(Result<&2, &2, E.AaError, AaChB>, X.AaText.is(w, "safe"), AaChB.mode(b, 1n, src), Bool.pick(Result<&2, &2, E.AaError, AaChB>, X.AaText.is(w, "unsafe"), AaChB.mode(b, 2n, src), AaChB.term.glob(R.AaRule.glob_text(w, src), b, src)))
112	    case T.AaTmQuoted{q}:
113	      AaChB.term.glob(R.AaRule.glob_text(q, src), b, src)
114	    case T.AaTmArrow{}:
115	      AaChB.arrow(b, src)
116	    case _:
117	      Fail{E.AaSrc.syntax(src)}
118	
119	def AaChB.run(ts: List<&2, T.AaTerm>, b: AaChB, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaChB>:
120	  match ts:
121	    case Nil{}:
122	      Done{b}
123	    case Con{t, rest}:
124	      do Result<&2, &2, E.AaError, AaChB>:
125	        b2 : AaChB <- AaChB.step(t, b, src)
126	        AaChB.run(rest, b2, src)
127	
128	def AaChange.is_some(m: Maybe<&2, G.AaGlob>) -> Bool:
129	  match m:
130	    case None{}:
131	      False{}
132	    case Some{g}:
133	      True{}
134	
135	# an exec mode needs an exec condition; an arrow needs a target
136	def AaChB.finish(q: P.AaQual, b: AaChB, src: E.AaSrc) -> Result<&2, &2, E.AaError, AaChangeRule>:
137	  match b:
138	    case AaChB{+m, +e, ar, +tg}:
139	      +bad = Bool.or(Bool.and(Nat.is_gt(m, 0n), Bool.not(AaChange.is_some(e))), Bool.and(ar, Bool.not(AaChange.is_some(tg))))
140	      Bool.pick(Result<&2, &2, E.AaError, AaChangeRule>, bad, Fail{E.AaSrc.syntax(src)}, Done{AaChangeRule{q, e, Bool.not(Nat.is_eq(m, 2n)), tg}})
141	
142	def AaChange.parse.q(r: Result<&2, &2, E.AaError, P.AaQual>, ts: List<&2, T.AaTerm>, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaChangeRule>:
143	  match r:
144	    case Fail{e}:
145	      Fail{e}
146	    case Done{q}:
147	      do Result<&2, &2, E.AaError, AaChangeRule>:
148	        b : AaChB <- AaChB.run(ts, AaChB{0n, None{}, False{}, None{}}, src)
149	        AaChB.finish(q, b, src)
150	
151	# the terms after `change_profile`
152	def AaChange.parse(ts: List<&2, T.AaTerm>, q: P.AaQual, +src: E.AaSrc) -> Result<&2, &2, E.AaError, AaChangeRule>:
153	  AaChange.parse.q(R.AaRule.no_owner(q, src), ts, src)
154	
155	# Matching: the target matches, and a rule with an exec condition applies
156	# only to a change at the exec of a matching program
157	
158	def AaChange.exec_ok(m: Maybe<&2, G.AaGlob>, x: Maybe<&2, List<&2, U32>>) -> Bool:
159	  match m:
160	    case None{}:
161	      True{}
162	    case Some{g}:
163	      match x:
164	        case None{}:
165	          False{}
166	        case Some{p}:
167	          G.AaGlob.matches(g, p)
168	
169	def AaChangeRule.matches(r: AaChangeRule, q: AaChangeQuery) -> Bool:
170	  match r:
171	    case AaChangeRule{qu, e, s, tg}:
172	      match q:
173	        case AaChangeQuery{qe, qt}:
174	          Bool.and(AaChange.exec_ok(e, qe), R.AaRule.opt_match(tg, qt))
175	
176	def AaChangeRule.matching.go(hit: Bool, r: AaChangeRule, rest: List<&2, AaChangeRule>) -> List<&2, AaChangeRule>:
177	  match hit:
178	    case True{}:
179	      Con{r, rest}
180	    case False{}:
181	      rest
182	
183	def AaChangeRule.matching(rs: List<&2, AaChangeRule>, +q: AaChangeQuery) -> List<&2, AaChangeRule>:
184	  match rs:
185	    case Nil{}:
186	      Nil{}
187	    case Con{+r, t}:
188	      AaChangeRule.matching.go(AaChangeRule.matches(r, q), r, AaChangeRule.matching(t, q))
189	
190	def AaChangeRule.grants.of(rs: List<&2, AaChangeRule>) -> List<&2, P.AaGrant>:
191	  match rs:
192	    case Nil{}:
193	      Nil{}
194	    case Con{r, t}:
195	      match r:
196	        case AaChangeRule{qu, e, s, tg}:
197	          Con{P.AaGrant.of(qu, P.AaPerms.bit(0n)), AaChangeRule.grants.of(t)}
198	
199	def AaChangeRule.grants(rs: List<&2, AaChangeRule>, +q: AaChangeQuery) -> List<&2, P.AaGrant>:
200	  AaChangeRule.grants.of(AaChangeRule.matching(rs, q))
201	
202	def AaChangeRule.append(xs: List<&2, AaChangeRule>, ys: List<&2, AaChangeRule>) -> List<&2, AaChangeRule>:
203	  match xs:
204	    case Nil{}:
205	      ys
206	    case Con{h, t}:
207	      Con{h, AaChangeRule.append(t, ys)}
208	
209	def AaChangeQuery.req() -> P.AaPerms:
210	  P.AaPerms.bit(0n)