Max-Planck-Institut für Informatik
max planck institut
informatik
mpii logo Minerva of the Max Planck Society
 

MPI-INF or MPI-SWS or Local Campus Event Calendar

<< Previous Entry Next Entry >> New Event Entry Edit this Entry Login to DB (to update, delete)
What and Who
Title:Formal and Compositional Reasoning about Object Capabilities
Speaker:David Swasey
coming from:Max Planck Institute for Software Systems
Speakers Bio:
Event Type:SWS Student Defense Talks - Thesis Proposal
Visibility:SWS
We use this to send out email in the morning.
Level:Public Audience
Language:English
Date, Time and Location
Date:Friday, 8 December 2017
Time:12:00
Duration:-- Not specified --
Location:Saarbrücken
Building:E1 5
Room:029
Abstract
In scenarios such as web programming, where code is linked
together from multiple sources, object capability patterns
(OCPs) provide an essential safeguard, enabling programmers to
protect the private state of their objects from corruption by
unknown and untrusted code. However, the benefits of OCPs in
terms of security and program verification are barely
understood. Our proposed thesis bridges this gap, advancing
our understanding of the security and functional properties of
OCP-based programs, systems, and programming language
implementations.

Building on the recently developed Iris framework for
separation logic, we propose OCPL, the first formal system for
compositionally specifying and verifying OCPs in a simple but
representative language with closures and mutable state. The
key idea of OCPL is to account for the boundary between
verified and untrusted code by adopting a well-known idea from
the literature on security protocol verification, namely
robust safety. Programs that export only properly wrapped
values to their environment can be proven robustly safe,
meaning that their untrusted environment cannot violate their
internal invariants. Using OCPL, we can give the first
general, compositional, and machine-checked specs for several
commonly-used OCPs—including the dynamic sealing, membrane,
and caretaker patterns—which we can then use to verify robust
safety for representative client code.

A second apsect of our thesis is that separation logic and
robust safety scale to reasoning about the far more
sophisticated OCPs arising in practical systems. We propose to
model the Firefox web browser and its script interpreter,
which uses an automatic security membrane to enforce the web's
same-origin policy. After extending OCPL to account for the
browser and the membrane-aware scripts it interprets, we can
formalize how, under certain trust assumptions, Firefox
supports the illusion (critical to most script authors) of
“normal object reasoning” for membrane-unaware scripts.

The final element in our thesis is that robust safety and
separation logic ease the burden of developing certified
programming language implementations. To benefit from OCPs, a
programmer must choose a language implementation that
preserves the functional and security properties of her
capability-wrapped code. We propose to develop a correct and
secure compiler (targeting WebAssembly, an interesting new
language for running low-level code in web browsers) based on
the ideas of preserving OCPL specifications and robust safety.
This is meaningful because a compiler focused on such concrete
goals is easier to certify and can generate more efficient
code, compared to compilers organized around generic notions
of correctness and security.
Contact
Name(s):
Video Broadcast
Video Broadcast:YesTo Location:Kaiserslautern
To Building:G26To Room:111
Tags, Category, Keywords and additional notes
Note:
Attachments, File(s):
Created by:Maria-Louise Albrecht/MPI-KLSB, 11/24/2017 10:46 AMLast modified by:Maria-Louise Albrecht/MPI-KLSB, 11/24/2017 10:50 AM
  • Maria-Louise Albrecht, 11/24/2017 10:50 AM -- Created document.