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

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

• Thomas Van Strydonck, KU Leuven
• Monday 18 March 2019, 11:45-12:15
• FW26.

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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• FW26
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.