Abstract
The most common form of computers today is the hand held form and specially smart phones and tablets. The platform for the majority of smart phones is the Android operating system. Therefore analyzing and verifying the Android applications become an issue of extreme importance. However classical techniques of static analysis are not applicable directly to Android applications. This is so because typically Android applications are developed using Java code that is translated into Java bytecode and executed using Dalvik virtual machine. Also developing new techniques for static analysis of Android applications is an involved problem due to many facts such as the concept of gestures used in Android interaction with users.
One of the main tools of analyzing and verifying programs is types systems [11]. This paper presents a new type system, Android\(\mathcal {T}\), which is specific to Android applications. The proposed type system ensures the absence of errors like “method is undefined”. Also the type system is applicable to check the soundness of static analyses of Android applications.
Keywords
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
Dalvik bytecode. https://source.android.com/devices/tech/dalvik/dalvik-bytecode.html. Accessed 1 Feb 2016
Dalvik docs mirror. http://www.statista.com/topics/840/smartphones/. Accessed Feb 2016
Dalvik docs mirror. http://www.milk.com/kodebase/dalvik-docs-mirror/. Accessed Feb 2016
Gartner, Inc.: Worldwide Traditional PC, Tablet, Ultramobile and Mobile Phoneshipments. www.gartner.com/newsroom/id/2692318
Amalfitano, D., Fasolino, A.R., Tramontana, P., De Carmine, S., Memon, A.M.: Using GUI ripping for automated testing of android applications. In: Proceedings of 27th IEEE/ACM International Conference on Automated Software Engineering, pp. 258–261. ACM (2012)
Bugliesi, M., Calzavara, S., Spanò, A.: Lintent: towards security type-checking of android applications. In: Beyer, D., Boreale, M. (eds.) FORTE 2013 and FMOODS 2013. LNCS, vol. 7892, pp. 289–304. Springer, Heidelberg (2013)
Cardelli, L.: Type systems. ACM Comput. Surv. 28(1), 263–264 (1996)
Costa, G.: Securing Android with local policies. In: Bodei, C., Ferrari, G.-L., Priami, C. (eds.) Programming Languages with Applications to Biology and Security: Essays Dedicated to Pierpaolo Degano on the Occasion of His 65th Birthday. LNCS, vol. 9465, pp. 202–218. Springer, Heidelberg (2015). doi:10.1007/978-3-319-25527-9_14
Cousot, P.: Semantic foundations of program analysis. In: Muchnick, S., Jones, N. (eds.) Program Flow Analysis : Theory and Applications. Prentice Hall, Englewood Cliffs (1981)
El-Zawawy, M.A.: An operational semantics for Android applications. In: Computational Science and Its Applications-ICCSA (2016)
El-Zawawy, M.A.: Heap slicing using type systems. In: Murgante, B., Gervasi, O., Misra, S., Nedjah, N., Rocha, A.M.A.C., Taniar, D., Apduhan, B.O. (eds.) ICCSA 2012, Part III. LNCS, vol. 7335, pp. 592–606. Springer, Heidelberg (2012)
El-Zawawy, M.A.: Recognition of logically related regions based heap abstraction. J. Egypt. Math. Soci. 20(2), 64–71 (2012)
Gunadi, H.: Formal certification of non-interferent Android bytecode (DEX bytecode). In: 2015 20th International Conference on Engineering of Complex Computer Systems (ICECCS), pp. 202–205. IEEE (2015)
Karlsen, H.S., Wognsen, E.R.: Static analysis of Dalvik bytecode and reflection in Android. Master’s thesis, Aalborg University, June 2012
Cuixiong, H., Neamtiu, I.: Automating gui testing for Android applications. In: Proceedings of 6th International Workshop on Automation of Software Test, pp. 77–83. ACM (2011)
Huang, W., Dong, Y., Milanova, A., Dolby, J.: Scalable and precise taint analysis for Android. In: Proceedings of 2015 International Symposium on Software Testing and Analysis, pp. 106–117. ACM (2015)
Just, R., Ernst, M.D., Millstein, S.: Collaborative verification of information flow for a high-assurance app store. Softw. Eng. Manag. 77 (2015)
Machiry, A., Tahiliani, R., Naik, M.: Dynodroid: an input generation system for Android apps. In: Proceedings of 2013 9th Joint Meeting on Foundations of Software Engineering, pp. 224–234. ACM (2013)
Mann, C., Starostin, A.: A framework for static detection of privacy leaks in android applications. In: Proceedings of 27th Annual ACM Symposium on Applied Computing, pp. 1457–1462. ACM (2012)
Mednieks, Z., Dornin, L., Meike, G.B., Nakamura, M.: Programming Android. O’Reilly Media Inc, Sebastopol (2012)
Micinski, K., Fetter-Degges, J., Jeon, J., Foster, J.S., Clarkson, M.R.: Checking interaction-based declassification policies for Android using symbolic execution. In: Pernul, G., Ryan, P.Y.A., Weippl, E. (eds.) ESORICS 2015. LNCS, vol. 9327, pp. 520–538. Springer, Heidelberg (2015). doi:10.1007/978-3-319-24177-7_26
Milette, G., Stroud, A.: Professional Android Sensor Programming. Wiley, New York (2012)
Mohr, M., Graf, J., Hecker, M.: JoDroid: adding android support to a static information flow control tool. In: Software Engineering (Workshops), pp. 140–145 (2015)
Newcomer, K.E., Hatry, H.P., Wholey, J.S.: Handbook of Practical Program Evaluation. Wiley, New York (2015)
Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (2015)
Octeau, D., Jha, S., McDaniel, P.: Retargeting Android applications to Java bytecode. In: Proceedings of ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering, p. 6. ACM (2012)
Payet, É., Spoto, F.: An operational semantics for android activities. In: Chin, W.-N., Hage, J. (eds.) Proceedings of ACM SIGPLAN 2014 Workshop on Partial Evaluation and Program Manipulation, PEPM, San Diego, California, USA, pp. 121–132. ACM, 20–21 January 2014
Reddy, N., Jeon, J., Vaughan, J., Millstein, T., Foster, J.: Application-centric security policies on unmodified Android. UCLA Computer Science Department, Technical report 110017 (2011)
Rogers, R., Lombardo, J., Mednieks, Z., Meike, B.: Android Application Development: Programming with the Google SDK. O’Reilly Media Inc., Sebastopol (2009)
Schwartzbach, M.I., Palsberg, J.: Object-Oriented Type Systems. Wiley, New York (1994)
Wegbreit, B.: Mechanical program analysis. Commun. ACM 18(9), 528–539 (1975)
Rubin, X., Saïdi, H., Anderson, R.: Aurasium: practical policy enforcement for android applications. Paper presented at the Part of 21st USENIX Security Symposium (USENIX Security 12), pp. 539–552 (2012)
Yang, S.: Static analyses of GUI behavior in Android applications. Ph.D. thesis, The Ohio State University (2015)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
El-Zawawy, M.A. (2016). A Type System for Android Applications. In: Gervasi, O., et al. Computational Science and Its Applications – ICCSA 2016. ICCSA 2016. Lecture Notes in Computer Science(), vol 9790. Springer, Cham. https://doi.org/10.1007/978-3-319-42092-9_10
Download citation
DOI: https://doi.org/10.1007/978-3-319-42092-9_10
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-42091-2
Online ISBN: 978-3-319-42092-9
eBook Packages: Computer ScienceComputer Science (R0)