Skip to main content


Runtime verification meets android security


Andreas Bauer, Jan-Christoph Kuester and Gil Vegliach


Australian National University

Vienna Univ. of Technology


A dynamic security mechanism for Android-powered devices based on runtime verification known in the security community as behavioural detection is introduced, which lets users monitor the behaviour of installed applications. The general idea and a prototypical implementation are outlined, an application to real-world security threats shown, and the underlying logical foundations, relating to the employed specification formalism, sketched.

BibTeX Entry

    publisher        = {Springer},
    author           = {Bauer, Andreas and Kuester, Jan-Christoph and Vegliach, Gil},
    month            = apr,
    year             = {2012},
    keywords         = {monitoring, runtime verification, first-order temporal logic, android, mobile security},
    title            = {Runtime Verification meets Android Security},
    booktitle        = {4th NASA Formal Methods Symposium (NFM)},
    pages            = {174--180},
    address          = {Norfolk, Virginia, USA}


Served by Apache on Linux on seL4.