Module cap_proofs 

Capability Formal Model

Formal verification of the capability system: non-forgery, rights monotonicity (derivation produces subsets), cascading revocation, generation-based invalidation, and cross-address-space isolation.

Structs

CapInvariantChecker

Capability invariant checker

CapSpaceModel

Capability space model (per-process capability table)

CapabilityModel

Model of a capability token

Enums

CapModelError

Errors from capability verification

Constants

CAP_ALL_RIGHTS

CAP_RIGHT_DERIVE

CAP_RIGHT_EXECUTE

CAP_RIGHT_GRANT

CAP_RIGHT_MAP

CAP_RIGHT_READ

Rights bitmask constants

CAP_RIGHT_REVOKE

CAP_RIGHT_WRITE