nx_caps.nx

nx_caps.nx -- high-level capability combinators on memcap. memcap.nx ships the LOW-LEVEL primitive (32-byte software cap with addr/base/len/perms/tag). This module gives the COMBINATOR API that makes capabilities useful in practice: * derive_subrange -- carve a smaller cap from a larger one with no more permission than the parent * narrow_perms -- drop permissions (read-only view of an RW region, etc.); the inverse direction is illegal (caps may only get weaker) * seal / unseal -- type-safe opaque wrapper (Mark Miller's "sealer" pattern, E language 1997) * revoke -- one-way invalidation; future derefs fail * delegate -- transfer ownership across a boundary with audit trail * verify_chain -- prove a cap is reachable from a root via legal weakening operations only CAPABILITY SECURITY MODEL: A cap is a triple (memory_region, perms, tag). Holding a cap means having the AUTHORITY to use the region under perms. The integrity of the model rests on: 1. UNFORGEABILITY -- you cannot construct a cap from nothing; you can only derive from existing caps. 2. MONOTONIC WEAKENING -- derived caps may have FEWER permissions than parents; never more. 3. NO AMBIENT AUTHORITY -- capability is the ONLY way to access; there's no global "open file" syscall that takes a string path. 4. REVOCATION -- the holder of the parent (or a designated revoker) can void all derived caps. LINEAGE: * Dennis-Van Horn 1966 (object capabilities, MIT) * Hardy KeyKOS 1985 (capability microkernel) * Shapiro EROS 1999 (capability OS, formal)