Formalizing Stack Safety as a Security Property
Sean Noble Anderson, Roberto Blanco, Leonidas Lampropoulos, Benjamin C. Pierce, Andrew Tolmach
TL;DR
The paper tackles the challenge of formally defining stack safety by decomposing it into five properties—caller integrity, caller confidentiality, callee integrity, callee confidentiality, and well-bracketed control flow—within a security-augmented machine model. It introduces a modular security semantics layered on top of a conventional ISA, enabling property-based reasoning about stack activations, memory regions, and control flow with observable events. The framework is extended to support realistic features such as argument passing on the stack, tail calls, and callee-saves registers, and it is validated through QuickChick-based randomized testing against Roessler & DeHon’s Lazy Tagging and Clearing micro-policies, including mutation testing that uncovers failures and guides fixes. The work advances the ability to reason about stack safety across diverse enforcement mechanisms, offering a test-driven path toward stronger guarantees and guiding future exploration in capability-based architectures and beyond.
Abstract
The term stack safety is used to describe a variety of compiler, run-time, 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. We propose a new formal characterization of stack safety using concepts from language-based security. Rather than treating stack safety as a monolithic property, we decompose it into an integrity property and a confidentiality property for each of the caller and the callee, plus a control-flow property: five properties in all. This formulation is motivated by a particular class of enforcement mechanisms, the "lazy" stack safety micro-policies studied by Roessler and DeHon, which permit functions to write into one another's frames but taint the changed locations so that the frame's owner cannot access them. No existing characterization of stack safety captures this style of safety; we capture it here by stating our properties in terms of the observable behavior of the system. Our properties go further than previous formal definitions of stack safety, supporting caller- and callee-saved registers, arguments passed on the stack, and tail-call elimination. We validate the properties by using them to distinguish between correct and incorrect implementations of Roessler and DeHon's micro-policies using property-based random testing. Our test harness successfully identifies several broken variants, including Roessler and DeHon's lazy policy; a repaired version of their policy passes our tests.