Object Capabilities
summary
Claim: object capabilities act as necessary conditions for effects, not just rights, and tracking which objects can reach which capabilities lets one distinguish the good/better/account modules from the bad one. Method: a two‑state invariant/spec language plus an algorithmic inference system over encapsulated assertions that lifts and lowers proofs across external calls by tracking protection (path‑based access). Result: handwritten proofs show soundness for modules that preserve balance/password effects; work remains to automate and refine the syntactic protection notion.
AI-written summary · about
chapters (13)
- 0:00Object capabilities intro
- 3:12Why capabilities are necessary
- 8:12Specifying object capabilities
- 13:45Defining protection in systems
- 17:28API-agnostic specifications
- 21:51Key insights and future work
- 24:23Q&A on modules and defaults
- 26:33Syntactic limits of protection
- 28:47Internal vs external semantics
- 30:18Separation logic and proofs
- 33:07Untrusted code interfaces
- 34:11Inference system trade-offs
- 35:15Closing remarks
related talks
25mCapabilities, Effects, Ownership, and Behaviors
29mEfficient, Provable Local Capability Revocation using Uninitialized Capabilities
23mSecurity Reasoning via Substructural Dependency Tracking
34mHow can we trust our agents?
19mGradient: Gradual Compartmentalization via Object Capabilities Tracked in Types
17mReasoning about External Calls
24mImplementing a Capability Machine Model into Iris
16mCerisier: A Program Logic for Attestation in a Capability Machine