You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
`LoggedCap<P>` records every `try_cap()` invocation in an append-only audit log — implementing Saltzer & Schroeder's *compromise recording* principle ([The Protection of Information in Computer Systems](https://www.cs.virginia.edu/~evans/cs551/saltzer/), 1975, Design Principle #8):
`DualKeyCap<P>` requires two independent approvals before `try_cap()` succeeds — implementing Saltzer & Schroeder's *separation of privilege* principle (Design Principle #5: "a mechanism that requires two keys to unlock it is more robust than one that allows access to the presenter of only a single key"):
capsec's design draws from three foundational papers in capability-based security:
376
+
377
+
-**Dennis & Van Horn (1966)** — [Programming Semantics for Multiprogrammed Computations](https://dl.acm.org/doi/10.1145/365230.365252). Introduced capability lists (C-lists), unforgeable capability tokens, and spheres of protection. capsec's `Cap<P>` is a direct descendant of their capability concept; `Cap::new()` being `pub(crate)` enforces unforgeability in software the way their hardware enforced it in the supervisor.
378
+
379
+
-**Saltzer & Schroeder (1975)** — [The Protection of Information in Computer Systems](https://www.cs.virginia.edu/~evans/cs551/saltzer/). Defined the eight design principles for protection mechanisms. capsec implements six: economy of mechanism (zero-sized types), fail-safe defaults (no cap = no access), least privilege (the core mission), open design (open source + adversarial test suite), separation of privilege (`DualKeyCap`), and compromise recording (`LoggedCap`). The two partially met — complete mediation and least common mechanism — are inherent limitations of a library-level approach.
380
+
381
+
-**Melicher et al. (2017)** — [A Capability-Based Module System for Authority Control](https://www.cs.cmu.edu/~aldrich/papers/ecoop17modules.pdf) (ECOOP 2017). Formalized non-transitive authority in the Wyvern language, proving that a module's authority can be determined by inspecting only its interface. capsec achieves the same property: `Has<P>` bounds make a function's authority visible in its signature, and `Attenuated<P, S>` / runtime cap types that don't implement `Has<P>` enforce non-transitivity.
0 commit comments