Reasoning about Object Capabilities with Logical Relations and Effect Parametricity

Object capabilities are a technique for fine-grained
privilege separation in programming languages and systems,
with important applications in security. However, current formal characterisations do not fully capture capability-safety of
a programming language and are not sufficient for verifying
typical applications. 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 for deriving properties about effects. Our results
imply memory access bounds that have previously been used
to characterise capability-safety.