exec.bend

bend-osdev-caps@0.1.0.0 · 179 lines · 20 definitions

1# bend-osdev-caps, exec.bend: the transformation of a thread's capability
2# sets during execve(2), as capabilities(7) documents it ("Transformation of
3# capabilities during execve()", "Safety checking for capability-dumb
4# binaries", "Capabilities and execution of programs by root") and execve(2)
5# (set-user-ID, and when set-ID bits and file capabilities are ignored).
6import Base
7import bend-osdev-caps@0.1.0.0/caps.bend as C
8
9# The file's sets as the transformation uses them (the notional all-ones sets
10# of the root rules, or the file's own), the notional effective bit, and
11# whether the file is privileged (set-user-ID, set-group-ID, or with
12# capabilities).
13type CapExecFlags is Data:
14  CapExecFlags{privileged: Bool, effective: Bool, permitted: C.CapSet(), inheritable: C.CapSet()}
15
16def CapExec.ambient(privileged: Bool, a: C.CapSet()) -> C.CapSet():
17  match privileged:
18    case True{}:
19      C.CapSet.empty()
20    case False{}:
21      a
22
23def CapExec.effective(effective: Bool, p: C.CapSet(), a: C.CapSet()) -> C.CapSet():
24  match effective:
25    case True{}:
26      p
27    case False{}:
28      a
29
30# capabilities(7):
31#   P'(ambient)     = (file is privileged) ? 0 : P(ambient)
32#   P'(permitted)   = (P(inheritable) & F(inheritable)) |
33#                     (F(permitted) & P(bounding)) | P'(ambient)
34#   P'(effective)   = F(effective) ? P'(permitted) : P'(ambient)
35#   P'(inheritable) = P(inheritable)
36#   P'(bounding)    = P(bounding)
37def CapExec.sets(fl: CapExecFlags, s: C.CapState) -> C.CapState:
38  match fl s:
39    case CapExecFlags{priv, feff, fp, fi} C.CapState{p, +i, e, +b, a}:
40      +a2 = CapExec.ambient(priv, a)
41      +p2 = C.CapSet.union(C.CapSet.union(C.CapSet.inter(i, fi), C.CapSet.inter(fp, b)), a2)
42      C.CapState{p2, i, CapExec.effective(feff, p2, a2), b, a2}
43
44# the effective user ID after execve: the file's owner if it is
45# set-user-ID, unless set-ID bits are ignored
46def CapExec.euid(ign: Bool, setuid: Bool, owner: U32, euid: U32) -> U32:
47  match ign:
48    case True{}:
49      euid
50    case False{}:
51      match setuid:
52        case True{}:
53          owner
54        case False{}:
55          euid
56
57# the file's capabilities, unless they are ignored
58def CapExec.fcaps(ign: Bool, fc: Maybe<&2, C.CapFileSets>) -> Maybe<&2, C.CapFileSets>:
59  match ign:
60    case True{}:
61      None{}
62    case False{}:
63      fc
64
65def CapExec.has_caps(fc: Maybe<&2, C.CapFileSets>) -> Bool:
66  match fc:
67    case None{}:
68      False{}
69    case Some{x}:
70      True{}
71
72# a privileged file: set-user-ID, set-group-ID, or with capabilities
73def CapExec.privileged(ign: Bool, setuid: Bool, setgid: Bool, fc: Maybe<&2, C.CapFileSets>) -> Bool:
74  match ign:
75    case True{}:
76      CapExec.has_caps(fc)
77    case False{}:
78      Bool.or(setuid, Bool.or(setgid, CapExec.has_caps(fc)))
79
80# the file's own sets (empty when it has none); effective is the notional
81# effective bit of the root rules, ORed with the file's own
82def CapExec.flags.file(priv: Bool, effective: Bool, fc: Maybe<&2, C.CapFileSets>) -> CapExecFlags:
83  match fc:
84    case None{}:
85      CapExecFlags{priv, effective, C.CapSet.empty(), C.CapSet.empty()}
86    case Some{C.CapFileSets{fp, fi, fe}}:
87      CapExecFlags{priv, Bool.or(effective, fe), fp, fi}
88
89# effective UID 0 but real UID not: the file's sets are all ones, unless the
90# file has capabilities (a set-user-ID-root program with file capabilities)
91def CapExec.flags.suid_root(priv: Bool, fc: Maybe<&2, C.CapFileSets>) -> CapExecFlags:
92  match fc:
93    case None{}:
94      CapExecFlags{priv, True{}, C.CapSet.full(), C.CapSet.full()}
95    case Some{C.CapFileSets{fp, fi, fe}}:
96      CapExecFlags{priv, True{}, fp, fi}
97
98def CapExec.fc_effective(fc: Maybe<&2, C.CapFileSets>) -> Bool:
99  match fc:
100    case None{}:
101      False{}
102    case Some{C.CapFileSets{fp, fi, fe}}:
103      fe
104
105# "Capabilities and execution of programs by root": with r0 (real UID 0)
106# and e0 (effective UID 0, after the set-user-ID bit), unless SECBIT_NOROOT:
107#   (1) the file's inheritable and permitted sets are all ones (but a
108#       set-user-ID-root program with capabilities run by a non-root real
109#       UID keeps its own);
110#   (2) if e0, the file effective bit is one.
111def CapExec.flags.go(noroot: Bool, r0: Bool, e0: Bool, priv: Bool, fc: Maybe<&2, C.CapFileSets>) -> CapExecFlags:
112  match noroot:
113    case True{}:
114      CapExec.flags.file(priv, False{}, fc)
115    case False{}:
116      match r0:
117        case True{}:
118          CapExecFlags{priv, Bool.or(e0, CapExec.fc_effective(fc)), C.CapSet.full(), C.CapSet.full()}
119        case False{}:
120          match e0:
121            case True{}:
122              CapExec.flags.suid_root(priv, fc)
123            case False{}:
124              CapExec.flags.file(priv, False{}, fc)
125
126# the file's capabilities as execve sees them: none if ign, or if the kernel
127# has file capabilities off
128def CapExec.file_caps(k: C.CapsKernel, f: C.CapFile, ign: Bool) -> Maybe<&2, C.CapFileSets>:
129  match f:
130    case C.CapFile{u, su, sg, fc}:
131      CapExec.fcaps(Bool.or(ign, Bool.not(C.CapsKernel.file_caps(k))), fc)
132
133def CapExec.flags.mk(+fc2: Maybe<&2, C.CapFileSets>, c: C.CapCred, f: C.CapFile, +ign: Bool) -> CapExecFlags:
134  match c f:
135    case C.CapCred{r, e, s, nr, na, st} C.CapFile{u, +su, sg, fc}:
136      CapExec.flags.go(nr, U32.is_eq(r, 0), U32.is_eq(CapExec.euid(ign, su, u, e), 0), CapExec.privileged(ign, su, sg, fc2), fc2)
137
138def CapExec.flags(k: C.CapsKernel, c: C.CapCred, +f: C.CapFile, +ign: Bool) -> CapExecFlags:
139  CapExec.flags.mk(CapExec.file_caps(k, f, ign), c, f, ign)
140
141# The thread's sets after it executes f. ign: the set-user-ID and
142# set-group-ID bits and the file capabilities are ignored (no_new_privs, a
143# nosuid mount, or a ptraced caller: execve(2)).
144def Caps.execve.sets(k: C.CapsKernel, +c: C.CapCred, f: C.CapFile, ign: Bool) -> C.CapState:
145  CapExec.sets(CapExec.flags(k, c, f, ign), C.CapCred.sets(c))
146
147# "Safety checking for capability-dumb binaries": a file with capabilities
148# and the effective bit must grant all of its permitted set
149def CapExec.dumb_ok(fc: Maybe<&2, C.CapFileSets>, p: C.CapSet()) -> Bool:
150  match fc:
151    case None{}:
152      True{}
153    case Some{C.CapFileSets{fp, fi, fe}}:
154      match fe:
155        case False{}:
156          True{}
157        case True{}:
158          C.CapSet.subset(fp, p)
159
160def CapExec.fin(ok: Bool, c: C.CapCred, +euid: U32, s: C.CapState) -> Result<&2, &2, C.CapsError, C.CapCred>:
161  match ok:
162    case False{}:
163      Fail{C.CapsCapabilityDumb{}}
164    case True{}:
165      match c:
166        case C.CapCred{r, e, sv, nr, na, st}:
167          Done{C.CapCred{r, euid, euid, nr, na, s}}
168
169def CapExec.new_euid(c: C.CapCred, f: C.CapFile, ign: Bool) -> U32:
170  match c f:
171    case C.CapCred{r, e, s, nr, na, st} C.CapFile{u, su, sg, fc}:
172      CapExec.euid(ign, su, u, e)
173
174# execve(2) of f: the new credentials (the effective user ID changes for a
175# set-user-ID file, and the saved set-user-ID becomes the effective one), or
176# CapsCapabilityDumb (EPERM)
177def Caps.execve(+k: C.CapsKernel, +c: C.CapCred, +f: C.CapFile, +ign: Bool) -> Result<&2, &2, C.CapsError, C.CapCred>:
178  +s = Caps.execve.sets(k, c, f, ign)
179  CapExec.fin(CapExec.dumb_ok(CapExec.file_caps(k, f, ign), C.CapState.permitted(s)), c, CapExec.new_euid(c, f, ign), s)