University of Cambridge > > Logic and Semantics Seminar (Computer Laboratory) >  Linear capabilities for fully abstract compilation of separation-logic-verified code

Linear capabilities for fully abstract compilation of separation-logic-verified code

Add to your list(s) Download to your calendar using vCal

  • UserThomas Van Strydonck, KU Leuven
  • ClockMonday 18 March 2019, 11:45-12:15
  • HouseFW26.

If you have a question about this talk, please contact Victor Gomes.

Separation logic is the basis for many tools that support sound, modular verification of programs, such as VeriFast. We are concerned with scenarios where separation-logic-verified code interacts with untrusted, non-verified code (for example, when installing plugins from the internet). Our goal is to compile the verified code in such a way that we can preserve the guarantees obtained from verification, even under this untrusted interaction. This preservation of guarantees can be expressed in terms of the notion of fully abstract compilation: a formal property that is sometimes used to define secure compilation. We contribute a new approach to secure compilation of verified to unverified C code that we conjecture to be fully abstract. The approach relies on target language support for capabilities: a well-studied form of unforgeable memory pointers that enables fine-grained, efficient privilege separation. We rely on a form of capabilities called linear capabilities. Linear capabilities are specially treated by the hardware to ensure that they can never be copied. Our compiler relies on information from both the source program and its verification proof, i.e. it will be formally defined as a separation-logic-proof-directed compiler.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2023, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity