Describing Secure Interfaces with Interface Automata

Interface automata are a model that allows for the representation of stateful interfaces. In this paper we introduce a variant of interface automata, which we call interface structure for security (ISS), that allows for the modelling of security. We focus on the property of non interference, more precisely in bisimulation-based non interference for reactive systems. We define the notion of compatible interfaces in this setting meaning that they can be composed so that a secure interface can be synthesized from the composition. In fact, we provide an algorithm that determines whether an ISS can be made secure by controlling (more specifically, pruning) some public input actions, and if so, synthesize the secure ISS. In addition, we also provide some sufficient conditions on the components ISS to ensure that their composition is secure (and hence no synthesis process is needed).