A hyperproperty relates executions of a program and is used to formalize security objectives such as confidentiality, non-interference, privacy, and anonymity. Formally, a hyperproperty is a collection of allowable sets of executions. A program violates a hyperproperty if the set of its executions is not in the collection specified by the hyperproperty. The logic HyperCTL^* has been proposed in the literature to formally specify and verify hyperproperties. The problem of checking whether a finite-state program satisfies a HyperCTL^* formula is known to be decidable. However, the problem turns out to be undecidable for procedural (recursive) programs. Surprisingly, we show that decidability can be restored if we consider restricted classes of hyperproperties, namely those that relate only those executions of a program which have the same call-stack access pattern. We call such hyperproperties, \emph{stack-aware hyperproperties.} Our decision procedure can be used as a proof method for establishing security objectives such as noninference for recursive programs, and also for refuting security objectives such as observational determinism. Further, if the call stack size is observable to the attacker, the decision procedure provides exact verification.

翻译：超属性关联程序的执行轨迹，用于形式化表达机密性、非干扰、隐私和匿名性等安全目标。从形式上看，超属性是允许执行的集合族。若某程序的执行集合不属于超属性所规定的集合族，则该程序违反该超属性。学界已提出逻辑HyperCTL^*用于超属性的形式化规范与验证，且已知对于有限状态程序，验证其是否满足HyperCTL^*公式的问题是可判定的。然而对于过程式（递归）程序，该问题被证明不可判定。令人惊讶的是，我们发现若仅考虑一类受限超属性——即仅关联具有相同调用堆栈访问模式的程序执行轨迹，可判定性可以恢复。我们将此类超属性称为"堆栈感知超属性"。我们的判定程序可作为证明方法，用于建立递归程序的安全性目标（如非推理性质），也可用于反驳安全性目标（如观测确定性）。此外，若攻击者可观测调用堆栈大小，该判定程序能提供精确验证。