Abstraction-Based Synthesis of Opacity-Enforcing Controllers using Alternating Simulation Relations

Opacity is an important information-flow security property that captures the plausible deniability for some "secret" of a system. In this paper, we investigate the problem of synthesizing controllers that enforce opacity for labeled transition systems (LTS). Most of the existing works on synthesis of opacity-enforcing controllers are based on the original system model, which may contain a large number of states. To mitigate the complexity of the controller synthesis procedure, we propose an abstraction-based approach for controller synthesis. Specifically, we propose notion of opacity-preserving alternating (bi)simulation relation for the purpose of abstraction. We show that, if the abstract system is opacity-preserving alternatingly simulated by the original system which may be significantly smaller, then we can synthesize an opacity-enforcing controller based on the abstract system and then refine it back to a controller enforcing opacity of the original system. We investigate both initial-state opacity and infinite-step opacity. We also show the effectiveness of the proposed approach by a set of examples.