What exactly 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 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.
翻译:“ 堆叠安全” 的确切含义是什么? 短语是指各种编译者、 运行时间和硬件机制来保护堆叠内存。 但这些机制通常缺乏精确的规格, 通常依赖非正式描述和他们防止的不良行为实例。 我们提议对堆叠安全进行正式定性, 其设计概念来自基于语言的安全: 完整财产( “ 每个调用者堆叠框中的私人状态” ) 、 保密财产( “ 被调用者的行为对调用者的私人状态不敏感 ” ), 以及一个井井然有序的财产( “ 每一个被调用者将控制归到其直接的调用者 ” ) 。 我们使用这些属性来验证罗斯勒和德洪[ 2018] 提出的堆叠安全“ 宏观政策” 。 具体地说, 我们检查( 以地产为基础的随机测试), Roessler 和 Dehon的“ eger” 微观政策( ), 尽可能早地捕捉到违规情况, 执行简单的“ ” 变式的“ ”, 正确探测到几个变式的变式, 的变式“ 和变式“ 的“ 较弱的变式” 。