caps.bend

bend-osdev-caps@0.1.0.0 · 565 lines · 108 definitions

1# bend-osdev-caps: Linux capability sets, as capabilities(7) documents them.
2# This file: capability numbers, sets, and the thread's and file's sets.
3# exec.bend: the transformation during execve(2). adjust.bend: capset(2) and
4# the prctl(2) bounding-set and ambient operations.
5#
6# A capability set holds bit k for capability k, from CAP_CHOWN (0) to
7# CAP_CHECKPOINT_RESTORE (40): bits 0 to 31 in a native U32, bits 32 to 40 in
8# a Word(9n) (CapSetW, internal). The set operations work bit by bit; the
9# width-n forms (CapBits) are what the laws are proved by induction on, for
10# both parts.
11#
12# A thread has five sets (CapState): permitted, inheritable, effective,
13# bounding and ambient. A file has a permitted and an inheritable set and an
14# effective bit (CapFileSets). execve, capset, and the prctl(2) bounding-set
15# and ambient operations are modelled on a credential (CapCred): the sets, the
16# real, effective and saved user IDs, and the securebits SECBIT_NOROOT and
17# SECBIT_NO_CAP_AMBIENT_RAISE.
18import Base
19import bend-osdev-word64@0.1.0.0/word64.bend as W
20
21# Capability numbers
22
23def Cap.chown() -> U32:
24  0
25
26def Cap.dac_override() -> U32:
27  1
28
29def Cap.dac_read_search() -> U32:
30  2
31
32def Cap.fowner() -> U32:
33  3
34
35def Cap.fsetid() -> U32:
36  4
37
38def Cap.kill() -> U32:
39  5
40
41def Cap.setgid() -> U32:
42  6
43
44def Cap.setuid() -> U32:
45  7
46
47def Cap.setpcap() -> U32:
48  8
49
50def Cap.linux_immutable() -> U32:
51  9
52
53def Cap.net_bind_service() -> U32:
54  10
55
56def Cap.net_broadcast() -> U32:
57  11
58
59def Cap.net_admin() -> U32:
60  12
61
62def Cap.net_raw() -> U32:
63  13
64
65def Cap.ipc_lock() -> U32:
66  14
67
68def Cap.ipc_owner() -> U32:
69  15
70
71def Cap.sys_module() -> U32:
72  16
73
74def Cap.sys_rawio() -> U32:
75  17
76
77def Cap.sys_chroot() -> U32:
78  18
79
80def Cap.sys_ptrace() -> U32:
81  19
82
83def Cap.sys_pacct() -> U32:
84  20
85
86def Cap.sys_admin() -> U32:
87  21
88
89def Cap.sys_boot() -> U32:
90  22
91
92def Cap.sys_nice() -> U32:
93  23
94
95def Cap.sys_resource() -> U32:
96  24
97
98def Cap.sys_time() -> U32:
99  25
100
101def Cap.sys_tty_config() -> U32:
102  26
103
104def Cap.mknod() -> U32:
105  27
106
107def Cap.lease() -> U32:
108  28
109
110def Cap.audit_write() -> U32:
111  29
112
113def Cap.audit_control() -> U32:
114  30
115
116def Cap.setfcap() -> U32:
117  31
118
119def Cap.mac_override() -> U32:
120  32
121
122def Cap.mac_admin() -> U32:
123  33
124
125def Cap.syslog() -> U32:
126  34
127
128def Cap.wake_alarm() -> U32:
129  35
130
131def Cap.block_suspend() -> U32:
132  36
133
134def Cap.audit_read() -> U32:
135  37
136
137def Cap.perfmon() -> U32:
138  38
139
140def Cap.bpf() -> U32:
141  39
142
143def Cap.checkpoint_restore() -> U32:
144  40
145def Cap.count() -> U32:
146  41
147
148def Cap.names() -> List<&2, String>:
149  ["CAP_CHOWN", "CAP_DAC_OVERRIDE", "CAP_DAC_READ_SEARCH", "CAP_FOWNER", "CAP_FSETID", "CAP_KILL", "CAP_SETGID", "CAP_SETUID", "CAP_SETPCAP", "CAP_LINUX_IMMUTABLE", "CAP_NET_BIND_SERVICE", "CAP_NET_BROADCAST", "CAP_NET_ADMIN", "CAP_NET_RAW", "CAP_IPC_LOCK", "CAP_IPC_OWNER", "CAP_SYS_MODULE", "CAP_SYS_RAWIO", "CAP_SYS_CHROOT", "CAP_SYS_PTRACE", "CAP_SYS_PACCT", "CAP_SYS_ADMIN", "CAP_SYS_BOOT", "CAP_SYS_NICE", "CAP_SYS_RESOURCE", "CAP_SYS_TIME", "CAP_SYS_TTY_CONFIG", "CAP_MKNOD", "CAP_LEASE", "CAP_AUDIT_WRITE", "CAP_AUDIT_CONTROL", "CAP_SETFCAP", "CAP_MAC_OVERRIDE", "CAP_MAC_ADMIN", "CAP_SYSLOG", "CAP_WAKE_ALARM", "CAP_BLOCK_SUSPEND", "CAP_AUDIT_READ", "CAP_PERFMON", "CAP_BPF", "CAP_CHECKPOINT_RESTORE"]
150
151# whether k names a capability (0 to 40)
152def Cap.valid(k: U32) -> Bool:
153  U32.is_lt(k, 41)
154
155def Cap.name.go(v: Bool, k: U32) -> Maybe<&2, String>:
156  match v:
157    case False{}:
158      None{}
159    case True{}:
160      List.get(&2, String, Cap.names(), U32.to_nat(k))
161
162# the name of capability k, such as "CAP_CHOWN"
163def Cap.name(+k: U32) -> Maybe<&2, String>:
164  Cap.name.go(Cap.valid(k), k)
165
166def Cap.of_name.hit(hit: Bool, k: U32, rest: Maybe<&2, U32>) -> Maybe<&2, U32>:
167  match hit:
168    case True{}:
169      Some{k}
170    case False{}:
171      rest
172
173def Cap.of_name.go(xs: List<&2, String>, +s: String, +k: U32) -> Maybe<&2, U32>:
174  match xs:
175    case Nil{}:
176      None{}
177    case Con{h, t}:
178      Cap.of_name.hit(String.eq(h, s), k, Cap.of_name.go(t, s, U32.add(k, 1)))
179
180# the number of the capability named s
181def Cap.of_name(s: String) -> Maybe<&2, U32>:
182  Cap.of_name.go(Cap.names(), s, 0)
183
184# Sets of capabilities, for every width n
185
186# the set of every capability below n
187def CapBits.all(n: Nat) -> Word(n):
188  match n:
189    case 0n:
190      WNil{}
191    case 1n+p:
192      WCon{True{}, CapBits.all(p)}
193
194# one bit of a subset test: a bit in a must be in b; r is the rest
195def CapBits.sub.bit(a: Bool, b: Bool, r: Bool) -> Bool:
196  match a:
197    case False{}:
198      r
199    case True{}:
200      match b:
201        case False{}:
202          False{}
203        case True{}:
204          r
205
206# every capability in a is in b
207def CapBits.subset(n: Nat, a: Word(n), b: Word(n)) -> Bool:
208  match n:
209    case 0n:
210      True{}
211    case 1n+p:
212      match a b:
213        case WCon{ah, at} WCon{bh, bt}:
214          CapBits.sub.bit(ah, bh, CapBits.subset(p, at, bt))
215
216# the set holding capability k alone (empty if k >= n)
217def CapBits.single(n: Nat, k: Nat) -> Word(n):
218  match n:
219    case 0n:
220      WNil{}
221    case 1n+p:
222      match k:
223        case 0n:
224          WCon{True{}, Word.zero(p)}
225        case 1n+j:
226          WCon{False{}, CapBits.single(p, j)}
227
228# whether capability k is in s
229def CapBits.has(n: Nat, s: Word(n), k: Nat) -> Bool:
230  match n:
231    case 0n:
232      False{}
233    case 1n+p:
234      match s k:
235        case WCon{h, t} 0n:
236          h
237        case WCon{h, t} 1n+j:
238          CapBits.has(p, t, j)
239
240# the capabilities in s, in increasing order, numbered from k
241def CapBits.to_list(n: Nat, s: Word(n), +k: U32) -> List<&2, U32>:
242  match n:
243    case 0n:
244      Nil{}
245    case 1n+p:
246      match s:
247        case WCon{True{}, t}:
248          Con{k, CapBits.to_list(p, t, U32.add(k, 1))}
249        case WCon{False{}, t}:
250          CapBits.to_list(p, t, U32.add(k, 1))
251
252# Capability sets
253
254# A set is two words: capabilities 0 to 31 are the bits of a native U32 (bit
255# k is capability k), and capabilities 32 to 40 a Word(9n) (bit j is
256# capability 32 + j). Ten machine words, where a Word(41n) cost forty-one
257# (and a CapState of five of them was more than Bend's C backend compiles:
258# bendlang/bend#1069). The high part is exactly nine bits, so every value of
259# the type is a set of capabilities 0 to 40, with one representation each.
260# Internal: use the CapSet defs.
261type CapSetW is Data:
262  CapSetW{lo: U32, hi: Word(9n)}
263
264def CapSet() -> Data:
265  CapSetW
266
267def CapSet.empty() -> CapSet():
268  CapSetW{0, Word.zero(9n)}
269
270def CapSet.full() -> CapSet():
271  CapSetW{4294967295, CapBits.all(9n)}
272
273def CapSet.union(a: CapSet(), b: CapSet()) -> CapSet():
274  match a b:
275    case CapSetW{al, ah} CapSetW{bl, bh}:
276      CapSetW{U32.or(al, bl), Word.or(9n, ah, bh)}
277
278def CapSet.inter(a: CapSet(), b: CapSet()) -> CapSet():
279  match a b:
280    case CapSetW{al, ah} CapSetW{bl, bh}:
281      CapSetW{U32.and(al, bl), Word.and(9n, ah, bh)}
282
283# the capabilities of a not in b
284def CapSet.minus(a: CapSet(), b: CapSet()) -> CapSet():
285  match a b:
286    case CapSetW{al, ah} CapSetW{bl, bh}:
287      CapSetW{U32.and(al, U32.not(bl)), Word.and(9n, ah, Word.not(9n, bh))}
288
289# a within b: no bit of a outside b (on the low word, a & ~b == 0)
290def CapSet.subset(a: CapSet(), b: CapSet()) -> Bool:
291  match a b:
292    case CapSetW{al, ah} CapSetW{bl, bh}:
293      Bool.and(U32.is_eq(U32.and(al, U32.not(bl)), 0), CapBits.subset(9n, ah, bh))
294
295def CapSet.is_eq(a: CapSet(), b: CapSet()) -> Bool:
296  match a b:
297    case CapSetW{al, ah} CapSetW{bl, bh}:
298      Bool.and(U32.is_eq(al, bl), Cmp.is_eq(Word.cmp(9n, ah, bh)))
299
300def CapSetW.single.go(low: Bool, +k: U32) -> CapSet():
301  match low:
302    case True{}:
303      CapSetW{U32.shln(1, U32.to_nat(k)), Word.zero(9n)}
304    case False{}:
305      CapSetW{0, CapBits.single(9n, U32.to_nat(U32.sub(k, 32)))}
306
307# the set holding capability k alone (k is 0 to 40)
308def CapSetW.single(+k: U32) -> CapSet():
309  CapSetW.single.go(U32.is_lt(k, 32), k)
310
311def CapSet.of.go(v: Bool, k: U32) -> CapSet():
312  match v:
313    case False{}:
314      CapSet.empty()
315    case True{}:
316      CapSetW.single(k)
317
318# the set holding capability k alone (empty if k is not a capability)
319def CapSet.of(+k: U32) -> CapSet():
320  CapSet.of.go(Cap.valid(k), k)
321
322def CapSet.has.go(v: Bool, s: CapSet(), k: U32) -> Bool:
323  match v:
324    case False{}:
325      False{}
326    case True{}:
327      CapSet.subset(CapSetW.single(k), s)
328
329# whether capability k is in s
330def CapSet.has(s: CapSet(), +k: U32) -> Bool:
331  CapSet.has.go(Cap.valid(k), s, k)
332
333def CapSet.add(s: CapSet(), k: U32) -> CapSet():
334  CapSet.union(s, CapSet.of(k))
335
336def CapSet.del(s: CapSet(), k: U32) -> CapSet():
337  CapSet.minus(s, CapSet.of(k))
338
339def CapSet.from_list(xs: List<&2, U32>) -> CapSet():
340  match xs:
341    case Nil{}:
342      CapSet.empty()
343    case Con{h, t}:
344      CapSet.add(CapSet.from_list(t), h)
345
346def CapSetW.push(b: Bool, k: U32, rest: List<&2, U32>) -> List<&2, U32>:
347  match b:
348    case True{}:
349      Con{k, rest}
350    case False{}:
351      rest
352
353# the capabilities among the low n bits of w, numbered from k, then rest
354def CapSetW.lo_list(n: Nat, +w: U32, +k: U32, rest: List<&2, U32>) -> List<&2, U32>:
355  match n:
356    case 0n:
357      rest
358    case 1n+p:
359      CapSetW.push(U32.is_eq(U32.and(w, 1), 1), k, CapSetW.lo_list(p, U32.shr(w), U32.add(k, 1), rest))
360
361def CapSet.to_list(s: CapSet()) -> List<&2, U32>:
362  match s:
363    case CapSetW{l, h}:
364      CapSetW.lo_list(32n, l, 0, CapBits.to_list(9n, h, 32))
365
366def CapSetW.bit(b: Bool) -> U32:
367  match b:
368    case True{}:
369      1
370    case False{}:
371      0
372
373# the value of the n bits of w, and the n low bits of a, as native words
374def CapSetW.word_u32(n: Nat, w: Word(n)) -> U32:
375  match n:
376    case 0n:
377      0
378    case 1n+p:
379      match w:
380        case WCon{b, t}:
381          U32.or(CapSetW.bit(b), U32.shl(CapSetW.word_u32(p, t)))
382
383def CapSetW.u32_word(n: Nat, +a: U32) -> Word(n):
384  match n:
385    case 0n:
386      WNil{}
387    case 1n+p:
388      WCon{U32.is_eq(U32.and(a, 1), 1), CapSetW.u32_word(p, U32.shr(a))}
389
390# the 64-bit mask of a set, as capget(2) and /proc/<pid>/status show it
391def CapSet.to_w64(s: CapSet()) -> W.W64:
392  match s:
393    case CapSetW{l, h}:
394      W.W64.from_parts(CapSetW.word_u32(9n, h), l)
395
396# the set of the low 41 bits of a 64-bit mask
397def CapSet.from_w64(+v: W.W64) -> CapSet():
398  CapSetW{W.W64.lo(v), CapSetW.u32_word(9n, W.W64.hi(v))}
399
400# 16 hex digits, as the CapEff line of /proc/<pid>/status
401def CapSet.show(s: CapSet()) -> String:
402  W.W64.show_hex(CapSet.to_w64(s))
403
404# Thread and file capability sets
405
406type CapState is Data:
407  CapState{permitted: CapSet(), inheritable: CapSet(), effective: CapSet(), bounding: CapSet(), ambient: CapSet()}
408
409def CapState.permitted(s: CapState) -> CapSet():
410  match s:
411    case CapState{p, i, e, b, a}:
412      p
413
414def CapState.inheritable(s: CapState) -> CapSet():
415  match s:
416    case CapState{p, i, e, b, a}:
417      i
418
419def CapState.effective(s: CapState) -> CapSet():
420  match s:
421    case CapState{p, i, e, b, a}:
422      e
423
424def CapState.bounding(s: CapState) -> CapSet():
425  match s:
426    case CapState{p, i, e, b, a}:
427      b
428
429def CapState.ambient(s: CapState) -> CapSet():
430  match s:
431    case CapState{p, i, e, b, a}:
432      a
433
434def CapState.with_bounding(s: CapState, b: CapSet()) -> CapState:
435  match s:
436    case CapState{p, i, e, x, a}:
437      CapState{p, i, e, b, a}
438
439def CapState.with_ambient(s: CapState, a: CapSet()) -> CapState:
440  match s:
441    case CapState{p, i, e, b, x}:
442      CapState{p, i, e, b, a}
443
444# capabilities(7)'s invariants: effective within permitted, and no capability
445# ambient unless it is both permitted and inheritable
446def CapState.valid(s: CapState) -> Bool:
447  match s:
448    case CapState{+p, +i, e, b, +a}:
449      Bool.and(CapSet.subset(e, p), Bool.and(CapSet.subset(a, p), CapSet.subset(a, i)))
450
451# A thread's credentials: real, effective and saved set-user-ID, the
452# securebits SECBIT_NOROOT and SECBIT_NO_CAP_AMBIENT_RAISE, and the sets.
453type CapCred is Data:
454  CapCred{ruid: U32, euid: U32, suid: U32, noroot: Bool, no_ambient_raise: Bool, sets: CapState}
455
456def CapCred.ruid(c: CapCred) -> U32:
457  match c:
458    case CapCred{r, e, s, nr, na, st}:
459      r
460
461def CapCred.euid(c: CapCred) -> U32:
462  match c:
463    case CapCred{r, e, s, nr, na, st}:
464      e
465
466def CapCred.suid(c: CapCred) -> U32:
467  match c:
468    case CapCred{r, e, s, nr, na, st}:
469      s
470
471def CapCred.no_ambient_raise(c: CapCred) -> Bool:
472  match c:
473    case CapCred{r, e, s, nr, na, st}:
474      na
475
476def CapCred.sets(c: CapCred) -> CapState:
477  match c:
478    case CapCred{r, e, s, nr, na, st}:
479      st
480
481def CapCred.with_sets(c: CapCred, st: CapState) -> CapCred:
482  match c:
483    case CapCred{r, e, s, nr, na, x}:
484      CapCred{r, e, s, nr, na, st}
485
486# A file's capabilities (the security.capability attribute)
487type CapFileSets is Data:
488  CapFileSets{permitted: CapSet(), inheritable: CapSet(), effective: Bool}
489
490# An executable: its owner, its set-user-ID and set-group-ID bits, and its
491# capabilities, if it has any
492type CapFile is Data:
493  CapFile{uid: U32, setuid: Bool, setgid: Bool, caps: Maybe<&2, CapFileSets>}
494
495# The kernel's choices: the highest capability it supports
496# (/proc/sys/kernel/cap_last_cap; at most 40 here) and whether file
497# capabilities are on (off when booted with no_file_caps)
498type CapsKernel is Data:
499  CapsKernel{last_cap: U32, file_caps: Bool}
500
501# Linux since 5.9: capabilities 0 to 40, file capabilities on
502def CapsKernel.linux() -> CapsKernel:
503  CapsKernel{40, True{}}
504
505def CapsKernel.file_caps(k: CapsKernel) -> Bool:
506  match k:
507    case CapsKernel{l, f}:
508      f
509
510# whether c names a capability this kernel supports
511def CapsKernel.valid(k: CapsKernel, +c: U32) -> Bool:
512  match k:
513    case CapsKernel{l, f}:
514      Bool.and(Cap.valid(c), U32.is_le(c, l))
515
516# Why a call fails
517type CapsError is Data:
518  CapsInvalidCap{}
519  CapsPermittedGrows{}
520  CapsEffectiveNotPermitted{}
521  CapsInheritableNotBounded{}
522  CapsInheritableNotPermitted{}
523  CapsNoSetpcap{}
524  CapsAmbientRaiseLocked{}
525  CapsAmbientNotAllowed{}
526  CapsCapabilityDumb{}
527
528# the errno the kernel answers: EINVAL (22) for a capability it does not
529# support, EPERM (1) otherwise
530def CapsError.errno(e: CapsError) -> U32:
531  match e:
532    case CapsInvalidCap{}:
533      22
534    case CapsPermittedGrows{}:
535      1
536    case CapsEffectiveNotPermitted{}:
537      1
538    case CapsInheritableNotBounded{}:
539      1
540    case CapsInheritableNotPermitted{}:
541      1
542    case CapsNoSetpcap{}:
543      1
544    case CapsAmbientRaiseLocked{}:
545      1
546    case CapsAmbientNotAllowed{}:
547      1
548    case CapsCapabilityDumb{}:
549      1
550
551# the credentials after a call: the new ones, or c if it failed
552def Caps.or(r: Result<&2, &2, CapsError, CapCred>, c: CapCred) -> CapCred:
553  match r:
554    case Done{x}:
555      x
556    case Fail{e}:
557      c
558
559# the sets after a call, or s if it failed
560def Caps.sets_or(r: Result<&2, &2, CapsError, CapCred>, s: CapState) -> CapState:
561  match r:
562    case Done{x}:
563      CapCred.sets(x)
564    case Fail{e}:
565      s