Runtime Verification meets Android Security

Right now, this page serves more or less as a placeholder for demonstrating a prototypic implementation of a runtime verification framework on Android.

If the above link does not work, go directly to YouTube to see the video.

Accompanying papers

2012

The above video serves as background material to the following NFM'12 short paper, which discusses our runtime verification approach on Android phones:

• Andreas Bauer, Jan-Christoph Küster, and Gil Vegliach.
  Runtime Verification meets Android Security.
  In A. Goodloe and S. Person, editors, Proceedings of the 4th NASA Formal Methods Symposium (NFM), volume 7226 of Lecture Notes in Computer Science, pages 174-180. Springer-Verlag, Berlin, Heidelberg, April 2012. © Copyright Springer-Verlag.
  [pdf] [bibtex-entry]

2013

Vastly improved presentation of our logic, LTLFO, that was used in the previous paper to monitor Apps. New, more efficient monitoring algorithm based on automata.

• Andreas Bauer, Jan-Christoph Küster, and Gil Vegliach.
  From propositional to first-order monitoring.
  Computing Research Repository (CoRR) abs/1303.3645. Association for Computing Machinery (ACM), March 2013.
  [html] [pdf] [bibtex-entry]

Tool downloads

Coming soon...