The bibliographic entry was discovered and compiled by a machine, and published without a person checking it against the publication. The publication itself is the authors' own work — this badge says nothing about it.
Reasoning about Object Capabilities with Logical Relations and Effect Parametricity
From OpenAlex, which stores abstracts as an
index of words and their positions: what is shown is rebuilt from that,
and reads fluently whether or not it is what the author wrote.
Abstract
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.
@misc{devriese2016reasoning,
title = {Reasoning about Object Capabilities with Logical Relations and Effect Parametricity},
author = {Dominique Devriese and Lars Birkedal and Frank Piessens},
year = {2016},
journal = {IEEE European Symposium on Security and Privacy},
pages = {147--162},
doi = {10.1109/eurosp.2016.22},
}