Sat 13 Jan 2018 11:30 - 11:35 at Hershey - Short Talks Session Chair(s): Dominique Devriese

We propose a rigorous characterization of what it means for a programming language to be memory safe, capturing the intuition that memory safety supports local reasoning about state. We formalize this principle in two ways. First, we show how a small memory-safe imperative language validates a noninterference property: a program can neither affect nor be affected by parts of the state it cannot reach. Second, we show how to take advantage of memory safety to extend separation logic with a variant of its frame rule. Our new rule is stronger because it applies even when parts of the program are buggy or malicious, but also weaker because it requires a stricter form of separation between parts of the program state. We also consider a number of pragmatically motivated variations of memory safety and the reasoning principles they support. As an application of our characterization, we evaluate the security of a previously proposed dynamic monitor for memory safety of heap-allocated data.

Slides (main.pdf)154KiB

Sat 13 Jan

11:30 - 12:00: PriSC 2018 - Short Talks Session at Hershey
Chair(s): Dominique DevrieseKU Leuven
prisc-2018151583940000011:30 - 11:35
Arthur Azevedo de AmorimCarnegie Mellon University, USA, Cătălin HriţcuInria Paris, Benjamin C. PierceUniversity of Pennsylvania
Pre-print File Attached
prisc-2018151583970000011:35 - 11:40
William J. BowmanNortheastern University, USA
Link to publication File Attached
prisc-2018151584000000011:40 - 11:45
Santosh NagarakatteRutgers University, USA
Pre-print File Attached
prisc-2018151584030000011:45 - 11:50
Jonathan ProtzenkoMicrosoft Research, n.n.
File Attached