Opacity From Observers With a Bounded Memory

Opacity is an information-flow property capturing privacy from observers that are aware of a system's dynamics. The potential for an observer with perfect recall to reason about long histories of the system poses a challenge for opacity verification. In this letter, we address this challenge by proposing a new notion of opacity over automata, called bounded memory opacity, with respect to an observer with a bounded memory. We show that verifying this weaker notion of opacity has reduced computational complexity compared to general opacity (co- NP vs. PSPACE). Furthermore, we present a corresponding verification algorithm using an encoding to the Boolean satisfiability problem (SAT). We demonstrate this approach on randomly generated automata as well as a Web server load-hiding example.

Automated summary

Opacity is a property that protects privacy by preventing observers from inferring a system's dynamics. We propose a new notion called bounded memory opacity, which addresses the challenge of verifying opacity when an observer has limited memory. We show that verifying this weaker notion has reduced computational complexity compared to general opacity. Additionally, we present a verification algorithm using Boolean satisfiability problem encoding, and demonstrate its effectiveness on randomly generated automata and a Web server load-hiding example.