Abstract
The Android system is in widespread use currently, and Android apps play an important role in our daily life. How to specify and verify apps is a challenging problem. In this paper, we study a formalism for abstracting the behaviour of Android apps, called Activity Transition Systems (ATS), which includes back transitions, value assignments and assertions. Given such a transition system with a corresponding Activity Transition Graph (ATG), it is interesting to know whether it violates some value assertions. We first prove some theoretical properties of transitions and propose a state-merging strategy. Then we further introduce a post-reachability graph technique. Based on this technique, we design an algorithm to traverse an ATG that avoids path cycles. Lastly, we also extend our model and our algorithm to handle more complicated problems.
This work is partially supported by the National Key Basic Research (973) Program of China (Grant No.2014CB340701), the National Natural Science Foundation of China (Grant No. 61672505), and the Key Research Program of Frontier Sciences, CAS (Grant No. QYZDJ-SSW-JSC036).
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
References
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 of ASE, pp. 258–261 (2012)
Amalfitano, D., Fasolino, A.R., Tramontana, P., Ta, B.D., Memon, A.M.: Mobiguitar: automated model-based testing of mobile apps. IEEE Softw. 32(5), 53–59 (2015)
Azim, T., Neamtiu, I.: Targeted and depth-first exploration for systematic testing of Android apps. In: Proceedings of of OOPSLA, pp. 641–660 (2013)
Baek, Y.M., Bae, D.: Automated model-based android GUI testing using multi-level GUI comparison criteria. In: Proceedings of of ASE, pp. 238–249 (2016)
Bhoraskar, R., et al.: Brahmastra: driving apps to test the security of third-party components. In: Proceedings of USENIX, pp. 1021–1036 (2014)
Chen, Q.A., Qian, Z., Mao, Z.M.: Peeking into your app without actually seeing it: UI state inference and novel android attacks. In: Proceedings of USENIX, pp. 1037–1052 (2014)
Chen, T., He, J., Song, F., Wang, G., Wu, Z., Yan, J.: Android stack machine. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 487–504. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-96142-2_29
Choi, W., Necula, G.C., Sen, K.: Guided GUI testing of android apps with minimal restart and approximate learning. In: Proceedigns of OOPSLA, pp. 623–640 (2013)
Do, L.N.Q., Ali, K., Livshits, B., Bodden, E., Smith, J., Murphy-Hill, E.R.: Just-in-time static analysis. In: Proceedings of SIGSOFT, pp. 307–317 (2017)
Feng, Y., Anand, S., Dillig, I., Aiken, A.: Apposcopy: semantics-based detection of android malware through static analysis. In: Proceedings of FSE, pp. 576–587 (2014)
Feng, Y., Bastani, O., Martins, R., Dillig, I., Anand, S.: Automated synthesis of semantic malware signatures using maximum satisfiability. In: Proceedings of NDSS (2017)
Gordon, M.I., Kim, D., Perkins, J.H., Gilham, L., Nguyen, N., Rinard, M.C.: Information flow analysis of android applications in DroidSafe. In: Proceedings of NDSS (2015)
Huang, W., Dong, Y., Milanova, A., Dolby, J.: Scalable and precise taint analysis for android. In: Proceedings of ISSTA, pp. 106–117 (2015)
Li, L., et al.: IccTA: detecting inter-component privacy leaks in android apps. In: Proceedings of ICSE, pp. 280–291 (2015)
Lu, L., Li, Z., Wu, Z., Lee, W., Jiang, G.: CHEX: statically vetting android apps for component hijacking vulnerabilities. In: Proceedings of CCS, pp. 229–240 (2012)
Mahmood, R., Mirzaei, N., Malek, S.: Evodroid: segmented evolutionary testing of android apps. In: Proceedings of FSE, pp. 599–609 (2014)
Mirzaei, N., Garcia, J., Bagheri, H., Sadeghi, A., Malek, S.: Reducing combinatorics in GUI testing of Android applications. In: Proceedings of ICSE, pp. 559–570 (2016)
Payet, E., Spoto, F.: An operational semantics for android activities. In: Proceedings of PEPM, pp. 121–132 (2014)
Shao, Y., Luo, X., Qian, C., Zhu, P., Zhang, L.: Towards a scalable resource-driven approach for detecting repackaged android applications. In: Proceedings of ACSAC, pp. 56–65 (2014)
Wei, F., Roy, S., Ou, X., Robby: Amandroid: a precise and general inter-component data flow analysis framework for security vetting of android apps. In: Proceedings of SIGSAC, pp. 1329–1341 (2014)
Yan, J., Wu, T., Yan, J., Zhang, J.: Widget-sensitive and back-stack-aware GUI exploration for testing android apps. In: Proceedings of QRS, pp. 42–53 (2017)
Yang, S., Yan, D., Wu, H., Wang, Y., Rountev, A.: Static control-flow analysis of user-driven callbacks in android applications. In: Proceedings of ICSE, pp. 89–99 (2015)
Yang, S., Zhang, H., Wu, H., Wang, Y., Yan, D., Rountev, A.: Static window transition graphs for Android(T). In: Proceedings of ASE, pp. 658–668 (2015)
Zhang, Y., Sui, Y., Xue, J.: Launch-mode-aware context-sensitive activity transition analysis. In: ICSE (2018, accepted)
Acknowledgements
The authors are grateful to the reviewers for helpful comments and suggestions, and to Ping Wang for reading a preliminary version of this paper carefully.
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Ge, C., Yan, J., Yan, J., Zhang, J. (2018). Checking Activity Transition Systems with Back Transitions Against Assertions. In: Sun, J., Sun, M. (eds) Formal Methods and Software Engineering. ICFEM 2018. Lecture Notes in Computer Science(), vol 11232. Springer, Cham. https://doi.org/10.1007/978-3-030-02450-5_23
Download citation
DOI: https://doi.org/10.1007/978-3-030-02450-5_23
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-02449-9
Online ISBN: 978-3-030-02450-5
eBook Packages: Computer ScienceComputer Science (R0)