Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Automated Verification of Critical Systems

International Workshop on Formal Methods for Industrial Critical Systems

AVoCS 2016, FMICS 2016: Critical Systems: Formal Methods and Automated Verification pp 142–149Cite as

Utilising \({\mathbb {K}}\) Semantics for Collusion Detection in Android Applications

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 9933))

Abstract

The Android OS supports multiple communication methods between apps. This opens the possibility to carry out threats in a collaborative fashion, c.f. the Soundcomber example from 2011. In this paper we demonstrate an effective attempt to detect collusion via model-checking a set of apps utilising the \({\mathbb {K}}\) framework.

This research has been partially supported by the ACID project.

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

Notes

  1. 1.

    http://www.cs.swan.ac.uk/~csmarkus/ProcessesAndData/androidsmali-semantics-k.

  2. 2.

    http://www.cs.swansea.ac.uk/~csmarkus/ProcessesAndData/sites/default/files/uploads/resources/code.zip.

  3. 3.

    We refrain to define what malicious behaviour might be and assume that the security community already has classified (sets of) apps to be malware. For example, our industrial partner Intel Security does so on a daily a basis for single apps.

  4. 4.

    All experiments are carried out on a Macbook Pro with an Intel i7 2.2 GHz quad-core processor and 16 GB of memory.

References

  1. Android Package Index (2016). http://developer.android.com/reference/packages.html

  2. Android Open Source Project. Dalvik Bytecode (2016). https://source.android.com/devices/tech/dalvik/dalvik-bytecode.html

  3. Asavoae, I.M., Blasco, J., Chen, T.M., Kalutarage, H.K., Muttik, I., Nguyen, H.N., Roggenbach, M., Shaikh, S.A.: Towards automated Android app collusion detection (2016). CoRR, abs/1603.02308

    Google Scholar 

  4. Blasco, J., Chen, T.M., Muttik, I., Roggenbach, M.: Wild android collusions. In: Virus Bulletin (2016, to appear)

    Google Scholar 

  5. Bogdănaş, D., Roşu, G.: K-Java: a complete semantics of Java. In: POPL 2015. ACM (2015)

    Google Scholar 

  6. Bugiel, S., Davi, L., Dmitrienko, A., Heuser, S., Sadeghi, A.-R., Shastry, B.: Practical and lightweight domain isolation on Android. In: SPSM 2011. ACM (2011)

    Google Scholar 

  7. Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C. (eds.): All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007)

    MATH  Google Scholar 

  8. Hathhorn, C., Ellison, C., Roşu, G.: Defining the undefinedness of c. In: PLDI 2015. ACM (2015)

    Google Scholar 

  9. Li, L., Bartel, A., Bissyandé, T.F., Klein, J., Traon, Y.L.: ApkCombiner: combining multiple android apps to support inter-app analysis. In: Federrath, H., Gollmann, D., Chakravarthy, S.R. (eds.) SEC 2015. IFIP AICT, vol. 455, pp. 513–527. Springer, Heidelberg (2015). doi:10.1007/978-3-319-18467-8_34

    Chapter  Google Scholar 

  10. Octeau, D., Luchaup, D., Dering, M., Jha, S., McDaniel, P.: Composite constant propagation: application to android inter-component communication analysis. In: ICSE 2015. IEEE Computer Society (2015)

    Google Scholar 

  11. Octeau, D., McDaniel, P., Jha, S., Bartel, A., Bodden, E., Klein, J., Traon, Y.L.: Effective inter-component communication mapping in android: an essential step towards holistic security analysis. In: Security Symposium. USENIX Association (2013)

    Google Scholar 

  12. Ravitch, T., Creswick, E.R., Tomb, A., Foltzer, A., Elliott, T., Casburn, L.: Multi-app security analysis with FUSE: statically detecting Android app collusion. In: ACSAC 2014. ACM (2014)

    Google Scholar 

  13. Roşu, G., Şerbănuţă, T.F.: An overview of the K semantic framework. J. Log. Algebr. Program. 79(6), 397–434 (2010)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Acknowledgement

The authors would like to thank our colleagues in ACID for the good cooperation in the project, and Erwin R. Catesbeiana Jr. for excellent guidance through the Android ecosystem.

Author information

Authors and Affiliations

  1. Swansea University, Swansea, UK

    Irina Măriuca Asăvoae & Markus Roggenbach

  2. Coventry University, Coventry, UK

    Hoang Nga Nguyen & Siraj Shaikh

Authors
  1. Irina Măriuca Asăvoae
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Hoang Nga Nguyen
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Markus Roggenbach
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Siraj Shaikh
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Markus Roggenbach .

Editor information

Editors and Affiliations

  1. ISTI-CNR , Pisa, Italy

    Maurice H. ter Beek

  2. ISTI-CNR , Pisa, Italy

    Stefania Gnesi

  3. Universität Augsburg, Augsburg, Germany

    Alexander Knapp

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing AG

About this paper

Cite this paper

Asăvoae, I.M., Nguyen, H.N., Roggenbach, M., Shaikh, S. (2016). Utilising \({\mathbb {K}}\) Semantics for Collusion Detection in Android Applications. In: ter Beek, M., Gnesi, S., Knapp, A. (eds) Critical Systems: Formal Methods and Automated Verification. AVoCS FMICS 2016 2016. Lecture Notes in Computer Science(), vol 9933. Springer, Cham. https://doi.org/10.1007/978-3-319-45943-1_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-45943-1_10

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-45942-4

  • Online ISBN: 978-3-319-45943-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation