1	# bend-osdev-apparmor: profiles (apparmor.d(5), "Profile Head", "Flags",
2	# and the rules of a profile body), their children and hats, and a loaded
3	# policy.
4	#
5	# A profile has a name, an optional exec attachment (a pattern; a name that
6	# is an absolute path is its own attachment), flags (a mode and the audit
7	# flag), its rules of each kind, and its child profiles and hats. A child's
8	# full name is parent//child.
9	import Base
10	import ./text.bend as X
11	import ./glob.bend as G
12	import ./perm.bend as P
13	import ./rule_file.bend as F
14	import ./rule_capability.bend as RC
15	import ./rule_network.bend as RN
16	import ./rule_signal.bend as RS
17	import ./rule_ptrace.bend as RP
18	import ./rule_mount.bend as RM
19	import ./rule_dbus.bend as RD
20	import ./rule_change_profile.bend as RX
21	
22	# the profile modes of apparmor.d(5): enforce (the default), complain, kill,
23	# unconfined, default_allow, prompt
24	type AaMode is Data:
25	  AaModeEnforce{}
26	  AaModeComplain{}
27	  AaModeKill{}
28	  AaModeUnconfined{}
29	  AaModeDefaultAllow{}
30	  AaModePrompt{}
31	
32	type AaFlags is Data:
33	  AaFlags{mode: AaMode, audit: Bool}
34	
35	def AaFlags.default() -> AaFlags:
36	  AaFlags{AaModeEnforce{}, False{}}
37	
38	def AaFlags.mode(f: AaFlags) -> AaMode:
39	  match f:
40	    case AaFlags{m, a}:
41	      m
42	
43	def AaFlags.audit(f: AaFlags) -> Bool:
44	  match f:
45	    case AaFlags{m, a}:
46	      a
47	
48	def AaMode.show(m: AaMode) -> String:
49	  match m:
50	    case AaModeEnforce{}:
51	      "enforce"
52	    case AaModeComplain{}:
53	      "complain"
54	    case AaModeKill{}:
55	      "kill"
56	    case AaModeUnconfined{}:
57	      "unconfined"
58	    case AaModeDefaultAllow{}:
59	      "default_allow"
60	    case AaModePrompt{}:
61	      "prompt"
62	
63	# the modes in which an access no rule allows is refused
64	def AaMode.enforcing(m: AaMode) -> Bool:
65	  match m:
66	    case AaModeEnforce{}:
67	      True{}
68	    case AaModeKill{}:
69	      True{}
70	    case AaModePrompt{}:
71	      True{}
72	    case AaModeComplain{}:
73	      False{}
74	    case AaModeUnconfined{}:
75	      False{}
76	    case AaModeDefaultAllow{}:
77	      False{}
78	
79	def AaMode.is_complain(m: AaMode) -> Bool:
80	  match m:
81	    case AaModeComplain{}:
82	      True{}
83	    case _:
84	      False{}
85	
86	# The rules of a profile, by kind
87	
88	type AaRules is Data:
89	  AaRules{files: List<&2, F.AaFileRule>, caps: List<&2, RC.AaCapRule>, nets: List<&2, RN.AaNetRule>, signals: List<&2, RS.AaSignalRule>, ptraces: List<&2, RP.AaPtraceRule>, mounts: List<&2, RM.AaMountRule>, dbus: List<&2, RD.AaDbusRule>, changes: List<&2, RX.AaChangeRule>}
90	
91	def AaRules.empty() -> AaRules:
92	  AaRules{Nil{}, Nil{}, Nil{}, Nil{}, Nil{}, Nil{}, Nil{}, Nil{}}
93	
94	# the rules of a and of b
95	def AaRules.append(a: AaRules, b: AaRules) -> AaRules:
96	  match a b:
97	    case AaRules{f1, c1, n1, s1, p1, m1, d1, x1} AaRules{f2, c2, n2, s2, p2, m2, d2, x2}:
98	      AaRules{F.AaFileRule.append(f1, f2), RC.AaCapRule.append(c1, c2), RN.AaNetRule.append(n1, n2), RS.AaSignalRule.append(s1, s2), RP.AaPtraceRule.append(p1, p2), RM.AaMountRule.append(m1, m2), RD.AaDbusRule.append(d1, d2), RX.AaChangeRule.append(x1, x2)}
99	
100	def AaRules.files(r: AaRules) -> List<&2, F.AaFileRule>:
101	  match r:
102	    case AaRules{f, c, n, s, p, m, d, x}:
103	      f
104	
105	def AaRules.caps(r: AaRules) -> List<&2, RC.AaCapRule>:
106	  match r:
107	    case AaRules{f, c, n, s, p, m, d, x}:
108	      c
109	
110	def AaRules.nets(r: AaRules) -> List<&2, RN.AaNetRule>:
111	  match r:
112	    case AaRules{f, c, n, s, p, m, d, x}:
113	      n
114	
115	def AaRules.signals(r: AaRules) -> List<&2, RS.AaSignalRule>:
116	  match r:
117	    case AaRules{f, c, n, s, p, m, d, x}:
118	      s
119	
120	def AaRules.ptraces(r: AaRules) -> List<&2, RP.AaPtraceRule>:
121	  match r:
122	    case AaRules{f, c, n, s, p, m, d, x}:
123	      p
124	
125	def AaRules.mounts(r: AaRules) -> List<&2, RM.AaMountRule>:
126	  match r:
127	    case AaRules{f, c, n, s, p, m, d, x}:
128	      m
129	
130	def AaRules.dbus(r: AaRules) -> List<&2, RD.AaDbusRule>:
131	  match r:
132	    case AaRules{f, c, n, s, p, m, d, x}:
133	      d
134	
135	def AaRules.changes(r: AaRules) -> List<&2, RX.AaChangeRule>:
136	  match r:
137	    case AaRules{f, c, n, s, p, m, d, x}:
138	      x
139	
140	def AaRules.file(r: F.AaFileRule) -> AaRules:
141	  AaRules{[r], Nil{}, Nil{}, Nil{}, Nil{}, Nil{}, Nil{}, Nil{}}
142	
143	def AaRules.cap(r: RC.AaCapRule) -> AaRules:
144	  AaRules{Nil{}, [r], Nil{}, Nil{}, Nil{}, Nil{}, Nil{}, Nil{}}
145	
146	def AaRules.net(r: RN.AaNetRule) -> AaRules:
147	  AaRules{Nil{}, Nil{}, [r], Nil{}, Nil{}, Nil{}, Nil{}, Nil{}}
148	
149	def AaRules.signal(r: RS.AaSignalRule) -> AaRules:
150	  AaRules{Nil{}, Nil{}, Nil{}, [r], Nil{}, Nil{}, Nil{}, Nil{}}
151	
152	def AaRules.ptrace(r: RP.AaPtraceRule) -> AaRules:
153	  AaRules{Nil{}, Nil{}, Nil{}, Nil{}, [r], Nil{}, Nil{}, Nil{}}
154	
155	def AaRules.mount(r: RM.AaMountRule) -> AaRules:
156	  AaRules{Nil{}, Nil{}, Nil{}, Nil{}, Nil{}, [r], Nil{}, Nil{}}
157	
158	def AaRules.dbus_rule(r: RD.AaDbusRule) -> AaRules:
159	  AaRules{Nil{}, Nil{}, Nil{}, Nil{}, Nil{}, Nil{}, [r], Nil{}}
160	
161	def AaRules.change(r: RX.AaChangeRule) -> AaRules:
162	  AaRules{Nil{}, Nil{}, Nil{}, Nil{}, Nil{}, Nil{}, Nil{}, [r]}
163	
164	def AaRules.with_files(r: AaRules, fs: List<&2, F.AaFileRule>) -> AaRules:
165	  match r:
166	    case AaRules{f, c, n, s, p, m, d, x}:
167	      AaRules{fs, c, n, s, p, m, d, x}
168	
169	# Profiles
170	
171	type AaProfile is Data:
172	  AaProfile{name: List<&2, U32>, attach: Maybe<&2, G.AaGlob>, flags: AaFlags, rules: AaRules, children: List<&2, AaProfile>, hats: List<&2, AaProfile>}
173	
174	def AaProfile.name(p: AaProfile) -> List<&2, U32>:
175	  match p:
176	    case AaProfile{n, a, f, r, c, h}:
177	      n
178	
179	def AaProfile.attach(p: AaProfile) -> Maybe<&2, G.AaGlob>:
180	  match p:
181	    case AaProfile{n, a, f, r, c, h}:
182	      a
183	
184	def AaProfile.flags(p: AaProfile) -> AaFlags:
185	  match p:
186	    case AaProfile{n, a, f, r, c, h}:
187	      f
188	
189	def AaProfile.rules(p: AaProfile) -> AaRules:
190	  match p:
191	    case AaProfile{n, a, f, r, c, h}:
192	      r
193	
194	def AaProfile.children(p: AaProfile) -> List<&2, AaProfile>:
195	  match p:
196	    case AaProfile{n, a, f, r, c, h}:
197	      c
198	
199	def AaProfile.hats(p: AaProfile) -> List<&2, AaProfile>:
200	  match p:
201	    case AaProfile{n, a, f, r, c, h}:
202	      h
203	
204	# a profile with no rules, children or hats
205	def AaProfile.new(n: List<&2, U32>, a: Maybe<&2, G.AaGlob>, f: AaFlags) -> AaProfile:
206	  AaProfile{n, a, f, AaRules.empty(), Nil{}, Nil{}}
207	
208	def AaProfile.with_flags(p: AaProfile, f: AaFlags) -> AaProfile:
209	  match p:
210	    case AaProfile{n, a, f0, r, c, h}:
211	      AaProfile{n, a, f, r, c, h}
212	
213	# p with the rules r added: what an include of rules r into p does
214	def AaProfile.include(p: AaProfile, r: AaRules) -> AaProfile:
215	  match p:
216	    case AaProfile{n, a, f, r0, c, h}:
217	      AaProfile{n, a, f, AaRules.append(r0, r), c, h}
218	
219	def AaProfile.list_append(xs: List<&2, AaProfile>, ys: List<&2, AaProfile>) -> List<&2, AaProfile>:
220	  match xs:
221	    case Nil{}:
222	      ys
223	    case Con{h, t}:
224	      Con{h, AaProfile.list_append(t, ys)}
225	
226	# p with the rules r put first (the order of rules does not matter; this is
227	# what loading uses, in time proportional to r)
228	def AaProfile.prepend(p: AaProfile, r: AaRules) -> AaProfile:
229	  match p:
230	    case AaProfile{n, a, f, r0, c, h}:
231	      AaProfile{n, a, f, AaRules.append(r, r0), c, h}
232	
233	def AaProfile.add_child(p: AaProfile, k: AaProfile) -> AaProfile:
234	  match p:
235	    case AaProfile{n, a, f, r, c, h}:
236	      AaProfile{n, a, f, r, AaProfile.list_append(c, [k]), h}
237	
238	def AaProfile.add_hat(p: AaProfile, k: AaProfile) -> AaProfile:
239	  match p:
240	    case AaProfile{n, a, f, r, c, h}:
241	      AaProfile{n, a, f, r, c, AaProfile.list_append(h, [k])}
242	
243	def AaProfile.find.go(hit: Bool, p: AaProfile, rest: Maybe<&2, AaProfile>) -> Maybe<&2, AaProfile>:
244	  match hit:
245	    case True{}:
246	      Some{p}
247	    case False{}:
248	      rest
249	
250	# the profile of the list named n
251	def AaProfile.find(ps: List<&2, AaProfile>, +n: List<&2, U32>) -> Maybe<&2, AaProfile>:
252	  match ps:
253	    case Nil{}:
254	      None{}
255	    case Con{+p, t}:
256	      AaProfile.find.go(X.AaText.eq(AaProfile.name(p), n), p, AaProfile.find(t, n))
257	
258	# A policy: the top-level profiles of a namespace
259	
260	type AaPolicy is Data:
261	  AaPolicy{profiles: List<&2, AaProfile>}
262	
263	def AaPolicy.profiles(p: AaPolicy) -> List<&2, AaProfile>:
264	  match p:
265	    case AaPolicy{ps}:
266	      ps
267	
268	# the child or hat named by the rest of a full name
269	def AaProfile.descend(fuel: Nat, m: Maybe<&2, AaProfile>, rest: Maybe<&2, X.AaSplit>) -> Maybe<&2, AaProfile>:
270	  match fuel:
271	    case 0n:
272	      None{}
273	    case 1n+f:
274	      match m:
275	        case None{}:
276	          None{}
277	        case Some{+p}:
278	          match rest:
279	            case None{}:
280	              Some{p}
281	            case Some{sp}:
282	              match sp:
283	                case X.AaSplit{first, more}:
284	                  AaProfile.descend(f, AaProfile.find(AaProfile.list_append(AaProfile.children(p), AaProfile.hats(p)), first), X.AaText.split2.opt(more))
285	
286	def AaPolicy.lookup.go(s: X.AaSplit, ps: List<&2, AaProfile>, fuel: Nat) -> Maybe<&2, AaProfile>:
287	  match s:
288	    case X.AaSplit{first, more}:
289	      AaProfile.descend(fuel, AaProfile.find(ps, first), X.AaText.split2.opt(more))
290	
291	# the profile with the full name n (a, a//b, a//b//c, ...)
292	def AaPolicy.lookup(pol: AaPolicy, +n: List<&2, U32>) -> Maybe<&2, AaProfile>:
293	  AaPolicy.lookup.go(X.AaText.split2(n), AaPolicy.profiles(pol), 1n+X.AaText.len(n))