Write a Blog >>
SPLASH 2017
Sun 22 - Fri 27 October 2017 Vancouver, Canada
Thu 26 Oct 2017 15:52 - 16:15 at Regency C - Verification in Practice Chair(s): Davide Ancona

In scenarios such as web programming, where code is linked together from multiple sources, \emph{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 program verification have never been properly formalized. In this paper, building on the recently developed Iris framework for concurrent separation logic, we develop OCPL, the first program logic for compositionally specifying and verifying OCPs in a language with closures, mutable state, and concurrency. The key idea of OCPL is to account for the interface between verified and untrusted code by adopting a well-known idea from the literature on security protocol verification, namely \emph{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. We use OCPL to give the first general, compositional, and machine-checked specs for several commonly-used OCPs—including the \emph{dynamic sealing}, \emph{membrane}, and \emph{caretaker} patterns—which we then use to verify robust safety for representative client code. All our results are fully mechanized in the Coq proof assistant.

Thu 26 Oct

Displayed time zone: Tijuana, Baja California change

15:30 - 17:00
Verification in PracticeOOPSLA at Regency C
Chair(s): Davide Ancona University of Genova
15:30
22m
Talk
A Model for Reasoning about JavaScript Promises
OOPSLA
Magnus Madsen University of Waterloo, Ondřej Lhoták University of Waterloo, Canada, Frank Tip Northeastern University
DOI
15:52
22m
Talk
Robust and Compositional Verification of Object Capability Patterns
OOPSLA
David Swasey MPI-SWS, Germany, Deepak Garg Max Planck Institute for Software Systems, Derek Dreyer MPI-SWS
DOI
16:15
22m
Talk
A Verified Messaging System
OOPSLA
William Mansky Princeton University, Andrew W. Appel Princeton, Aleksey Nogin HRL Laboratories, LLC
DOI
16:37
22m
Talk
Who Guards the Guards? Formal Validation of the ARM v8-M Architecture Specification
OOPSLA
DOI