Skip to main content
SpringerLink
Log in
Book cover

International Conference on Computational Science and Its Applications

ICCSA 2017: Computational Science and Its Applications – ICCSA 2017 pp 218–232Cite as

Separation Logic for States Dependencies in Life Cycles of Android Activities and Fragments

  • Conference paper
  • First Online:

  • 2307 Accesses

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10409))

Abstract

Millions of smart phones are run by Android, the most common operating system for mobile devices. Main component of Android is applications providing most functionalities of Android smart devices. These applications include e-mail client, entertainment, educational, news, banking, maps, and contacts applications. Testing and verifying Android applications is an important direction of research.

This paper presents a separation logic for state transitions of activities and fragments (important components of applications) during their life cycles. The logic considers the necessary coordinations between the state transitions in the two life cycles. The logic is a good tool to verify and test applications against various issues including security ones.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

References

  1. Android developers. http://developer.android.com

  2. 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(6), 259–269 (2014)

    Article  Google Scholar 

  3. Barrera, D., Kayacik, H.G., van Oorschot, P.C., Somayaji, A.: A methodology for empirical analysis of permission-based security models and its application to android. In: Proceedings of the 17th ACM Conference on Computer and Communications Security, pp. 73–84. ACM (2010)

    Google Scholar 

  4. Bartel, A., Klein, J., Le Traon, Y., Monperrus, M.: Dexpler: converting android dalvik bytecode to jimple for static analysis with soot. In: Proceedings of the ACM SIGPLAN International Workshop on State of the Art in Java Program Analysis, pp. 27–38. ACM (2012)

    Google Scholar 

  5. El-Zawawy, M.A.: An operational semantics for android applications. In: Gervasi, O., et al. (eds.) ICCSA 2016. LNCS, vol. 9790, pp. 100–114. Springer, Cham (2016). doi:10.1007/978-3-319-42092-9_9

    Chapter  Google Scholar 

  6. El-Zawawy, M.A.: A type system for android applications. In: Gervasi, O., et al. (eds.) ICCSA 2016. LNCS, vol. 9790, pp. 115–128. Springer, Cham (2016). doi:10.1007/978-3-319-42092-9_10

    Chapter  Google Scholar 

  7. Enck, W., Gilbert, P., Han, S., Tendulkar, V., 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. ACM Trans. Comput. Syst. (TOCS) 32(2), 5 (2014)

    Article  Google Scholar 

  8. Enck, W., Octeau, D., McDaniel, P., Chaudhuri, S.: A study of android application security. In: USENIX security symposium, vol. 2, p. 2 (2011)

    Google Scholar 

  9. Enck, W., Ongtang, M., McDaniel, P.: Understanding android security. IEEE Secur. Priv. 7(1), 50–57 (2009)

    Article  Google Scholar 

  10. Felt, A.P., Chin, E., Hanna, S., Song, D., Wagner, D.: Android permissions demystified. In: Proceedings of the 18th ACM Conference on Computer and Communications Security, pp. 627–638. ACM (2011)

    Google Scholar 

  11. Gunadi, H., Tiu, A.: Efficient runtime monitoring with metric temporal logic: a case study in the android operating system. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 296–311. Springer, Cham (2014). doi:10.1007/978-3-319-06410-9_21

    Chapter  Google Scholar 

  12. Huisman, M., Jacobs, B.: Java program verification via a hoare logic with abrupt termination. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol. 1783, pp. 284–303. Springer, Heidelberg (2000). doi:10.1007/3-540-46428-X_20

    Chapter  Google Scholar 

  13. Jeon, J., Micinski, K.K., Foster, J.S.: Symbolic execution for dalvik bytecode. Technical report, Symdroid (2012)

    Google Scholar 

  14. Mirzaei, N., Malek, S., Păsăreanu, C.S., Esfahani, N., Mahmood, R.: Testing android apps through symbolic execution. ACM SIGSOFT Softw. Eng. Notes 37(6), 1–5 (2012)

    Article  Google Scholar 

  15. Payet, E., Spoto, F.: An operational semantics for android activities. In: Proceedings of the ACM SIGPLAN 2014 Workshop on Partial Evaluation and Program Manipulation, pp. 121–132. ACM (2014)

    Google Scholar 

  16. Poetzsch-Heffter, A., Müller, P.: A programming logic for sequential Java. In: Swierstra, S.D. (ed.) ESOP 1999. LNCS, vol. 1576, pp. 162–176. Springer, Heidelberg (1999). doi:10.1007/3-540-49099-X_11

    Chapter  Google Scholar 

  17. Quigley, C.L.: A programming logic for java bytecode programs. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 41–54. Springer, Heidelberg (2003). doi:10.1007/10930755_3

    Chapter  Google Scholar 

  18. Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: 2002 Proceedings of 17th Annual IEEE Symposium on Logic in Computer Science, pp. 55–74. IEEE (2002)

    Google Scholar 

  19. Schreckling, D., Köstler, J., Schaff, M.: Kynoid: real-time enforcement of fine-grained, user-defined, and data-centric security policies for android. Inf. Secur. Tech. Rep. 17(3), 71–80 (2013)

    Article  Google Scholar 

  20. Yan, L.-K., Yin, H.: Droidscope: seamlessly reconstructing the OS and dalvik semantic views for dynamic android malware analysis. In: USENIX Security Symposium, pp. 569–584 (2012)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. College of Computer and Information Sciences, Al Imam Mohammad Ibn Saud Islamic University (IMSIU), Riyadh, Kingdom of Saudi Arabia

    Mohamed A. El-Zawawy

  2. Department of Mathematics, Faculty of Science, Cairo University, Giza, 12613, Egypt

    Mohamed A. El-Zawawy

Authors
  1. Mohamed A. El-Zawawy
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Mohamed A. El-Zawawy .

Editor information

Editors and Affiliations

  1. University of Perugia, Perugia, Italy

    Osvaldo Gervasi

  2. University of Basilicata, Potenza, Italy

    Beniamino Murgante

  3. Covenant University, Ota, Nigeria

    Sanjay Misra

  4. University of Trieste, Trieste, Italy

    Giuseppe Borruso

  5. Polytechnic University of Bari, Bari, Italy

    Carmelo M. Torre

  6. University of Minho, Braga, Portugal

    Ana Maria A.C. Rocha

  7. Monash University, Clayton, Victoria, Australia

    David Taniar

  8. Kyushu Sangyo University, Fukuoka, Japan

    Bernady O. Apduhan

  9. Saint Petersburg State University, Saint Petersburg, Russia

    Elena Stankova

  10. University of Trieste, Trieste, Italy

    Alfredo Cuzzocrea

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

El-Zawawy, M.A. (2017). Separation Logic for States Dependencies in Life Cycles of Android Activities and Fragments. In: Gervasi, O., et al. Computational Science and Its Applications – ICCSA 2017. ICCSA 2017. Lecture Notes in Computer Science(), vol 10409. Springer, Cham. https://doi.org/10.1007/978-3-319-62407-5_15

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-62407-5_15

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-62406-8

  • Online ISBN: 978-3-319-62407-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation