law execve_nonroot_effective

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

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

142law execve_nonroot_effective:
143  for +k: C.CapsKernel
144  for +r: U32
145  for +e: U32
146  for hr: {U32.is_eq(r, 0) == False{} : Bool}
147  for he: {U32.is_eq(e, 0) == False{} : Bool}
148  for +s: C.CapState
149  for +sv: U32
150  for +nr: Bool
151  for +na: Bool
152  for +u: U32
153  for +ign: Bool
154  {C.CapState.effective(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()}