Unwinding Conditional Noninterference

TL;DR

This paper introduces a flexible framework for conditional noninterference policies that encompass transitive and intransitive policies, supporting dynamic security requirements and providing sound and complete unwinding relations.

Contribution

It defines a new framework for conditional noninterference that generalizes existing policies and introduces unwinding relations for these policies.

Findings

The framework subsumes transitive and intransitive noninterference policies.

Supports dynamic security requirements like upgrading and downgrading.

Provides sound and complete unwinding relations for the new policies.

Abstract

Noninterference provides a control over information flow in a system for ensuring confidentiality and integrity properties. In the literature this notion has been well studied as transitive noninterference and intransitive noninterference. In this paper we define a framework on the notion of conditional noninterference, which allows to specify information flow policies based on the semantics of action channels. Our new policies subsume the policies of both transitive and intransitive noninterference, and support dynamic requirements such as upgrading and downgrading. We also present unwinding relations that are both sound and complete for the new policies.