LAWS.bend

bend-osdev-apparmor@0.1.0.0 · 299 lines · 51 definitions

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.
26import Base
27import bend-osdev-apparmor@0.1.0.0/text.bend as X
28import bend-osdev-apparmor@0.1.0.0/glob.bend as G
29import bend-osdev-apparmor@0.1.0.0/perm.bend as P
30import bend-osdev-apparmor@0.1.0.0/options.bend as O
31import bend-osdev-apparmor@0.1.0.0/profile.bend as PR
32import bend-osdev-apparmor@0.1.0.0/eval.bend as V
33import bend-osdev-apparmor@0.1.0.0/transitions.bend as TR
34import bend-osdev-apparmor@0.1.0.0/rule_file.bend as F
35import bend-osdev-apparmor@0.1.0.0/rule_capability.bend as RC
36import bend-osdev-apparmor@0.1.0.0/rule_network.bend as RN
37import bend-osdev-apparmor@0.1.0.0/rule_signal.bend as RS
38import bend-osdev-apparmor@0.1.0.0/rule_ptrace.bend as RP
39import bend-osdev-apparmor@0.1.0.0/rule_mount.bend as RM
40import bend-osdev-apparmor@0.1.0.0/rule_dbus.bend as RD
41import bend-osdev-apparmor@0.1.0.0/rule_change_profile.bend as RX
42import bend-osdev-apparmor@0.1.0.0/example.bend as EX
43
44# Globs
45
46law 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
51law 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
56law 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
61law 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
68law 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
72law 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
81law 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
89law 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
97law 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
108law 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
116law 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
127law 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
134law 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
141law 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
148law 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
155law 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
162law 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
169law 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
176law 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
185law 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
201law 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
204law 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
207law 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
210law 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
213law 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
216law 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
219law 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
222law 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
225law 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
228law 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
231law 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
234law 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
237law 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
240law 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
245law glob_star_not_empty_segment:
246  {G.AaGlob.match_text(X.AaText.of_string("/tmp/*"), X.AaText.of_string("/tmp/")) == False{} : Bool}
247
248law glob_star_file:
249  {G.AaGlob.match_text(X.AaText.of_string("/tmp/*"), X.AaText.of_string("/tmp/x")) == True{} : Bool}
250
251law glob_star_no_slash:
252  {G.AaGlob.match_text(X.AaText.of_string("/tmp/*"), X.AaText.of_string("/tmp/x/y")) == False{} : Bool}
253
254law glob_star2_not_dir_itself:
255  {G.AaGlob.match_text(X.AaText.of_string("/tmp/**"), X.AaText.of_string("/tmp/")) == False{} : Bool}
256
257law glob_star2_deep:
258  {G.AaGlob.match_text(X.AaText.of_string("/tmp/**"), X.AaText.of_string("/tmp/a/b/")) == True{} : Bool}
259
260law glob_star_inside_segment:
261  {G.AaGlob.match_text(X.AaText.of_string("/a/*b"), X.AaText.of_string("/a/b")) == True{} : Bool}
262
263law glob_star_in_braces:
264  {G.AaGlob.match_text(X.AaText.of_string("/a/{b,*}"), X.AaText.of_string("/a/")) == True{} : Bool}
265
266law 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
269law glob_slashes_collapse:
270  {G.AaGlob.match_text(X.AaText.of_string("/a//b"), X.AaText.of_string("/a/b")) == True{} : Bool}
271
272law 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
275law 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
278law 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
281law glob_one_alternative_rejected:
282  {G.AaGlob.parse(X.AaText.of_string("/a/{b}")) == None{} : Maybe<&2, G.AaGlob>}
283
284law glob_trailing_dash_rejected:
285  {G.AaGlob.parse(X.AaText.of_string("/a/[a-]")) == None{} : Maybe<&2, G.AaGlob>}
286
287law 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
295law 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
298law 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>}