Write a Blog >>
ICFP 2019
Sun 18 - Fri 23 August 2019 Berlin, Germany
Mon 19 Aug 2019 14:15 - 14:37 at Aurora Borealis - Verified Compilation Chair(s): Ralf Jung

Separation logic is a powerful program logic for the static modular verification of imperative programs. However, dynamic checking of separation logic contracts on the boundaries between verified and untrusted modules is hard, because it requires one to enforce (among other things) that outcalls from a verified to an untrusted module do not access memory resources currently owned by the verified module.

This paper proposes an approach to dynamic contract checking by relying on support for capabilities, a well-studied form of unforgeable memory pointers that enables fine-grained, efficient memory access control. More specifically, we rely on a form of capabilities called linear capabilities for which the hardware enforces that they cannot be copied.

We formalize our approach as a fully abstract compiler from a statically verified source language to an unverified target language with support for linear capabilities. The key insight behind our compiler is that memory resources described by spatial separation logic predicates can be represented at run time by linear capabilities. The compiler is separation-logic-proof-directed: it uses the separation logic proof of the source program to determine how memory accesses in the source program should be compiled to linear capability accesses in the target program.

The full abstraction property of the compiler essentially guarantees that compiled verified modules can interact with untrusted target language modules as if they were compiled from verified code as well.

Mon 19 Aug

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

13:30 - 15:00
Verified CompilationResearch Papers at Aurora Borealis
Chair(s): Ralf Jung MPI-SWS
13:30
22m
Talk
Narcissus: Correct-By-Construction Derivation of Decoders and Encoders from Binary Formats
Research Papers
Benjamin Delaware Purdue University, Sorawit Suriyakarn , Clément Pit-Claudel MIT CSAIL, Qianchuan Ye Purdue University, Adam Chlipala Massachusetts Institute of Technology
Link to publication DOI Authorizer link
13:52
22m
Talk
Closure Conversion is Safe for Space
Research Papers
Zoe Paraskevopoulou Princeton University, Andrew Appel Princeton
14:15
22m
Talk
Linear capabilities for fully abstract compilation of separation-logic-verified code
Research Papers
Thomas Van Strydonck KULeuven, Frank Piessens KU Leuven, Dominique Devriese Vrije Universiteit Brussel
14:37
22m
Talk
The Next 700 Compiler Correctness Theorems. A Functional Pearl.
Research Papers
Daniel Patterson Northeastern University, Amal Ahmed Northeastern University, USA