Formalizing Stack Safety as a Security Property

What does "stack safety" mean? The phrase is associated with a variety of compiler, run-time, and hardware mechanisms for protecting stack memory, but these mechanisms typically lack precise specifications, relying instead on informal descriptions and examples of the bad behaviors that they prevent. We propose a generic, formal characterization of stack safety based on concepts from language-based security: a combination of an integrity property ("the private state in each caller's stack frame is held invariant by the callee"), and a confidentiality property ("the callee's behavior is insensitive to the caller's private state"), plus an optional control-flow property. We use these properties to validate the stack safety micro-policies proposed by Roessler and DeHon [2018]. Specifically, we check (with property-based random testing) that their "eager" micro-policy, which catches violations early, enforces a simple "stepwise" variant of our properties, and that (a repaired version of) their more performant "lazy" micro-policy enforces a slightly weaker and more extensional observational property. Meanwhile our testing successfully detects violations in several broken variants, including Roessler and DeHon's original lazy policy.