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).
6	import Base
7	import ./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).
13	type CapExecFlags is Data:
14	  CapExecFlags{privileged: Bool, effective: Bool, permitted: C.CapSet(), inheritable: C.CapSet()}
15	
16	def 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	
23	def 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)
37	def 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
46	def 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
58	def 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	
65	def 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
73	def 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
82	def 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)
91	def 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	
98	def 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.
111	def 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
128	def 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	
133	def 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	
138	def 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)).
144	def 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
149	def 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	
160	def 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	
169	def 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)
177	def 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)