1	# Properties, for every input:
2	#   globs: the backtracking matcher agrees with the list model (a path
3	#     matches a pattern when it can be cut into one piece per pattern
4	#     element, each piece matching its element), and the fast matcher (a set
5	#     of active positions moved a byte at a time) with the backtracking one,
6	#     for every sequence, pattern and path;
7	#   the decision engine (eval.bend), for every set of matching rules (their
8	#     grants), every request, mode and option:
9	#     what is granted never includes what is denied;
10	#     a deny rule that meets the request wins, in every mode where deny
11	#       rules apply (all but unconfined, and complain only with
12	#       complain_deny);
13	#     a request no rule matches is denied in enforcing modes (enforce,
14	#       kill, prompt);
15	#     complain mode allows exactly what no applicable deny rule refuses, so
16	#       with complain_deny off it never denies;
17	#   the same for file rules on a profile: a deny rule meeting the request
18	#     wins, a path no rule matches is denied;
19	#   include is idempotent: adding a set of rules to a profile twice decides
20	#     every request of every kind as adding it once;
21	#   an exec the profile does not grant x for fails.
22	#
23	# Witnesses: each hypothesis above holds for some input (the *_sat laws).
24	# Vectors: globs as apparmor_parser compiles them (see the README,
25	# "Experiments"), and decisions on a small policy.
26	import Base
27	import ./text.bend as X
28	import ./glob.bend as G
29	import ./perm.bend as P
30	import ./options.bend as O
31	import ./profile.bend as PR
32	import ./eval.bend as V
33	import ./transitions.bend as TR
34	import ./rule_file.bend as F
35	import ./rule_capability.bend as RC
36	import ./rule_network.bend as RN
37	import ./rule_signal.bend as RS
38	import ./rule_ptrace.bend as RP
39	import ./rule_mount.bend as RM
40	import ./rule_dbus.bend as RD
41	import ./rule_change_profile.bend as RX
42	import ./example.bend as EX
43	
44	# Globs
45	
46	law glob_seq_model:
47	  for seq: List<&2, G.AaGTok>
48	  for s: List<&2, U32>
49	  {G.AaGSeq.matches(seq, s) == G.AaGSeq.model(seq, s) : Bool}
50	
51	law glob_run:
52	  for seq: List<&2, G.AaGTok>
53	  for s: List<&2, U32>
54	  {G.AaGSeq.run(seq, s) == G.AaGSeq.matches(seq, s) : Bool}
55	
56	law glob_model:
57	  for g: G.AaGlob
58	  for s: List<&2, U32>
59	  {G.AaGlob.matches(g, s) == G.AaGlob.model(g, s) : Bool}
60	
61	law glob_ref_model:
62	  for g: G.AaGlob
63	  for s: List<&2, U32>
64	  {G.AaGlob.matches_ref(g, s) == G.AaGlob.model(g, s) : Bool}
65	
66	# The decision engine
67	
68	law granted_never_denied:
69	  for gs: List<&2, P.AaGrant>
70	  {P.AaPerms.meets(V.AaEval.granted(gs), V.AaEval.denied(gs)) == False{} : Bool}
71	
72	law deny_wins:
73	  for opts: O.AaOptions
74	  for gs: List<&2, P.AaGrant>
75	  for flags: PR.AaFlags
76	  for req: P.AaPerms
77	  for h1: {V.AaEval.deny_applies(opts, PR.AaFlags.mode(flags)) == True{} : Bool}
78	  for h2: {P.AaPerms.meets(req, V.AaEval.denied(gs)) == True{} : Bool}
79	  {V.AaDecision.allowed(V.AaEval.decide(opts, flags, req, gs)) == False{} : Bool}
80	
81	law unmatched_denied:
82	  for opts: O.AaOptions
83	  for flags: PR.AaFlags
84	  for req: P.AaPerms
85	  for h1: {PR.AaMode.enforcing(PR.AaFlags.mode(flags)) == True{} : Bool}
86	  for h2: {P.AaPerms.any(req) == True{} : Bool}
87	  {V.AaDecision.allowed(V.AaEval.decide(opts, flags, req, Nil{})) == False{} : Bool}
88	
89	law complain_decided_by_deny:
90	  for opts: O.AaOptions
91	  for flags: PR.AaFlags
92	  for req: P.AaPerms
93	  for gs: List<&2, P.AaGrant>
94	  for h: {PR.AaMode.is_complain(PR.AaFlags.mode(flags)) == True{} : Bool}
95	  {V.AaDecision.allowed(V.AaEval.decide(opts, flags, req, gs)) == Bool.not(Bool.and(O.AaOptions.complain_deny(opts), P.AaPerms.meets(req, V.AaEval.denied(gs)))) : Bool}
96	
97	law complain_never_denies:
98	  for opts: O.AaOptions
99	  for flags: PR.AaFlags
100	  for req: P.AaPerms
101	  for gs: List<&2, P.AaGrant>
102	  for h1: {O.AaOptions.complain_deny(opts) == False{} : Bool}
103	  for h2: {PR.AaMode.is_complain(PR.AaFlags.mode(flags)) == True{} : Bool}
104	  {V.AaDecision.allowed(V.AaEval.decide(opts, flags, req, gs)) == True{} : Bool}
105	
106	# File rules on a profile
107	
108	law file_deny_wins:
109	  for opts: O.AaOptions
110	  for p: PR.AaProfile
111	  for q: F.AaFileQuery
112	  for h1: {V.AaEval.deny_applies(opts, PR.AaFlags.mode(PR.AaProfile.flags(p))) == True{} : Bool}
113	  for h2: {P.AaPerms.meets(F.AaFileQuery.req(q), V.AaEval.denied(F.AaFileRule.grants(PR.AaRules.files(PR.AaProfile.rules(p)), q))) == True{} : Bool}
114	  {V.AaDecision.allowed(V.AaEval.file(opts, p, q)) == False{} : Bool}
115	
116	law file_unmatched_denied:
117	  for opts: O.AaOptions
118	  for p: PR.AaProfile
119	  for q: F.AaFileQuery
120	  for h1: {PR.AaMode.enforcing(PR.AaFlags.mode(PR.AaProfile.flags(p))) == True{} : Bool}
121	  for h2: {F.AaFileRule.matching(PR.AaRules.files(PR.AaProfile.rules(p)), q) == Nil{} : List<&2, F.AaFileRule>}
122	  for h3: {P.AaPerms.any(F.AaFileQuery.req(q)) == True{} : Bool}
123	  {V.AaDecision.allowed(V.AaEval.file(opts, p, q)) == False{} : Bool}
124	
125	# Include is idempotent, for every kind of rule
126	
127	law include_idempotent_file:
128	  for opts: O.AaOptions
129	  for p: PR.AaProfile
130	  for r: PR.AaRules
131	  for q: F.AaFileQuery
132	  {V.AaEval.file(opts, PR.AaProfile.include(PR.AaProfile.include(p, r), r), q) == V.AaEval.file(opts, PR.AaProfile.include(p, r), q) : V.AaDecision}
133	
134	law include_idempotent_capability:
135	  for opts: O.AaOptions
136	  for p: PR.AaProfile
137	  for r: PR.AaRules
138	  for q: RC.AaCapQuery
139	  {V.AaEval.capability(opts, PR.AaProfile.include(PR.AaProfile.include(p, r), r), q) == V.AaEval.capability(opts, PR.AaProfile.include(p, r), q) : V.AaDecision}
140	
141	law include_idempotent_network:
142	  for opts: O.AaOptions
143	  for p: PR.AaProfile
144	  for r: PR.AaRules
145	  for q: RN.AaNetQuery
146	  {V.AaEval.network(opts, PR.AaProfile.include(PR.AaProfile.include(p, r), r), q) == V.AaEval.network(opts, PR.AaProfile.include(p, r), q) : V.AaDecision}
147	
148	law include_idempotent_signal:
149	  for opts: O.AaOptions
150	  for p: PR.AaProfile
151	  for r: PR.AaRules
152	  for q: RS.AaSignalQuery
153	  {V.AaEval.signal(opts, PR.AaProfile.include(PR.AaProfile.include(p, r), r), q) == V.AaEval.signal(opts, PR.AaProfile.include(p, r), q) : V.AaDecision}
154	
155	law include_idempotent_ptrace:
156	  for opts: O.AaOptions
157	  for p: PR.AaProfile
158	  for r: PR.AaRules
159	  for q: RP.AaPtraceQuery
160	  {V.AaEval.ptrace(opts, PR.AaProfile.include(PR.AaProfile.include(p, r), r), q) == V.AaEval.ptrace(opts, PR.AaProfile.include(p, r), q) : V.AaDecision}
161	
162	law include_idempotent_mount:
163	  for opts: O.AaOptions
164	  for p: PR.AaProfile
165	  for r: PR.AaRules
166	  for q: RM.AaMountQuery
167	  {V.AaEval.mount(opts, PR.AaProfile.include(PR.AaProfile.include(p, r), r), q) == V.AaEval.mount(opts, PR.AaProfile.include(p, r), q) : V.AaDecision}
168	
169	law include_idempotent_dbus:
170	  for opts: O.AaOptions
171	  for p: PR.AaProfile
172	  for r: PR.AaRules
173	  for q: RD.AaDbusQuery
174	  {V.AaEval.dbus(opts, PR.AaProfile.include(PR.AaProfile.include(p, r), r), q) == V.AaEval.dbus(opts, PR.AaProfile.include(p, r), q) : V.AaDecision}
175	
176	law include_idempotent_change_profile:
177	  for opts: O.AaOptions
178	  for p: PR.AaProfile
179	  for r: PR.AaRules
180	  for q: RX.AaChangeQuery
181	  {V.AaEval.change_profile(opts, PR.AaProfile.include(PR.AaProfile.include(p, r), r), q) == V.AaEval.change_profile(opts, PR.AaProfile.include(p, r), q) : V.AaDecision}
182	
183	# Exec
184	
185	law exec_needs_x:
186	  for opts: O.AaOptions
187	  for pol: PR.AaPolicy
188	  for name: List<&2, U32>
189	  for owner: Bool
190	  for path: List<&2, U32>
191	  for p: PR.AaProfile
192	  for h1: {PR.AaPolicy.lookup(pol, name) == Some{p} : Maybe<&2, PR.AaProfile>}
193	  for h2: {TR.AaTrans.is_unconfined(PR.AaFlags.mode(PR.AaProfile.flags(p))) == False{} : Bool}
194	  for h3: {V.AaDecision.allowed(V.AaEval.file(opts, p, F.AaFileQuery{path, owner, P.AaPerms.bit(6n)})) == False{} : Bool}
195	  {TR.AaExecResult.ok(TR.AaTrans.exec(opts, pol, name, owner, path)) == False{} : Bool}
196	
197	# Witnesses: the hypotheses of the laws above hold for some input (the
198	# example profile ex of example.bend: /etc/x rw, deny /etc/x w, audit
199	# /var/log/x w, /lib/** r, no exec rule)
200	
201	law deny_wins_sat:
202	  {Bool.and(V.AaEval.deny_applies(O.AaOptions.default(), PR.AaFlags.mode(PR.AaProfile.flags(EX.AaExample.profile(PR.AaModeEnforce{})))), P.AaPerms.meets(F.AaFileQuery.req(EX.AaExample.query("/etc/x", "w")), V.AaEval.denied(F.AaFileRule.grants(PR.AaRules.files(PR.AaProfile.rules(EX.AaExample.profile(PR.AaModeEnforce{}))), EX.AaExample.query("/etc/x", "w"))))) == True{} : Bool}
203	
204	law deny_wins_example:
205	  {V.AaEval.file(O.AaOptions.default(), EX.AaExample.profile(PR.AaModeEnforce{}), EX.AaExample.query("/etc/x", "w")) == V.AaDeny{False{}} : V.AaDecision}
206	
207	law allow_example:
208	  {V.AaEval.file(O.AaOptions.default(), EX.AaExample.profile(PR.AaModeEnforce{}), EX.AaExample.query("/etc/x", "r")) == V.AaAllow{} : V.AaDecision}
209	
210	law audit_example:
211	  {V.AaEval.file(O.AaOptions.default(), EX.AaExample.profile(PR.AaModeEnforce{}), EX.AaExample.query("/var/log/x", "w")) == V.AaAudit{} : V.AaDecision}
212	
213	law unmatched_sat:
214	  {Bool.and(PR.AaMode.enforcing(PR.AaFlags.mode(PR.AaProfile.flags(EX.AaExample.profile(PR.AaModeEnforce{})))), P.AaPerms.any(F.AaFileQuery.req(EX.AaExample.query("/etc/y", "r")))) == True{} : Bool}
215	
216	law file_unmatched_sat:
217	  {F.AaFileRule.matching(PR.AaRules.files(PR.AaProfile.rules(EX.AaExample.profile(PR.AaModeEnforce{}))), EX.AaExample.query("/etc/y", "r")) == Nil{} : List<&2, F.AaFileRule>}
218	
219	law unmatched_example:
220	  {V.AaEval.file(O.AaOptions.default(), EX.AaExample.profile(PR.AaModeEnforce{}), EX.AaExample.query("/etc/y", "r")) == V.AaDeny{True{}} : V.AaDecision}
221	
222	law complain_sat:
223	  {Bool.and(PR.AaMode.is_complain(PR.AaFlags.mode(PR.AaProfile.flags(EX.AaExample.profile(PR.AaModeComplain{})))), Bool.not(O.AaOptions.complain_deny(O.AaOptions.with_complain_deny(O.AaOptions.default(), False{})))) == True{} : Bool}
224	
225	law complain_example_unmatched:
226	  {V.AaEval.file(O.AaOptions.default(), EX.AaExample.profile(PR.AaModeComplain{}), EX.AaExample.query("/etc/y", "r")) == V.AaComplain{} : V.AaDecision}
227	
228	law complain_example_deny_rule:
229	  {V.AaEval.file(O.AaOptions.default(), EX.AaExample.profile(PR.AaModeComplain{}), EX.AaExample.query("/etc/x", "w")) == V.AaDeny{False{}} : V.AaDecision}
230	
231	law complain_example_no_deny:
232	  {V.AaEval.file(O.AaOptions.with_complain_deny(O.AaOptions.default(), False{}), EX.AaExample.profile(PR.AaModeComplain{}), EX.AaExample.query("/etc/x", "w")) == V.AaComplain{} : V.AaDecision}
233	
234	law kill_example:
235	  {V.AaEval.file(O.AaOptions.default(), EX.AaExample.profile(PR.AaModeKill{}), EX.AaExample.query("/etc/y", "r")) == V.AaKill{} : V.AaDecision}
236	
237	law exec_needs_x_sat:
238	  {PR.AaPolicy.lookup(EX.AaExample.policy(), X.AaText.of_string("ex")) == Some{EX.AaExample.profile(PR.AaModeEnforce{})} : Maybe<&2, PR.AaProfile>}
239	
240	law exec_needs_x_sat2:
241	  {Bool.and(Bool.not(TR.AaTrans.is_unconfined(PR.AaFlags.mode(PR.AaProfile.flags(EX.AaExample.profile(PR.AaModeEnforce{}))))), Bool.not(V.AaDecision.allowed(V.AaEval.file(O.AaOptions.default(), EX.AaExample.profile(PR.AaModeEnforce{}), F.AaFileQuery{X.AaText.of_string("/bin/sh"), False{}, P.AaPerms.bit(6n)})))) == True{} : Bool}
242	
243	# Vectors: globs, as apparmor_parser 4.0.1 compiles them
244	
245	law glob_star_not_empty_segment:
246	  {G.AaGlob.match_text(X.AaText.of_string("/tmp/*"), X.AaText.of_string("/tmp/")) == False{} : Bool}
247	
248	law glob_star_file:
249	  {G.AaGlob.match_text(X.AaText.of_string("/tmp/*"), X.AaText.of_string("/tmp/x")) == True{} : Bool}
250	
251	law glob_star_no_slash:
252	  {G.AaGlob.match_text(X.AaText.of_string("/tmp/*"), X.AaText.of_string("/tmp/x/y")) == False{} : Bool}
253	
254	law glob_star2_not_dir_itself:
255	  {G.AaGlob.match_text(X.AaText.of_string("/tmp/**"), X.AaText.of_string("/tmp/")) == False{} : Bool}
256	
257	law glob_star2_deep:
258	  {G.AaGlob.match_text(X.AaText.of_string("/tmp/**"), X.AaText.of_string("/tmp/a/b/")) == True{} : Bool}
259	
260	law glob_star_inside_segment:
261	  {G.AaGlob.match_text(X.AaText.of_string("/a/*b"), X.AaText.of_string("/a/b")) == True{} : Bool}
262	
263	law glob_star_in_braces:
264	  {G.AaGlob.match_text(X.AaText.of_string("/a/{b,*}"), X.AaText.of_string("/a/")) == True{} : Bool}
265	
266	law glob_negated_class_slash:
267	  {G.AaGlob.match_text(X.AaText.of_string("/a/[^b]c"), X.AaText.of_string("/a//c")) == True{} : Bool}
268	
269	law glob_slashes_collapse:
270	  {G.AaGlob.match_text(X.AaText.of_string("/a//b"), X.AaText.of_string("/a/b")) == True{} : Bool}
271	
272	law glob_class_range:
273	  {Bool.and(G.AaGlob.match_text(X.AaText.of_string("/a/[a-c]x"), X.AaText.of_string("/a/bx")), Bool.not(G.AaGlob.match_text(X.AaText.of_string("/a/[a-c]x"), X.AaText.of_string("/a/dx")))) == True{} : Bool}
274	
275	law glob_nested_braces:
276	  {G.AaGlob.match_text(X.AaText.of_string("/a/{b,c{d,e}}"), X.AaText.of_string("/a/ce")) == True{} : Bool}
277	
278	law glob_question:
279	  {Bool.and(G.AaGlob.match_text(X.AaText.of_string("/a/?b"), X.AaText.of_string("/a/xb")), Bool.not(G.AaGlob.match_text(X.AaText.of_string("/a/?b"), X.AaText.of_string("/a//b")))) == True{} : Bool}
280	
281	law glob_one_alternative_rejected:
282	  {G.AaGlob.parse(X.AaText.of_string("/a/{b}")) == None{} : Maybe<&2, G.AaGlob>}
283	
284	law glob_trailing_dash_rejected:
285	  {G.AaGlob.parse(X.AaText.of_string("/a/[a-]")) == None{} : Maybe<&2, G.AaGlob>}
286	
287	law glob_empty_class_rejected:
288	  {G.AaGlob.parse(X.AaText.of_string("/a/[]]")) == None{} : Maybe<&2, G.AaGlob>}
289	
290	# Vectors: a small policy text (AaExample.small_files: a tunable, an
291	# abstraction included twice, a deny rule, a variable, a px exec into a
292	# complain-mode profile), loaded and asked. (The larger example policy is
293	# in check.bend: the --verdict kernel runs out of fuel parsing it.)
294	
295	law policy_file_vectors:
296	  {[EX.AaExample.small_file("/usr/bin/foo", "/lib/x/y.so", "mr"), EX.AaExample.small_file("/usr/bin/foo", "/etc/shadow", "r"), EX.AaExample.small_file("/usr/bin/foo", "/home/al/f", "rw"), EX.AaExample.small_file("/usr/bin/foo", "/root/f", "a"), EX.AaExample.small_file("/usr/bin/foo", "/etc/x", "r"), EX.AaExample.small_file("bar", "/etc/x", "r")] == [Some{V.AaAllow{}}, Some{V.AaDeny{False{}}}, Some{V.AaAllow{}}, Some{V.AaAllow{}}, Some{V.AaDeny{True{}}}, Some{V.AaComplain{}}] : List<&2, Maybe<&2, V.AaDecision>>}
297	
298	law policy_exec_vectors:
299	  {[EX.AaExample.small_exec("/usr/bin/foo", "/bin/x"), EX.AaExample.small_exec("/usr/bin/foo", "/bin/y")] == ["profile bar", "denied (deny)"] : List<&2, String>}