Graphical event model learning and verification for security assessment

Abstract

The main objective of our work is to assess the security of a given real world system by verifying whether this system satisfies given properties and, if not, how far it is from satisfying them. We are interested in performing formal verification of this system based on event sequences collected from its execution. In this paper, we propose a preliminary model-based approach where a Graphical Event Model (GEM), learned from the event streams, is considered to be representative of the underlying system. This model is then used to check a certain security property. If the property is not verified, we also propose a search methodology to find another close model that satisfies it. Our approach is generic with respect to the verification procedure and the notion of distance between models. For the sake of completeness, we propose a distance measure between GEMs that allows to give an insight on how far our real system is from verifying the given property. The interest of this approach is illustrated with a toy example.