Abstract
A dynamic security mechanism for Android-powered devices based on runtime verification 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.
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
Preview
Unable to display preview. Download preview PDF.
References
Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Trans. Softw. Eng. Methodol. (TOSEM) 20(4), 14 (2011)
Bose, A., Hu, X., Shin, K.G., Park, T.: Behavioral detection of malware on mobile handsets. In: Proc. 6th Int. Conf. Mobile Systems, Applications, and Services (MobiSys), pp. 225–238. ACM (2008)
Chen, F., Roşu, G.: Java-MOP: A Monitoring Oriented Programming Environment for Java. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 546–550. Springer, Heidelberg (2005)
Enck, W., Gilbert, P., Chun, B.-G., Cox, L.P., Jung, J., McDaniel, P., Sheth, A.N.: TaintDroid: an information-flow tracking system for realtime privacy monitoring on smartphones. In: Proc. 9th USENIX Symp. on OS Design and Implementation (OSDI). USENIX (2010)
Felt, A.P., Chin, E., Hanna, S., Song, D., Wagner, D.: Android permissions demystified. In: Proc. 18th ACM Conf. Comp. and Comm. Security (CCS), pp. 627–638. ACM (2011)
Felt, A.P., Greenwood, K., Wagner, D.: The effectiveness of application permissions. In: Proc. 2nd USENIX Conf. on Web Application Development, pp. 7–19. USENIX (2011)
Goldberg, A., Havelund, K., Mcgann, C.: Runtime verification for autonomous spacecraft software. In: IEEE 2005 Aerospace Conference (IEEEAC), pp. 507–516. IEEE (2005)
Google Inc., Android development site, http://developer.android.com/
Google Inc., http://developer.android.com/guide/topics/security/security.html
Jacob, G., Debar, H., Filiol, E.: Behavioral detection of malware: from a survey towards an established taxonomy. Journal in Computer Virology 4(3), 251–266 (2008)
Leyden, J.: First SMS Trojan for Android is in the wild. Web site, The Register (August 2010)
Ongtang, M., McLaughlin, S., Enck, W., McDaniel, P.: Semantically rich application-centric security in Android. In: Proc. Annual Comp. Sec. Applications Conference (ACSAC), pp. 340–349. IEEE (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bauer, A., Küster, JC., Vegliach, G. (2012). Runtime Verification Meets Android Security. In: Goodloe, A.E., Person, S. (eds) NASA Formal Methods. NFM 2012. Lecture Notes in Computer Science, vol 7226. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28891-3_18
Download citation
DOI: https://doi.org/10.1007/978-3-642-28891-3_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-28890-6
Online ISBN: 978-3-642-28891-3
eBook Packages: Computer ScienceComputer Science (R0)