To ensure programs do not leak private data, we often want to be able to provide formal guarantees ensuring such data is handled correctly. Often, we cannot keep such data secret entirely; instead programmers specify how private data may be declassified. While security definitions for declassification exist, they mostly do not handle higher-order programs. In fact, in the higher-order setting no compositional security definition exists for intensional information-flow properties such as where declassification, which allows declassification in specific parts of a program. We use logical relations to build a model (and thus security definition) of where declassification. The key insight required for our model is that we must stop enforcing indistinguishability once a \emph{relevant declassification} has occurred. We show that the resulting security definition provides more security than the most related previous definition, which is for the lower-order setting. This paper is an extended version of the paper of the same name published at OOPSLA 2023 ([21]).

翻译：为了确保程序不泄露私有数据，我们通常希望能够提供形式化保证，确保这类数据得到正确处理。然而，私有数据往往无法完全保密；相反，程序员需要指定私有数据可以如何被降级。虽然已有针对降级的安全定义，但大多数定义无法处理高阶程序。事实上，在高阶设置中，对于诸如“何处降级”（允许在程序的特定部分进行降级）这类内涵信息流属性，并不存在组合性的安全定义。我们利用逻辑关系构建了一个关于“何处降级”的模型（从而定义了安全）。我们模型的关键洞见在于：一旦发生了相关降级，必须停止强制执行不可区分性。我们证明，所得的安全定义比之前最相关的定义（针对低阶设置）提供了更高的安全性。本文是发表于OOPSLA 2023同名论文（[21]）的扩展版本。