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.
19	import Base
20	import ./caps.bend as C
21	import ./exec.bend as E
22	import ./adjust.bend as A
23	
24	# execve(2)
25	
26	law 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	
33	law 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	
40	law 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	
47	law 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	
55	law 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	
63	law 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	
70	law 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")
80	law 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
88	law 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.
100	law 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	
112	law 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.
128	law 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	
142	law 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	
158	law 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	
165	law 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	
172	law 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	
182	law 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)
190	law 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	
198	law 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	
205	law 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	
212	law 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	
218	law 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	
224	law 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	
230	law name_first:
231	  {C.Cap.name(0) == Some{"CAP_CHOWN"} : Maybe<&2, String>}
232	
233	law name_last:
234	  {C.Cap.name(40) == Some{"CAP_CHECKPOINT_RESTORE"} : Maybe<&2, String>}
235	
236	law name_beyond:
237	  {C.Cap.name(41) == None{} : Maybe<&2, String>}
238	
239	law 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
243	law show_full:
244	  {C.CapSet.show(C.CapSet.full()) == "000001ffffffffff" : String}
245	
246	# CAP_NET_RAW (13) and CAP_NET_BIND_SERVICE (10): 0x2400
247	law 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.
252	law 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.
258	law 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.
263	law 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.
267	law 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
271	law 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
275	law 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
279	law 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):
286	law 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
290	law 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	
293	law 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)
298	law witness_nonzero_uid:
299	  {U32.is_eq(1000, 0) == False{} : Bool}