Gradient: Gradual Compartmentalization via Object Capabilities Tracked in Types
summary
Proposal implements a Scala extension called Gradient that lets legacy code be migrated incrementally to an object-capability model by combining runtime enforcement and type-tracked authority. It implements dynamic Enclosures to run untrusted packages with only approved system calls, and static Capture Tracking (capture ascriptions) to forbid unwanted device access at compile time. Formal work extends the capture calculus with mutability, modules and objects and proves soundness. Prototype migrates the standard Scala XML library with only trivial edits and measures enclosure-based performance.
AI-written summary · about
chapters (12)
- 0:00Supply chain attacks problem
- 1:04Principle of least authority
- 2:08Process-based compartment limits
- 3:11Gradual capability migration
- 4:17Gradient Scala extension
- 6:47Security via encapsulation
- 7:50Classical and capability code
- 10:18Dynamic compartment blocks
- 12:04Tracking capabilities in types
- 13:54Static compartments via capture
- 15:19Formal validation results
- 17:07Q&A
related talks
34mHow can we trust our agents?
31mSecurity with Scala Refined Types and Object Capabilities
36mObject Capabilities
25mCapabilities, Effects, Ownership, and Behaviors
22mQuest Complete: The Holy Grail of Gradual Security
26mType-directed Program Transformation for Constant-Time Enforcement
22mReconciling Progress-Intensive Noninterference and Declassification
29mEfficient, Provable Local Capability Revocation using Uninitialized Capabilities