adjust.bend

bend-osdev-caps@0.1.0.0 · 148 lines · 19 definitions

1# bend-osdev-caps, adjust.bend: changing a thread's capability sets.
2# capset(2) under the rules of capabilities(7) ("Programmatically adjusting
3# capability sets"), and the prctl(2) operations PR_CAPBSET_READ,
4# PR_CAPBSET_DROP and PR_CAP_AMBIENT.
5import Base
6import bend-osdev-caps@0.1.0.0/caps.bend as C
7
8# capset(2)
9
10# the new sets; ambient capabilities no longer both permitted and
11# inheritable are lowered (capabilities(7), "Ambient")
12def CapAdjust.set_pie(s: C.CapState, +p: C.CapSet(), +i: C.CapSet(), e: C.CapSet()) -> C.CapState:
13  match s:
14    case C.CapState{op, oi, oe, b, a}:
15      C.CapState{p, i, e, b, C.CapSet.inter(C.CapSet.inter(a, p), i)}
16
17def CapAdjust.capset.done(+c: C.CapCred, e: C.CapSet(), p: C.CapSet(), i: C.CapSet()) -> Result<&2, &2, C.CapsError, C.CapCred>:
18  Done{C.CapCred.with_sets(c, CapAdjust.set_pie(C.CapCred.sets(c), p, i, e))}
19
20# without CAP_SETPCAP in the effective set: the new inheritable set must be
21# within the old inheritable and permitted sets
22def CapAdjust.capset.r4(setpcap: Bool, inh_ok: Bool, +c: C.CapCred, e: C.CapSet(), p: C.CapSet(), i: C.CapSet()) -> Result<&2, &2, C.CapsError, C.CapCred>:
23  match setpcap:
24    case True{}:
25      CapAdjust.capset.done(c, e, p, i)
26    case False{}:
27      match inh_ok:
28        case False{}:
29          Fail{C.CapsInheritableNotPermitted{}}
30        case True{}:
31          CapAdjust.capset.done(c, e, p, i)
32
33# the new inheritable set must be within the old inheritable and bounding sets
34def CapAdjust.capset.r3(ok: Bool, +c: C.CapCred, e: C.CapSet(), p: C.CapSet(), +i: C.CapSet()) -> Result<&2, &2, C.CapsError, C.CapCred>:
35  match ok:
36    case False{}:
37      Fail{C.CapsInheritableNotBounded{}}
38    case True{}:
39      +s = C.CapCred.sets(c)
40      CapAdjust.capset.r4(C.CapSet.has(C.CapState.effective(s), C.Cap.setpcap()), C.CapSet.subset(i, C.CapSet.union(C.CapState.inheritable(s), C.CapState.permitted(s))), c, e, p, i)
41
42# the new effective set must be within the new permitted set
43def CapAdjust.capset.r2(ok: Bool, +c: C.CapCred, e: C.CapSet(), p: C.CapSet(), +i: C.CapSet()) -> Result<&2, &2, C.CapsError, C.CapCred>:
44  match ok:
45    case False{}:
46      Fail{C.CapsEffectiveNotPermitted{}}
47    case True{}:
48      +s = C.CapCred.sets(c)
49      CapAdjust.capset.r3(C.CapSet.subset(i, C.CapSet.union(C.CapState.inheritable(s), C.CapState.bounding(s))), c, e, p, i)
50
51# the new permitted set must be within the old one
52def CapAdjust.capset.r1(ok: Bool, +c: C.CapCred, +e: C.CapSet(), +p: C.CapSet(), i: C.CapSet()) -> Result<&2, &2, C.CapsError, C.CapCred>:
53  match ok:
54    case False{}:
55      Fail{C.CapsPermittedGrows{}}
56    case True{}:
57      CapAdjust.capset.r2(C.CapSet.subset(e, p), c, e, p, i)
58
59# capset(2) with new effective e, permitted p and inheritable i. The rules
60# are checked in this order, and the first that fails names the error.
61def Caps.capset(+c: C.CapCred, e: C.CapSet(), +p: C.CapSet(), i: C.CapSet()) -> Result<&2, &2, C.CapsError, C.CapCred>:
62  CapAdjust.capset.r1(C.CapSet.subset(p, C.CapState.permitted(C.CapCred.sets(c))), c, e, p, i)
63
64# prctl(2) PR_CAPBSET_READ and PR_CAPBSET_DROP
65
66def CapAdjust.bset_drop.go(v: Bool, setpcap: Bool, +c: C.CapCred, x: U32) -> Result<&2, &2, C.CapsError, C.CapCred>:
67  match v:
68    case False{}:
69      Fail{C.CapsInvalidCap{}}
70    case True{}:
71      match setpcap:
72        case False{}:
73          Fail{C.CapsNoSetpcap{}}
74        case True{}:
75          +s = C.CapCred.sets(c)
76          Done{C.CapCred.with_sets(c, C.CapState.with_bounding(s, C.CapSet.del(C.CapState.bounding(s), x)))}
77
78# drop capability x from the bounding set: CapsInvalidCap (EINVAL) if the
79# kernel does not support x, CapsNoSetpcap (EPERM) without CAP_SETPCAP in the
80# effective set
81def Caps.bset_drop(k: C.CapsKernel, +c: C.CapCred, +x: U32) -> Result<&2, &2, C.CapsError, C.CapCred>:
82  CapAdjust.bset_drop.go(C.CapsKernel.valid(k, x), C.CapSet.has(C.CapState.effective(C.CapCred.sets(c)), C.Cap.setpcap()), c, x)
83
84def CapAdjust.bset_read.go(v: Bool, c: C.CapCred, x: U32) -> Result<&2, &2, C.CapsError, Bool>:
85  match v:
86    case False{}:
87      Fail{C.CapsInvalidCap{}}
88    case True{}:
89      Done{C.CapSet.has(C.CapState.bounding(C.CapCred.sets(c)), x)}
90
91# whether x is in the bounding set
92def Caps.bset_read(k: C.CapsKernel, c: C.CapCred, +x: U32) -> Result<&2, &2, C.CapsError, Bool>:
93  CapAdjust.bset_read.go(C.CapsKernel.valid(k, x), c, x)
94
95# prctl(2) PR_CAP_AMBIENT
96
97def CapAdjust.ambient.allowed(c: C.CapCred, +x: U32) -> Bool:
98  +s = C.CapCred.sets(c)
99  Bool.and(C.CapSet.has(C.CapState.permitted(s), x), C.CapSet.has(C.CapState.inheritable(s), x))
100
101def CapAdjust.ambient_raise.go(v: Bool, locked: Bool, allowed: Bool, +c: C.CapCred, x: U32) -> Result<&2, &2, C.CapsError, C.CapCred>:
102  match v:
103    case False{}:
104      Fail{C.CapsInvalidCap{}}
105    case True{}:
106      match locked:
107        case True{}:
108          Fail{C.CapsAmbientRaiseLocked{}}
109        case False{}:
110          match allowed:
111            case False{}:
112              Fail{C.CapsAmbientNotAllowed{}}
113            case True{}:
114              +s = C.CapCred.sets(c)
115              Done{C.CapCred.with_sets(c, C.CapState.with_ambient(s, C.CapSet.add(C.CapState.ambient(s), x)))}
116
117# PR_CAP_AMBIENT_RAISE: x must be both permitted and inheritable
118# (CapsAmbientNotAllowed), and SECBIT_NO_CAP_AMBIENT_RAISE clear
119# (CapsAmbientRaiseLocked)
120def Caps.ambient_raise(k: C.CapsKernel, +c: C.CapCred, +x: U32) -> Result<&2, &2, C.CapsError, C.CapCred>:
121  CapAdjust.ambient_raise.go(C.CapsKernel.valid(k, x), C.CapCred.no_ambient_raise(c), CapAdjust.ambient.allowed(c, x), c, x)
122
123def CapAdjust.ambient_lower.go(v: Bool, +c: C.CapCred, x: U32) -> Result<&2, &2, C.CapsError, C.CapCred>:
124  match v:
125    case False{}:
126      Fail{C.CapsInvalidCap{}}
127    case True{}:
128      +s = C.CapCred.sets(c)
129      Done{C.CapCred.with_sets(c, C.CapState.with_ambient(s, C.CapSet.del(C.CapState.ambient(s), x)))}
130
131# PR_CAP_AMBIENT_LOWER
132def Caps.ambient_lower(k: C.CapsKernel, +c: C.CapCred, +x: U32) -> Result<&2, &2, C.CapsError, C.CapCred>:
133  CapAdjust.ambient_lower.go(C.CapsKernel.valid(k, x), c, x)
134
135def CapAdjust.ambient_is_set.go(v: Bool, c: C.CapCred, x: U32) -> Result<&2, &2, C.CapsError, Bool>:
136  match v:
137    case False{}:
138      Fail{C.CapsInvalidCap{}}
139    case True{}:
140      Done{C.CapSet.has(C.CapState.ambient(C.CapCred.sets(c)), x)}
141
142# PR_CAP_AMBIENT_IS_SET
143def Caps.ambient_is_set(k: C.CapsKernel, c: C.CapCred, +x: U32) -> Result<&2, &2, C.CapsError, Bool>:
144  CapAdjust.ambient_is_set.go(C.CapsKernel.valid(k, x), c, x)
145
146# PR_CAP_AMBIENT_CLEAR_ALL
147def Caps.ambient_clear_all(+c: C.CapCred) -> C.CapCred:
148  C.CapCred.with_sets(c, C.CapState.with_ambient(C.CapCred.sets(c), C.CapSet.empty()))