Opacity with Orwellian Observers and Intransitive Non-interference

TL;DR

This paper introduces a new form of opacity called Orwellian partial observability, analyzes its verification complexity, and relates it to intransitive non-interference, expanding security property frameworks.

Contribution

It formalizes Orwellian partial observability, provides verification methods for regular secrets, and establishes the equivalence with intransitive non-interference.

Findings

Verification of opacity under Orwellian projection is decidable for regular languages.

Opacity verification is undecidable for general Orwellian observation functions.

Opacity is equivalent to intransitive non-interference in regular secrets.

Abstract

Opacity is a general behavioural security scheme flexible enough to account for several specific properties. Some secret set of behaviors of a system is opaque if a passive attacker can never tell whether the observed behavior is a secret one or not. Instead of considering the case of static observability where the set of observable events is fixed off line or dynamic observability where the set of observable events changes over time depending on the history of the trace, we consider Orwellian partial observability where unobservable events are not revealed unless a downgrading event occurs in the future of the trace. We show how to verify that some regular secret is opaque for a regular language L w.r.t. an Orwellian projection while it has been proved undecidable even for a regular language L w.r.t. a general Orwellian observation function. We finally illustrate relevancy of our results by proving the equivalence between the opacity property of regular secrets w.r.t. Orwellian projection and the intransitive non-interference property.