BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY: Linear capabilities for fully abstract compilation of separation-
 logic-verified code - Thomas Van Strydonck\, KU Leuven
DTSTART:20190318T114500Z
DTEND:20190318T121500Z
UID:TALK121768@talks.cam.ac.uk
CONTACT:Victor Gomes
DESCRIPTION:Separation logic is the basis for many tools that support soun
 d\,\n modular verification of programs\, such as VeriFast. We are concerne
 d\n with scenarios where separation-logic-verified code interacts with\n u
 ntrusted\, non-verified code (for example\, when installing plugins from\n
  the internet). Our goal is to compile the verified code in such a way\n t
 hat we can preserve the guarantees obtained from verification\, even\n und
 er this untrusted interaction. This preservation of guarantees can\n be ex
 pressed in terms of the notion of fully abstract compilation: a\n formal p
 roperty that is sometimes used to define secure compilation. We\n contribu
 te a new approach to secure compilation of verified to\n unverified C code
  that we conjecture to be fully abstract. The approach\n relies on target 
 language support for capabilities: a well-studied form\n of unforgeable me
 mory pointers that enables fine-grained\, efficient\n privilege separation
 . We rely on a form of capabilities called linear\n capabilities. Linear c
 apabilities are specially treated by the hardware\n to ensure that they ca
 n never be copied. Our compiler relies on\n information from both the sour
 ce program and its verification proof\,\n i.e. it will be formally defined
  as a separation-logic-proof-directed\n compiler.
LOCATION:FW26
END:VEVENT
END:VCALENDAR