Sites Inria

Seminaire des équipes de recheche

The Meaning of Memory Safety

© INRIA Sophie Auvin - P comme Protocole

We give 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. 

  • Date : 12/04/2018
  • Lieu : Inria de Paris - 2 rue Simone Iff - 75012 Paris, room Lions 2 - 11h00
  • Intervenants : Arthur Azevedo de Amorim (CMU)

The Meaning of Memory Safety

  • Intervenant : Arthur Azevedo de Amorim (CMU)

First, we show how a small memory-safe language validates a noninterference property: a program can neither affect nor be affected by unreachable parts of the state.

Second, we extend separation logic, a proof system for heap-manipulating programs, with a memory-safe variant of its frame rule.  The new rule is stronger because it applies even when parts of the program are buggy or malicious, but also weaker because it demands a stricter form of separation between parts of the program state.

We also consider a number of pragmatically motivated variations on 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.

Keywords: Séminaire Prosecco Inria de Paris Meaning Memory Safety

Haut de page

Suivez Inria tout au long de son 50e anniversaire et au-delà !