Jan Menz, Andrew K. Hirsch, Peixuan Li, and Deepak Garg
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 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.
To Appear in OOPSLA 2023