Existential Types for Relaxed Noninterference

TL;DR

This paper introduces a new approach to relaxed noninterference in information-flow security by using existential types for declassification policies, enabling expressive and advanced security policies in non-object-oriented languages.

Contribution

It proposes an existential types-based method for relaxed noninterference, extending prior label-as-types approaches with a more flexible abstraction mechanism.

Findings

Formalization of existential relaxed noninterference in a core calculus

Proof that well-typed programs satisfy the new security property

Enhanced expressiveness for declassification policies

Abstract

Information-flow security type systems ensure confidentiality by enforcing noninterference: a program cannot leak private data to public channels. However, in practice, programs need to selectively declassify information about private data. Several approaches have provided a notion of relaxed noninterference supporting selective and expressive declassification while retaining a formal security property. The labels-as-functions approach provides relaxed noninterference by means of declassification policies expressed as functions. The labels-as-types approach expresses declassification policies using type abstraction and faceted types, a pair of types representing the secret and public facets of values. The original proposal of labels-as-types is formulated in an object-oriented setting where type abstraction is realized by subtyping. The object-oriented approach however suffers from limitations due to its receiver-centric paradigm. In this work, we consider an alternative approach to labels-as-types, applicable in non-object-oriented languages, which allows us to express advanced declassification policies, such as extrinsic policies, based on a different form of type abstraction: existential types. An existential type exposes abstract types and operations on these; we leverage this abstraction mechanism to express secrets that can be declassified using the provided operations. We formalize the approach in a core functional calculus with existential types, define existential relaxed noninterference, and prove that well-typed programs satisfy this form of type-based relaxed noninterference.