Controller Synthesis for Non-Interference Properties

In this paper, we focus on the synthesis of secure systems. We assume the system is composed of two users, the low level and the high level users. The security property the system must satisfy is a non- interference property. A system is non-interferent if the low level user cannot deduce any information about the system by playing its low level actions. Various notions of non-interference have been defined in the literature, and in this paper we consider the most popular ones: trace- based non-interference (SNNI) and (bi)simulation-based non-interference (CSNNI and BSNNI). For each of these notions, we study the correspond- ing synthesis problem, i.e., build a controller s.t. the controlled system is non-interferent.