LAWS.bend

bend-osdev-caps@0.1.0.0 · 299 lines · 40 definitions

1# Properties, for every input (every kernel parameter record, credential,
2# file and request):
3#   execve: the effective set ends within the permitted set, and the ambient
4#     set within the permitted set and (when it was before) the inheritable
5#     set; the bounding and inheritable sets are unchanged; the new permitted
6#     set is within the old bounding, inheritable and ambient sets (so a
7#     capability in none of them never becomes permitted); the documented
8#     root and non-root simplifications; execve answers either
9#     CapsCapabilityDumb or exactly the transformed sets.
10#   capset: the permitted set never grows, the bounding set is unchanged, and
11#     the invariants (effective within permitted, ambient within permitted
12#     and inheritable) hold afterwards.
13#   PR_CAPBSET_DROP: the bounding set never grows, and nothing else changes.
14#   PR_CAP_AMBIENT: raising and lowering keep the invariants and change no
15#   other set; clearing empties the ambient set.
16#
17# Vectors: capability names and numbers, the text form of a set, and the
18# documented cases of capabilities(7) on concrete credentials.
19import Base
20import bend-osdev-caps@0.1.0.0/caps.bend as C
21import bend-osdev-caps@0.1.0.0/exec.bend as E
22import bend-osdev-caps@0.1.0.0/adjust.bend as A
23
24# execve(2)
25
26law execve_result:
27  for +k: C.CapsKernel
28  for +c: C.CapCred
29  for +f: C.CapFile
30  for +ign: Bool
31  {C.Caps.sets_or(E.Caps.execve(k, c, f, ign), E.Caps.execve.sets(k, c, f, ign)) == E.Caps.execve.sets(k, c, f, ign) : C.CapState}
32
33law execve_effective_within_permitted:
34  for +k: C.CapsKernel
35  for +c: C.CapCred
36  for +f: C.CapFile
37  for +ign: Bool
38  {C.CapSet.subset(C.CapState.effective(E.Caps.execve.sets(k, c, f, ign)), C.CapState.permitted(E.Caps.execve.sets(k, c, f, ign))) == True{} : Bool}
39
40law execve_ambient_within_permitted:
41  for +k: C.CapsKernel
42  for +c: C.CapCred
43  for +f: C.CapFile
44  for +ign: Bool
45  {C.CapSet.subset(C.CapState.ambient(E.Caps.execve.sets(k, c, f, ign)), C.CapState.permitted(E.Caps.execve.sets(k, c, f, ign))) == True{} : Bool}
46
47law execve_ambient_within_inheritable:
48  for +k: C.CapsKernel
49  for +c: C.CapCred
50  for +f: C.CapFile
51  for +ign: Bool
52  for h: {C.CapSet.subset(C.CapState.ambient(C.CapCred.sets(c)), C.CapState.inheritable(C.CapCred.sets(c))) == True{} : Bool}
53  {C.CapSet.subset(C.CapState.ambient(E.Caps.execve.sets(k, c, f, ign)), C.CapState.inheritable(E.Caps.execve.sets(k, c, f, ign))) == True{} : Bool}
54
55law execve_valid:
56  for +k: C.CapsKernel
57  for +c: C.CapCred
58  for +f: C.CapFile
59  for +ign: Bool
60  for h: {C.CapState.valid(C.CapCred.sets(c)) == True{} : Bool}
61  {C.CapState.valid(E.Caps.execve.sets(k, c, f, ign)) == True{} : Bool}
62
63law execve_bounding_unchanged:
64  for +k: C.CapsKernel
65  for +c: C.CapCred
66  for +f: C.CapFile
67  for +ign: Bool
68  {C.CapState.bounding(E.Caps.execve.sets(k, c, f, ign)) == C.CapState.bounding(C.CapCred.sets(c)) : C.CapSet()}
69
70law execve_inheritable_unchanged:
71  for +k: C.CapsKernel
72  for +c: C.CapCred
73  for +f: C.CapFile
74  for +ign: Bool
75  {C.CapState.inheritable(E.Caps.execve.sets(k, c, f, ign)) == C.CapState.inheritable(C.CapCred.sets(c)) : C.CapSet()}
76
77# a capability that is in none of the bounding, inheritable and ambient sets
78# never becomes permitted (the bounding set does not mask the inheritable
79# set: capabilities(7), "Capability bounding set")
80law execve_permitted_bounded:
81  for +k: C.CapsKernel
82  for +c: C.CapCred
83  for +f: C.CapFile
84  for +ign: Bool
85  {C.CapSet.subset(C.CapState.permitted(E.Caps.execve.sets(k, c, f, ign)), C.CapSet.union(C.CapState.bounding(C.CapCred.sets(c)), C.CapSet.union(C.CapState.inheritable(C.CapCred.sets(c)), C.CapState.ambient(C.CapCred.sets(c))))) == True{} : Bool}
86
87# with the ambient invariant, the bound is the bounding and inheritable sets
88law execve_permitted_bounded_valid:
89  for +k: C.CapsKernel
90  for +c: C.CapCred
91  for +f: C.CapFile
92  for +ign: Bool
93  for h: {C.CapSet.subset(C.CapState.ambient(C.CapCred.sets(c)), C.CapState.inheritable(C.CapCred.sets(c))) == True{} : Bool}
94  {C.CapSet.subset(C.CapState.permitted(E.Caps.execve.sets(k, c, f, ign)), C.CapSet.union(C.CapState.bounding(C.CapCred.sets(c)), C.CapState.inheritable(C.CapCred.sets(c)))) == True{} : Bool}
95
96# "when a process whose real and effective UIDs are zero execve(2)s a
97# program": P'(permitted) = P(inheritable) | P(bounding), and
98# P'(effective) = P'(permitted). For every state with the ambient invariant,
99# every file that is not set-user-ID, without SECBIT_NOROOT.
100law execve_root_permitted:
101  for +k: C.CapsKernel
102  for +s: C.CapState
103  for +sv: U32
104  for +na: Bool
105  for +u: U32
106  for +sg: Bool
107  for +fc: Maybe<&2, C.CapFileSets>
108  for +ign: Bool
109  for h: {C.CapSet.subset(C.CapState.ambient(s), C.CapState.inheritable(s)) == True{} : Bool}
110  {C.CapState.permitted(E.Caps.execve.sets(k, C.CapCred{0, 0, sv, False{}, na, s}, C.CapFile{u, False{}, sg, fc}, ign)) == C.CapSet.union(C.CapState.inheritable(s), C.CapState.bounding(s)) : C.CapSet()}
111
112law execve_root_effective:
113  for +k: C.CapsKernel
114  for +s: C.CapState
115  for +sv: U32
116  for +na: Bool
117  for +u: U32
118  for +sg: Bool
119  for +fc: Maybe<&2, C.CapFileSets>
120  for +ign: Bool
121  for h: {C.CapSet.subset(C.CapState.ambient(s), C.CapState.inheritable(s)) == True{} : Bool}
122  {C.CapState.effective(E.Caps.execve.sets(k, C.CapCred{0, 0, sv, False{}, na, s}, C.CapFile{u, False{}, sg, fc}, ign)) == C.CapSet.union(C.CapState.inheritable(s), C.CapState.bounding(s)) : C.CapSet()}
123
124# "if a process with nonzero user IDs performs an execve(2) then any
125# capabilities that are present in its permitted and effective sets will be
126# cleared": of a file without set-ID bits or capabilities, only the ambient
127# set remains, as both permitted and effective.
128law execve_nonroot_permitted:
129  for +k: C.CapsKernel
130  for +r: U32
131  for +e: U32
132  for hr: {U32.is_eq(r, 0) == False{} : Bool}
133  for he: {U32.is_eq(e, 0) == False{} : Bool}
134  for +s: C.CapState
135  for +sv: U32
136  for +nr: Bool
137  for +na: Bool
138  for +u: U32
139  for +ign: Bool
140  {C.CapState.permitted(E.Caps.execve.sets(k, C.CapCred{r, e, sv, nr, na, s}, C.CapFile{u, False{}, False{}, None{}}, ign)) == C.CapState.ambient(s) : C.CapSet()}
141
142law execve_nonroot_effective:
143  for +k: C.CapsKernel
144  for +r: U32
145  for +e: U32
146  for hr: {U32.is_eq(r, 0) == False{} : Bool}
147  for he: {U32.is_eq(e, 0) == False{} : Bool}
148  for +s: C.CapState
149  for +sv: U32
150  for +nr: Bool
151  for +na: Bool
152  for +u: U32
153  for +ign: Bool
154  {C.CapState.effective(E.Caps.execve.sets(k, C.CapCred{r, e, sv, nr, na, s}, C.CapFile{u, False{}, False{}, None{}}, ign)) == C.CapState.ambient(s) : C.CapSet()}
155
156# capset(2)
157
158law capset_permitted_never_grows:
159  for +c: C.CapCred
160  for +e: C.CapSet()
161  for +p: C.CapSet()
162  for +i: C.CapSet()
163  {C.CapSet.subset(C.CapState.permitted(C.CapCred.sets(C.Caps.or(A.Caps.capset(c, e, p, i), c))), C.CapState.permitted(C.CapCred.sets(c))) == True{} : Bool}
164
165law capset_bounding_unchanged:
166  for +c: C.CapCred
167  for +e: C.CapSet()
168  for +p: C.CapSet()
169  for +i: C.CapSet()
170  {C.CapState.bounding(C.CapCred.sets(C.Caps.or(A.Caps.capset(c, e, p, i), c))) == C.CapState.bounding(C.CapCred.sets(c)) : C.CapSet()}
171
172law capset_valid:
173  for +c: C.CapCred
174  for +e: C.CapSet()
175  for +p: C.CapSet()
176  for +i: C.CapSet()
177  for h: {C.CapState.valid(C.CapCred.sets(c)) == True{} : Bool}
178  {C.CapState.valid(C.CapCred.sets(C.Caps.or(A.Caps.capset(c, e, p, i), c))) == True{} : Bool}
179
180# prctl(2) PR_CAPBSET_DROP
181
182law bset_drop_never_grows:
183  for +k: C.CapsKernel
184  for +c: C.CapCred
185  for +x: U32
186  {C.CapSet.subset(C.CapState.bounding(C.CapCred.sets(C.Caps.or(A.Caps.bset_drop(k, c, x), c))), C.CapState.bounding(C.CapCred.sets(c))) == True{} : Bool}
187
188# dropping from the bounding set changes no other set (in particular, not the
189# inheritable set)
190law bset_drop_rest_unchanged:
191  for +k: C.CapsKernel
192  for +c: C.CapCred
193  for +x: U32
194  {C.CapState.with_bounding(C.CapCred.sets(C.Caps.or(A.Caps.bset_drop(k, c, x), c)), C.CapSet.empty()) == C.CapState.with_bounding(C.CapCred.sets(c), C.CapSet.empty()) : C.CapState}
195
196# prctl(2) PR_CAP_AMBIENT
197
198law ambient_raise_valid:
199  for +k: C.CapsKernel
200  for +c: C.CapCred
201  for +x: U32
202  for h: {C.CapState.valid(C.CapCred.sets(c)) == True{} : Bool}
203  {C.CapState.valid(C.CapCred.sets(C.Caps.or(A.Caps.ambient_raise(k, c, x), c))) == True{} : Bool}
204
205law ambient_lower_valid:
206  for +k: C.CapsKernel
207  for +c: C.CapCred
208  for +x: U32
209  for h: {C.CapState.valid(C.CapCred.sets(c)) == True{} : Bool}
210  {C.CapState.valid(C.CapCred.sets(C.Caps.or(A.Caps.ambient_lower(k, c, x), c))) == True{} : Bool}
211
212law ambient_raise_rest_unchanged:
213  for +k: C.CapsKernel
214  for +c: C.CapCred
215  for +x: U32
216  {C.CapState.with_ambient(C.CapCred.sets(C.Caps.or(A.Caps.ambient_raise(k, c, x), c)), C.CapSet.empty()) == C.CapState.with_ambient(C.CapCred.sets(c), C.CapSet.empty()) : C.CapState}
217
218law ambient_lower_rest_unchanged:
219  for +k: C.CapsKernel
220  for +c: C.CapCred
221  for +x: U32
222  {C.CapState.with_ambient(C.CapCred.sets(C.Caps.or(A.Caps.ambient_lower(k, c, x), c)), C.CapSet.empty()) == C.CapState.with_ambient(C.CapCred.sets(c), C.CapSet.empty()) : C.CapState}
223
224law ambient_clear_all_empty:
225  for +c: C.CapCred
226  {C.CapState.ambient(C.CapCred.sets(A.Caps.ambient_clear_all(c))) == C.CapSet.empty() : C.CapSet()}
227
228# Vectors
229
230law name_first:
231  {C.Cap.name(0) == Some{"CAP_CHOWN"} : Maybe<&2, String>}
232
233law name_last:
234  {C.Cap.name(40) == Some{"CAP_CHECKPOINT_RESTORE"} : Maybe<&2, String>}
235
236law name_beyond:
237  {C.Cap.name(41) == None{} : Maybe<&2, String>}
238
239law of_name_sys_admin:
240  {C.Cap.of_name("CAP_SYS_ADMIN") == Some{21} : Maybe<&2, U32>}
241
242# the full set, as /proc/<pid>/status shows it on Linux 5.9 and later
243law show_full:
244  {C.CapSet.show(C.CapSet.full()) == "000001ffffffffff" : String}
245
246# CAP_NET_RAW (13) and CAP_NET_BIND_SERVICE (10): 0x2400
247law show_two:
248  {C.CapSet.show(C.CapSet.from_list([13, 10])) == "0000000000002400" : String}
249
250# A capability-dumb binary (cap_net_raw=ep) run by a non-root user whose
251# bounding set lacks CAP_NET_RAW: execve fails with EPERM.
252law vector_dumb_binary:
253  {E.Caps.execve(C.CapsKernel.linux(), C.CapCred{1000, 1000, 1000, False{}, False{}, C.CapState{C.CapSet.empty(), C.CapSet.empty(), C.CapSet.empty(), C.CapSet.del(C.CapSet.full(), 13), C.CapSet.empty()}}, C.CapFile{0, False{}, False{}, Some{C.CapFileSets{C.CapSet.of(13), C.CapSet.empty(), True{}}}}, False{}) == Fail{C.CapsCapabilityDumb{}} : Result<&2, &2, C.CapsError, C.CapCred>}
254
255# A set-user-ID-root program with file capabilities (cap_net_bind_service=ep)
256# run by user 1000: the effective and saved UIDs become 0, and the process
257# gains just the file's capabilities.
258law vector_suid_root_with_caps:
259  {E.Caps.execve(C.CapsKernel.linux(), C.CapCred{1000, 1000, 1000, False{}, False{}, C.CapState{C.CapSet.empty(), C.CapSet.empty(), C.CapSet.empty(), C.CapSet.full(), C.CapSet.empty()}}, C.CapFile{0, True{}, False{}, Some{C.CapFileSets{C.CapSet.of(10), C.CapSet.empty(), True{}}}}, False{}) == Done{C.CapCred{1000, 0, 0, False{}, False{}, C.CapState{C.CapSet.of(10), C.CapSet.empty(), C.CapSet.of(10), C.CapSet.full(), C.CapSet.empty()}}} : Result<&2, &2, C.CapsError, C.CapCred>}
260
261# The same program without file capabilities gains every capability in the
262# bounding set.
263law vector_suid_root_plain:
264  {E.Caps.execve(C.CapsKernel.linux(), C.CapCred{1000, 1000, 1000, False{}, False{}, C.CapState{C.CapSet.empty(), C.CapSet.empty(), C.CapSet.empty(), C.CapSet.del(C.CapSet.full(), 21), C.CapSet.empty()}}, C.CapFile{0, True{}, False{}, None{}}, False{}) == Done{C.CapCred{1000, 0, 0, False{}, False{}, C.CapState{C.CapSet.del(C.CapSet.full(), 21), C.CapSet.empty(), C.CapSet.del(C.CapSet.full(), 21), C.CapSet.del(C.CapSet.full(), 21), C.CapSet.empty()}}} : Result<&2, &2, C.CapsError, C.CapCred>}
265
266# With no_new_privs (ign), the set-user-ID bit is ignored: nothing is gained.
267law vector_suid_ignored:
268  {E.Caps.execve(C.CapsKernel.linux(), C.CapCred{1000, 1000, 1000, False{}, False{}, C.CapState{C.CapSet.empty(), C.CapSet.empty(), C.CapSet.empty(), C.CapSet.full(), C.CapSet.empty()}}, C.CapFile{0, True{}, False{}, None{}}, True{}) == Done{C.CapCred{1000, 1000, 1000, False{}, False{}, C.CapState{C.CapSet.empty(), C.CapSet.empty(), C.CapSet.empty(), C.CapSet.full(), C.CapSet.empty()}}} : Result<&2, &2, C.CapsError, C.CapCred>}
269
270# capset may not add to the permitted set
271law vector_capset_grows:
272  {A.Caps.capset(C.CapCred{1000, 1000, 1000, False{}, False{}, C.CapState{C.CapSet.of(13), C.CapSet.empty(), C.CapSet.empty(), C.CapSet.full(), C.CapSet.empty()}}, C.CapSet.empty(), C.CapSet.from_list([13, 12]), C.CapSet.empty()) == Fail{C.CapsPermittedGrows{}} : Result<&2, &2, C.CapsError, C.CapCred>}
273
274# an ambient capability must be permitted and inheritable
275law vector_ambient_not_inheritable:
276  {A.Caps.ambient_raise(C.CapsKernel.linux(), C.CapCred{1000, 1000, 1000, False{}, False{}, C.CapState{C.CapSet.of(13), C.CapSet.empty(), C.CapSet.empty(), C.CapSet.full(), C.CapSet.empty()}}, 13) == Fail{C.CapsAmbientNotAllowed{}} : Result<&2, &2, C.CapsError, C.CapCred>}
277
278# 41 is beyond CAP_CHECKPOINT_RESTORE
279law vector_drop_invalid:
280  {A.Caps.bset_drop(C.CapsKernel.linux(), C.CapCred{0, 0, 0, False{}, False{}, C.CapState{C.CapSet.full(), C.CapSet.empty(), C.CapSet.full(), C.CapSet.full(), C.CapSet.empty()}}, 41) == Fail{C.CapsInvalidCap{}} : Result<&2, &2, C.CapsError, C.CapCred>}
281
282# Witnesses: every hypothesis of the laws above holds for some input, so no
283# law is vacuous. A valid state with a nonempty ambient set (CAP_NET_BIND_
284# SERVICE permitted, inheritable and ambient; CAP_NET_RAW permitted and
285# effective):
286law witness_valid:
287  {C.CapState.valid(C.CapCred.sets(C.CapCred{1000, 1000, 1000, False{}, False{}, C.CapState{C.CapSet.from_list([10, 13]), C.CapSet.of(10), C.CapSet.of(13), C.CapSet.full(), C.CapSet.of(10)}})) == True{} : Bool}
288
289# ambient within inheritable, for a credential's sets and for a state
290law witness_ambient_inheritable:
291  {C.CapSet.subset(C.CapState.ambient(C.CapCred.sets(C.CapCred{1000, 1000, 1000, False{}, False{}, C.CapState{C.CapSet.from_list([10, 13]), C.CapSet.of(10), C.CapSet.of(13), C.CapSet.full(), C.CapSet.of(10)}})), C.CapState.inheritable(C.CapCred.sets(C.CapCred{1000, 1000, 1000, False{}, False{}, C.CapState{C.CapSet.from_list([10, 13]), C.CapSet.of(10), C.CapSet.of(13), C.CapSet.full(), C.CapSet.of(10)}}))) == True{} : Bool}
292
293law witness_ambient_inheritable_state:
294  {C.CapSet.subset(C.CapState.ambient(C.CapState{C.CapSet.of(10), C.CapSet.of(10), C.CapSet.empty(), C.CapSet.full(), C.CapSet.of(10)}), C.CapState.inheritable(C.CapState{C.CapSet.of(10), C.CapSet.of(10), C.CapSet.empty(), C.CapSet.full(), C.CapSet.of(10)})) == True{} : Bool}
295
296# a nonzero user ID (the non-root laws' hypotheses on the real and effective
297# user IDs)
298law witness_nonzero_uid:
299  {U32.is_eq(1000, 0) == False{} : Bool}