一句话：用逻辑关系为高阶程序中的 where 解分类构建可组合安全定义，并证明其比已有低阶定义更安全。
论文关注信息流安全中的解分类（declassification）问题：程序常需在特定位置公开部分私有数据，其中 where 解分类允许在程序的特定部分进行解分类。已有安全定义大多无法处理高阶程序，且在高阶设定下尚无针对 where 解分类这类内涵式信息流性质的可组合安全定义。作者使用逻辑关系（logical relations）构建 where 解分类的语义模型，并由此得到安全定义；其核心洞见是：一旦相关解分类已经发生，就不再强制不可区分性（indistinguishability）。该定义具备可组合性，作者进一步表明其提供的安全性强于此前针对低阶设定的最相关定义。评估以形式化论证与比较为主。
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 bedeclassified. 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 aswheredeclassification, 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 arelevant declassificationhas occurred. We show that the resulting security definition provides more security than the most related previous definition, which is for the lower-order setting.
@article{paperbot2040,
title = {Compositional Security Definitions for Higher-Order Where Declassification},
author = {Jan Menz and Andrew K. Hirsch and Peixuan Li and Deepak Garg},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {OOPSLA1},
year = {2023},
doi = {10.1145/3586041}
}