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

TitleA Refinement Based Notion of Non-interference for Interface Automata: Compositionality, Decidability and Synthesis
Publication TypeConference Paper
Year of Publication2010
AuthorsLee, MD, D'Argenio, PR
Conference NameSCCC 2010, Proceedings of the XXIX International Conference of the Chilean Computer Science Society
PublisherIEEE Computer Society
AbstractInterface 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.
DOI10.1109/SCCC.2010.14
PDF (Full text):