law execve_nonroot_permitted

bend-osdev-caps@0.1.0.0 · LAWS.bend:124

import Base
import bend-osdev-caps@0.1.0.0/caps.bend as C
import bend-osdev-caps@0.1.0.0/exec.bend as E

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.
128law 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()}