Reasoning about object capabilities with logical relations and effect parametricity - Technical Report including proofs and details
Dominique Devriese, Lars Birkedal, Frank Piessens · Lirias · 2016
Object capabilities are a model for fine-grained privilege separation in programming languages and systems. However,formal characterisations of the model do not fully capturecapability-safety of a programming language and are not sufficient for verifying typical uses of the model. Using state-of-the-art techniques from programming languages research, we define a logical relation for a core calculus of JavaScript that better characterises capability-safety. The relation is powerful enough to reason about typical capability patterns and supports evolvable invariants on shared data structures, capabilities with restricted authority over them and isolated components with restricted communication channels. We use a novel notion of effect parametricity to support deriving properties about primitive effects. We demonstrate that it implies access bound properties that have previously been used to characterise capability-safety. This is a technical report accompanying a paper by the same title, which contains an additional section about a binary version of our results, as well as proofs and details for our results