Temporal safety for stack allocated memory on capability machines

Stelios Tsampas, Dominique Devriese, Frank Piessens

Research output: Chapter in Book/Report/Conference proceedingConference paper

3 Citations (Scopus)
59 Downloads (Pure)


Memory capabilities as supported in capability machines are very similar to fat pointers, and hence are very useful for the efficient enforcement of spatial memory safety. Enforcing temporal memory safety however, is more challenging. This paper investigates an approach to enforce temporal memory safety for stack-allocated memory in C-like languages by extending capabilities with a simple dynamic mechanism. This mechanism ensures that capabilities with a certain lifetime can only be stored in memory that has a longer lifetime. Our mechanism prevents temporal memory safety violations, yet is sufficiently permissive to allow typical C coding idioms where addresses of local variables are passed up the call stack. We formalize the desired behavior of a simple C-like language as a dependently typed operational semantics, and we show that existing compilers to capability machines do not simulate this desired behavior: they either have to break temporal safety, or they have to defensively rule out allowed behaviors. Finally, we show that with our proposed dynamic mechanism, our compiler is fully abstract.
Original languageEnglish
Title of host publication32nd IEEE Computer Security Foundations Symposium
Number of pages13
ISBN (Electronic)978-1-7281-1407-1
ISBN (Print)978-1-7281-1408-8
Publication statusPublished - Jun 2019
Event32nd IEEE Computer Security Foundations Symposium - Hoboken, NJ, United States
Duration: 25 Jun 201928 Jun 2019
Conference number: 32

Publication series

NameIEEE Computer Security Foundations Symposium (CSF)
ISSN (Electronic)2374-8303


Conference32nd IEEE Computer Security Foundations Symposium
Abbreviated titleCSF
CountryUnited States
CityHoboken, NJ
Internet address


  • capabilities
  • temporal memory safety
  • machine-checked proof


Dive into the research topics of 'Temporal safety for stack allocated memory on capability machines'. Together they form a unique fingerprint.

Cite this