A Refinement Based Notion of Non-interference for Interface Automata: Compositionality, Decidability and Synthesis

Interface automata (IA) introduce a framework to model stateful interfaces. Interface structures for security (ISS) extend IA to cope with security properties. In this article, we argue that bisimulation-based non interference is not quite appropriate to characterize security on ISS. We instead introduce refinement-based variants of non-interference that fit better in this context. Moreover, we show that these new properties are not preserved by composition, but give sufficient conditions to ensure compositionality. We give two algorithms. The first one determines if an ISS satisfies the refinement-based non-interference property. The second one, determines if an ISS can be made secure by controlling some input actions and, if so, synthesizes the secure ISS.