Security Properties for Stack Safety.
Sean Noble Anderson, Leonidas Lampropoulos, Roberto Blanco, Benjamin C. Pierce, Andrew P. Tolmach · arXiv (Cornell University) · 2021
What exactly does 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 bad behaviors that they prevent. We propose a formal characterization of stack safety, formulated with 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), a confidentiality property (the callee's behavior is insensitive to the caller's private state), and a well-bracketedness property (each callee returns control to its immediate caller). 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 Roessler and Dehon's eager micro-policy, which catches violations as early as possible, enforces a simple stepwise variant of our properties and correctly detects several broken variants, and that (a repaired version of) their more performant lazy micro-policy corresponds to a slightly weaker and more extensional observational variant of our properties.