Opacity with Orwellian Observers and Intransitive Non-interference
This addresses security verification for systems with dynamic observability, providing a decidable method for a previously undecidable problem, though it is incremental as it focuses on a specific projection case.
The paper tackles the verification of opacity, a security property where a passive attacker cannot distinguish secret behaviors, under Orwellian partial observability where unobservable events are revealed only after downgrading events. It shows that verifying opacity for regular secrets with Orwellian projection is decidable, unlike general Orwellian observation functions, and proves equivalence to intransitive non-interference.
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.