From propositional to First-order monitoring

Jan-Christoph Kuester (NICTA)

In the area of runtime verification a monitor typically describes a device or program which is automatically generated from a formal specification capturing undesired (resp. desired) system behaviour. The monitor?s task is to passively observe a running system in order to detect if the behavioural specification has been satisfied or violated by the observed system behaviour. While, arguably, the majority of runtime verification approaches are based on propositional logic, their expressiveness is insufficient, e.g., to monitor properties involving data in the scenario of smartphone security. To watch the secure behaviour of so-called 'apps' it is arguably not sufficient to merely record the fact that an app just sent an SMS, but also the associated phone number of that event in order to distinguish an intended use of the SMS facility from misuse due to malware activity. One way to distinguish these use cases would be to monitor a policy stating that ?the phone number of every outgoing SMS has to be in the users contact list?

In this talk, I will introduce a custom first-order temporal logic, LTLFO, and a corresponding monitor construction based on a new type of automaton, called spawning automaton. LTLFO was originally developed for the specification of runtime verification properties of Android 'Apps' and has already been used in that context. As monitoring a specification in LTLFO is an undecidable decision problem, the presented monitor is incomplete albeit sound. Furthermore, I will discuss experimental results from an implementation. These seem to substantiate my hypothesis that the automata-based construction leads to efficient runtime monitors whose size does not grow with increasing trace lengths (as is often observed in similar approaches). However, there exist formulae for which growth is unavoidable, irrespective of the chosen monitoring approach.
BIO:
Jan is a PhD student of Andreas Bauer at NICTA and is also associated with the Computer Systems Group at RSCS ANU. Previously he studied at the University of M??nster where he earned a Masters in Computer Science