Capturing Inter-process Communication for Runtime Verification on Android

  • Alex Villazón
  • Haiyang SunEmail author
  • Walter Binder
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11247)


Runtime verification (RV) covering the whole Android system is challenging, due to the lack of support for analyzing and monitoring events across multiple processes. Existing RV frameworks for Android, which are often built on top of RV tools for Java, only support single-process monitoring. In this paper, we describe an RV framework for Android, capable of performing RV across multiple Android components in different processes by capturing inter-process-communication events. Our approach features an extended regular expression formalism, allowing one to specify RV properties to describe event patterns across processes. We illustrate the use of our framework by detecting nested indirect service use through proxy processes, which is not possible with prevailing RV tools on Android.



The work presented in this paper has been supported by Swiss National Science Foundation (scientific exchange project IZSEZ0_177215) and by Hasler Foundation (project 18012). The research was conducted while A. Villazón was with Università della Svizzera italiana.


  1. 1.
    Backes, M., Gerling, S., Hammer, C., Maffei, M., von Styp-Rekowsky, P.: AppGuard – enforcing user requirements on Android apps. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 543–548. Springer, Heidelberg (2013). Scholar
  2. 2.
    Bosu, A., Liu, F., Yao, D.D., Wang, G.: Collusive data leak and more: large-scale threat analysis of inter-app communications. In: ASIA CCS, pp. 71–85 (2017)Google Scholar
  3. 3.
    Colombo, C., Pace, G.J., Schneider, G.: LARVA–safer monitoring of real-time Java programs (tool paper). In: SEFM, pp. 33–37 (2009)Google Scholar
  4. 4.
    Daian, P., et al.: RV-Android: efficient parametric android runtime verification, a brief tutorial. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 342–357. Springer, Cham (2015). Scholar
  5. 5.
    Falcone, Y., Currea, S., Jaber, M.: Runtime verification and enforcement for android applications with RV-Droid. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol. 7687, pp. 88–95. Springer, Heidelberg (2013). Scholar
  6. 6.
    Jin, D., Meredith, P.O.N., Lee, C., Roşu, G.: JavaMOP: efficient parametric runtime monitoring framework. In: ICSE, pp. 1427–1430 (2012)Google Scholar
  7. 7.
    Kim, M., Kannan, S., Lee, I., Sokolsky, O., Viswanathan, M.: Java-MaC. ENTCS 55(2), 218–235 (2001)zbMATHGoogle Scholar
  8. 8.
    Küster, J.-C., Bauer, A.: Monitoring real android malware. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 136–152. Springer, Cham (2015). Scholar
  9. 9.
    Marek, L., Villazón, A., Zheng, Y., Ansaloni, D., Binder, W., Qi, Z.: DiSL: a domain-specific language for bytecode instrumentation. In: AOSD, pp. 239–250 (2012)Google Scholar
  10. 10.
    Reger, G., Cruz, H.C., Rydeheard, D.: MarQ: monitoring at runtime with QEA. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 596–610. Springer, Heidelberg (2015). Scholar
  11. 11.
    Sun, H., North, A., Binder, W.: Multi-process runtime verification for android. In: APSEC, pp. 701–706 (2017)Google Scholar
  12. 12.
    Sun, H., Rosà, A., Javed, O., Binder, W.: ADRENALIN-RV: android runtime verification using load-time weaving. In: ICST, pp. 532–539 (2017)Google Scholar
  13. 13.
    Xiang, C., Qi, Z., Binder, W.: Flexible and extensible runtime verification for Java (Extended Version). Int. J. Softw. Eng. Knowl. Eng. 25, 1595–1609 (2015)CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.Universidad Privada Boliviana (UPB)ColcapirhuaBolivia
  2. 2.Università della Svizzera italiana (USI)LuganoSwitzerland

Personalised recommendations