Hier finden Sie wissenschaftliche Publikationen aus den Fraunhofer-Instituten.

Non-interference on UML state-charts

: Ochoa, M.


Furia, Carlo A.:
Objects, models, components, patterns. 50th international conference, TOOLS 2012 : Prague, Czech Republic, May 29 - 31, 2012; proceedings
Berlin: Springer, 2012 (Lecture Notes in Computer Science 7304)
ISBN: 978-3-642-30560-3 (Print)
ISBN: 978-3-642-30561-0 (Online)
ISBN: 3-642-30560-1
ISSN: 0302-9743
International Conference on Objects, Models, Components, Patterns (TOOLS) <50, 2012, Prague>
Fraunhofer ISST ()

Non-interference is a semantically well-defined property that allows one to reason about the security of systems with respect to information flow policies for groups of users. Many of the security problems of implementations could be already spotted at design time if information flow would be a concern in early phases of software development. In this paper we propose a methodology for automatically verifying the interaction of objects whose behaviour is described by deterministic UML State-charts with respect to information flow policies, based on the socalled unwinding theorem. We have extended this theorem to cope with the particularities of state-charts: the use of variables, guards, actions and hierarchical states and derived results about its compositionality. In order to validate our approach, we report on an implementation of our enhanced unwinding techniques and applications to scenarios from the Smart Metering domain.