law vector_dumb_binary

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

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

250# A capability-dumb binary (cap_net_raw=ep) run by a non-root user whose
251# bounding set lacks CAP_NET_RAW: execve fails with EPERM.
252law vector_dumb_binary:
253  {E.Caps.execve(C.CapsKernel.linux(), C.CapCred{1000, 1000, 1000, False{}, False{}, C.CapState{C.CapSet.empty(), C.CapSet.empty(), C.CapSet.empty(), C.CapSet.del(C.CapSet.full(), 13), C.CapSet.empty()}}, C.CapFile{0, False{}, False{}, Some{C.CapFileSets{C.CapSet.of(13), C.CapSet.empty(), True{}}}}, False{}) == Fail{C.CapsCapabilityDumb{}} : Result<&2, &2, C.CapsError, C.CapCred>}