Abstract
RV-Android is a new freely available open source runtime library for monitoring formal safety properties on Android. RV-Android uses the commercial RV-Monitor technology as its core monitoring library generation technology, allowing for the verification of safety properties during execution and operating entirely in userspace with no kernel or operating system modifications required. RV-Android improves on previous Android monitoring work by replacing the JavaMOP framework with RV-Monitor, a more advanced monitoring library generation tool with core algorithmic improvements that greatly improve resource consumption, efficiency, and battery life considerations. We demonstrate the developer usage of RV-Android with the standard Android build process, using instrumentation mechanisms effective on both Android binaries and source code. Our method allows for both property development and advanced application testing through runtime verification. We showcase the user frontend of RV-Monitor, which is available for public demo use and requires no knowledge of RV concepts. We explore the extra expressiveness the MOP paradigm provides over simply writing properties as aspects through two sample security properties, and show an example of a real security violation mitigated by RV-Android on-device. Lastly, we propose RV as an extension to the next-generation Android permissions system debuting in Android M.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Google Inc.: Android Developers (2014). http://developers.android.com
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)
Bauer, A., Küster, J.-C., Vegliach, G.: Runtime verification meets Android security. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 174–180. Springer, Heidelberg (2012)
Falcone, Y., Currea, S.: Weave Droid: aspect-oriented programming on Android devices: fully embedded or in the cloud. In: [23], pp. 350–353
Eclipse: The AspectJ project (2014). http://eclipse.org/aspectj
Luo, Q., Zhang, Y., Lee, C., Jin, D., Meredith, P.O.N., Şerbănuţă, T.F., Roşu, G.: RV-Monitor: efficient parametric runtime verification with simultaneous properties. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 285–300. Springer, Heidelberg (2014)
Mulliner, C.: Dynamic binary instrumentation on Android (2012)
Bodden, E.: Instrumenting Android apps with Soot (2014). http://www.bodden.de/2013/01/08/soot-android-instrumentation/
Binns, P., Englehart, M., Jackson, M., Vestal, S.: Domain specific software architectures for guidance, navigation and control. J. Softw. Eng. Knowl. Eng. 6(2), 201–227 (1996)
Enck, W., Ongtang, M., McDaniel, P.: Understanding Android security. IEEE Secur. Priv. 7(1), 50–57 (2009)
Shabtai, A., Fledel, Y., Kanonov, U., Elovici, Y., Dolev, S., Glezer, C.: Google Android: a comprehensive security assessment. IEEE Secur. Priv. 8(2), 35–44 (2010)
Google Inc.: Runtime—Android Developers (2015). http://developer.android.com/reference/java/lang/Runtime.html
TrendMicro Security Intelligence Blog: Android ransomware uses tor (2014). http://blog.trendmicro.com/trendlabs-security-intelligence/android-ransomware-uses-tor/
PCWorld: Cybercriminals are using the Tor network to control their botnets. (2013) http://www.pcworld.com/article/2045183/
Google Inc.: Google report Android security 2014 year in review (2014). https://static.googleusercontent.com/media/source.android.com/en/us/devices/tech/security/reports/Google_Android_Security_2014_Report_Final.pdf
BGR: This will be the most important (and possibly most overlooked) new android m feature (2015). http://bgr.com/2015/05/28/android-m-granular-permissions-controls/
Android Police: Android M will never ask users for permission to use the internet, and that’s probably okay (2015) Published on the 06 June 2015 at www.androidpolice.com
Amalfitano, D., Fasolino, A.R., Tramontana, P., Carmine, S.D., Memon, A.M.: Using GUI ripping for automated testing of Android applications. In: [23], pp. 258–261. http://wpage.unina.it/ptramont/GUIRipperWiki.htm
Wontae Choi on Github: Swifthand (2015). https://github.com/wtchoi/swifthand
Arzt, S., Rasthofer, S., Fritz, C., Bodden, E., Bartel, A., Klein, J., Le Traon, Y., Octeau, D., McDaniel, P.: Flowdroid: precise context, flow, field, object-sensitive and lifecycle-aware taint analysis for Android apps. ACM SIGPLAN Not. 49, 259–269 (2014). ACM
Fritz, C., Arzt, S., Rasthofer, S., Bodden, E., Bartel, A., Klein, J., Le Traon, Y., Octeau, D., McDaniel, P.: Highly precise taint analysis for Android applications. EC SPRIDE, TU Darmstadt, Technical report (2013)
Bodden, E., Hendren, L., Lam, P., Lhoták, O., Naeem, N.A.: Collaborative runtime verification with tracematches. In: Sokolsky, O., Taşıran, S. (eds.) RV 2007. LNCS, vol. 4839, pp. 22–37. Springer, Heidelberg (2007)
Goedicke, M., Menzies, T., Saeki, M. (eds.): IEEE/ACM International Conference on Automated Software Engineering, ASE 2012, Essen, Germany, 3–7 September. ACM (2012)
Acknowledgements
We would like to thank Patrick Meredith for developing the initial prototype of RV-Monitor applied to Android applications and continued feedback, as well as our partners at ITC and Denso for their continued support in the investigation of Android-related work for the automotive domain. We would also like to thank the miSecurity application team, for providing a basis for the graphical user frontend we describe.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Daian, P. et al. (2015). RV-Android: Efficient Parametric Android Runtime Verification, a Brief Tutorial. In: Bartocci, E., Majumdar, R. (eds) Runtime Verification. Lecture Notes in Computer Science(), vol 9333. Springer, Cham. https://doi.org/10.1007/978-3-319-23820-3_24
Download citation
DOI: https://doi.org/10.1007/978-3-319-23820-3_24
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-23819-7
Online ISBN: 978-3-319-23820-3
eBook Packages: Computer ScienceComputer Science (R0)