Formalizing Stack Safety as a Security Property

2023

Download

Conference / Journal

Authors

Andrew Tolmach Benjamin Crawford Pierce Leonidas Lampropoulos Roberto Blanco Sean Noble Anderson

Research Hub

Research Hub C: Sichere Systeme

Research Challenges

RC 7: Building Secure Systems
RC 8: Security with Untrusted Components

Abstract

The term stack safety is used to describe a variety of compiler, runtime, and hardware mechanisms for protecting stack memory. Unlike “the heap,” the ISA-level stack does not correspond to a single high-level language concept: different compilers use it in different ways to support procedural and functional abstraction mechanisms from a wide range of languages. This protean nature makes it difficult to nail down what it means to correctly enforce stack safety.