Talk by Prof. Sophia Drossopoulou : Reasoning with Object Capabilities, Friday January 26, 2024 at 14:00 in BC 01 and Zoom
Title: Reasoning with Object Capabilities
Abstract:
Joint work with James Noble, Susan Eisenbach, and Julian Mackay
The traditional explanation about object capabilities is that possession of a capability grants the power to use its processing abilities. However, we argue that this is too weak: Instead, for object capabilities to be truly useful, they should guarantee that lack to access to a capability prevents a certain effect from emerging.
Staring from this, we can then develop a proof system, that allows us to reason about executions emerging out of the liking of internal, trusted code, with external, untrusted, code.
Our proposal is based on the following main ingredients: We give semantics to “lack of access to a capability”. We propose formal, holistic, specifications of modules which express the requirement that lack of access to a capability guarantees the absence of certain effects. We propose program verification rules that keep track of access to capabilities, that can prove modules’ adherence to holistic specifications, and support verification of code, even in the presence of calls into external, untrusted code.
Biography :
Sophia Drossopoulou is a Professor at Imperial College London. Prior to that she has worked at Meta, as Visiting Researcher at Meta, and at the Technical University of Karlsruhe. Her research involves Object-oriented programming, Programming Languages, Semantics, Types, Concurrency, Holistic Specifications and Verification
Joint work with James Noble, Susan Eisenbach, and Julian Mackay
The traditional explanation about object capabilities is that possession of a capability grants the power to use its processing abilities. However, we argue that this is too weak: Instead, for object capabilities to be truly useful, they should guarantee that lack to access to a capability prevents a certain effect from emerging.
Staring from this, we can then develop a proof system, that allows us to reason about executions emerging out of the liking of internal, trusted code, with external, untrusted, code.
Our proposal is based on the following main ingredients: We give semantics to “lack of access to a capability”. We propose formal, holistic, specifications of modules which express the requirement that lack of access to a capability guarantees the absence of certain effects. We propose program verification rules that keep track of access to capabilities, that can prove modules’ adherence to holistic specifications, and support verification of code, even in the presence of calls into external, untrusted code.
Biography :
Sophia Drossopoulou is a Professor at Imperial College London. Prior to that she has worked at Meta, as Visiting Researcher at Meta, and at the Technical University of Karlsruhe. Her research involves Object-oriented programming, Programming Languages, Semantics, Types, Concurrency, Holistic Specifications and Verification
Practical information
- Informed public
- Free
Organizer
- Professor Martin odersky
Contact
- Natascha Fontana