Enforcing Well-bracketed Control Flow and Stack Encapsulation using Linear Capabilities
We propose and study a new calling convention that provably enforces well-bracketed control flow and local state encapsulation on a capability machine. The calling convention is based on linear capabilities, a new type of capabilities that are prevented by the hardware from being duplicated. In addition to designing and formalising this new calling convention, we also contribute a new way to formalise and prove that it effectively enforces well-bracketed control flow and local state encapsulation, building on the concept of fully abstract compilation.
Sat 13 Jan Times are displayed in time zone: Tijuana, Baja California change
10:30 - 11:30
|Linear capabilities for modular fully-abstract compilation of verified code|
|Enforcing Well-bracketed Control Flow and Stack Encapsulation using Linear Capabilities|