law execve_permitted_bounded

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

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

77# a capability that is in none of the bounding, inheritable and ambient sets
78# never becomes permitted (the bounding set does not mask the inheritable
79# set: capabilities(7), "Capability bounding set")
80law execve_permitted_bounded:
81  for +k: C.CapsKernel
82  for +c: C.CapCred
83  for +f: C.CapFile
84  for +ign: Bool
85  {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.CapSet.union(C.CapState.inheritable(C.CapCred.sets(c)), C.CapState.ambient(C.CapCred.sets(c))))) == True{} : Bool}