Expressing Security Properties Using Selective Interleaving Functions

TL;DR

This paper analyzes the expressive power of Selective Interleaving Functions (SIFs) in expressing security properties, showing limitations and proposing a generalized version that overcomes these constraints.

Contribution

It demonstrates the limitations of SIFs in capturing certain security properties and introduces a generalized SIF framework that can express more properties like NOS and is closed under conjunction.

Findings

SIFs cannot express nondeducibility on strategies (NOS)

The set of properties expressed by SIFs is not closed under conjunction

Generalized SIFs can express NOS and are closed under conjunction

Abstract

McLean's notion of Selective Interleaving Functions (SIFs) is perhaps the best-known attempt to construct a framework for expressing various security properties. We examine the expressive power of SIFs carefully. We show that SIFs cannot capture nondeducibility on strategies (NOS). We also prove that the set of security properties expressed with SIFs is not closed under conjunction, from which it follows that separability is strictly stronger than double generalized noninterference. However, we show that if we generalize the notion of SIF in a natural way, then NOS is expressible, and the set of security properties expressible by generalized SIFs is closed under conjunction.