Author:

Keywords:

Science & Technology, Technology, Computer Science, Theory & Methods, Engineering, Electrical & Electronic, Computer Science, Engineering, RECURSIVE TYPES, SEMANTICS, object capabilities, logical relations, effect parametricity, capability-safety, C16/15/058#53326573

Abstract:

© 2016 IEEE. Object capabilities are a technique for fine-grained privilegeseparation in programming languages and systems, with importantapplications in security. However, current formal characterisations donot fully capture capability-safety of a programming language and arenot sufficient for verifying typical applications. Usingstate-of-the-art techniques from programming languages research, wedefine a logical relation for a core calculus of JavaScript thatbetter characterises capability-safety. The relation is powerfulenough to reason about typical capability patterns and supportsevolvable invariants on shared data structures, capabilities withrestricted authority over them and isolated components with restrictedcommunication channels. We use a novel notion of effect parametricityfor deriving properties about effects. Our results imply memory accessbounds that have previously been used to characterisecapability-safety.