Compositional security definitions for higher-order where declassification

TL;DR

This paper introduces a new compositional security definition for higher-order programs with declassification, using logical relations to model where declassification occurs, enhancing security guarantees over previous lower-order definitions.

Contribution

It develops a novel security model for higher-order declassification using logical relations, addressing the lack of compositional definitions in this setting.

Findings

The new security definition is more secure than previous lower-order models.

Logical relations effectively model where declassification occurs in higher-order programs.

Stopping indistinguishability enforcement after relevant declassification improves security.

Abstract

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]).