Formalizing Stack Safety as a Security Property

The term stack safety is used for 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 formal characterization of stack safety using concepts from language-based security. Rather than packaging all aspects of stack safety into 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~\cite{DBLP:conf/sp/RoesslerD18}, which permit functions to write into one another's frames, but which taint the changed locations so that the frame's owner cannot access it. 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 our 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 does pass our tests.