law execve_permitted_bounded_valid

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

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

87# with the ambient invariant, the bound is the bounding and inheritable sets
88law execve_permitted_bounded_valid:
89  for +k: C.CapsKernel
90  for +c: C.CapCred
91  for +f: C.CapFile
92  for +ign: Bool
93  for h: {C.CapSet.subset(C.CapState.ambient(C.CapCred.sets(c)), C.CapState.inheritable(C.CapCred.sets(c))) == True{} : Bool}
94  {C.CapSet.subset(C.CapState.permitted(E.Caps.execve.sets(k, c, f, ign)), C.CapSet.union(C.CapState.bounding(C.CapCred.sets(c)), C.CapState.inheritable(C.CapCred.sets(c)))) == True{} : Bool}