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.

翻译：“栈安全性”这一术语用于描述一系列保护栈内存的编译器、运行时及硬件机制。与“堆”不同，指令集架构（ISA）层面的栈并不对应单一高级语言概念：不同编译器以不同方式利用它来支持多种语言中的过程式与函数式抽象机制。这种多变性使得准确定义栈安全性的正确实施变得困难。我们提出了一种基于语言安全概念的栈安全性形式化表征。我们并未将栈安全性的所有方面打包为一个单一属性，而是将其分解为：调用者与被调用者各自的完整性属性与机密性属性，再加上一个控制流属性——共计五种属性。这一构建源于Roessler与DeHon（引用自DBLP:conf/sp/RoesslerD18）研究的特定类别的实施机制——“惰性”栈安全微策略，该机制允许函数写入对方的栈帧，但会对所修改的位置进行污染，使得帧所有者无法再访问这些位置。现有的栈安全性表征均未捕捉到这种安全风格。我们通过基于系统可观察行为来表述属性，在此予以捕捉。我们的属性超越了以往栈安全性的形式化定义，支持调用者保存与被调用者保存寄存器、通过栈传递的参数以及尾调用消除。我们通过基于属性的随机测试，利用这些属性来区分Roessler与DeHon微策略的正确与错误实现，从而验证了这些属性。我们的测试框架成功识别出多个有缺陷的变体，包括Roessler与DeHon的惰性策略；而修复后的策略版本则通过了我们的测试。