Skip to main content
SpringerLink
Log in

Test4Enforcers: Test Case Generation for Software Enforcers

  • Conference paper
  • First Online:
Runtime Verification (RV 2020)

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

Included in the following conference series:

Abstract

Software enforcers can be used to modify the runtime behavior of software applications to guarantee that relevant correctness policies are satisfied. Indeed, the implementation of software enforcers can be tricky, due to the heterogeneity of the situations that they must be able to handle. Assessing their ability to steer the behavior of the target system without introducing any side effect is an important challenge to fully trust the resulting system. To address this challenge, this paper presents Test4Enforcers, the first approach to derive thorough test suites that can validate the impact of enforcers on a target system. The paper also shows how to implement the Test4Enforcers approach in the DroidBot test generator to validate enforcers for Android apps.

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

Access this chapter

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

Institutional subscriptions

Notes

  1. 1.

    Activities are fundamental components of Android apps and they represent the entry point for a user’s interaction with the app https://developer.android.com/guide/components/activities.

  2. 2.

    onPause() is a callback method that is invoked by the Android framework when an activity is paused.

  3. 3.

    https://play.google.com/store/apps/details?id=net.phunehehe.foocam2&hl=EN.

References

  1. Android Docs: Camera API (2020). https://developer.android.com/guide/topics/media/camera

  2. Belli, F., Beyazıt, M., Endo, A.T., Mathur, A., Simao, A.: Fault domain-based testing in imperfect situations: a heuristic approach and case studies. Softw. Qual. J. 23(3), 423–452 (2014). https://doi.org/10.1007/s11219-014-9242-6

    Article  Google Scholar 

  3. Bielova, N., Massacci, F.: Do you really mean what you actually enforced? Int. J. Inf. Secur. 10, 239–254 (2011)

    Article  Google Scholar 

  4. Chow, T.S.: Testing software design modeled by finite-state machines. IEEE Trans. Softw. Eng. 3, 178–187 (1978)

    Article  Google Scholar 

  5. Dai, Y., Xiang, Y., Zhang, G.: Self-healing and hybrid diagnosis in cloud computing. In: Jaatun, M.G., Zhao, G., Rong, C. (eds.) CloudCom 2009. LNCS, vol. 5931, pp. 45–56. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-10665-1_5

    Chapter  Google Scholar 

  6. Daian, P., et al.: RV-Android: efficient parametric android runtime verification, a brief tutorial. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 342–357. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-23820-3_24

    Chapter  Google Scholar 

  7. Dalal, S.R., et al.: Model-based testing in practice. In: Proceedings of the International Conference on Software Engineering (ICSE) (1999)

    Google Scholar 

  8. Dias Neto, A.C., Subramanyan, R., Vieira, M., Travassos, G.H.: A survey on model-based testing approaches: a systematic review. In: Proceedings of the ACM International Workshop on Empirical Assessment of Software Engineering Languages and Technologies (WEASELTech) (2007)

    Google Scholar 

  9. Dolzhenko, E., Ligatti, J., Reddy, S.: Modeling runtime enforcement with mandatory results automata. Int. J. Inf. Secur. 14(1), 47–60 (2014). https://doi.org/10.1007/s10207-014-0239-8

    Article  Google Scholar 

  10. Dorofeeva, R., El-Fakih, K., Maag, S., Cavalli, A.R., Yevtushenko, N.: FSM-based conformance testing methods: a survey annotated with experimental evaluation. Inf. Softw. Technol. 52(12), 1286–1297 (2010)

    Article  Google Scholar 

  11. Dorofeeva, R., El-Fakih, K., Yevtushenko, N.: An improved conformance testing method. In: Wang, F. (ed.) FORTE 2005. LNCS, vol. 3731, pp. 204–218. Springer, Heidelberg (2005). https://doi.org/10.1007/11562436_16

    Chapter  Google Scholar 

  12. Falcone, Y., Currea, S., Jaber, M.: Runtime verification and enforcement for android applications with RV-Droid. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol. 7687, pp. 88–95. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-35632-2_11

    Chapter  Google Scholar 

  13. Falcone, Y., Pinisetty, S.: On the runtime enforcement of timed properties. In: Finkbeiner, B., Mariani, L. (eds.) RV 2019. LNCS, vol. 11757, pp. 48–69. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-32079-9_4

    Chapter  Google Scholar 

  14. Falcone, Y.: You should better enforce than verify. In: Barringer, H., et al. (eds.) RV 2010. LNCS, vol. 6418, pp. 89–105. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16612-9_9

    Chapter  Google Scholar 

  15. Falcone, Y., Mariani, L., Rollet, A., Saha, S.: Runtime failure prevention and reaction. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification. LNCS, vol. 10457, pp. 103–134. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-75632-5_4

    Chapter  Google Scholar 

  16. Falcone, Y., Mounier, L., Fernandez, J.C., Richier, J.L.: Runtime enforcement monitors: composition, synthesis, and enforcement abilities. Formal Methods Syst. Des. 38(3), 223–262 (2011)

    Article  Google Scholar 

  17. Fujiwara, S., von Bochmann, G., Khendek, F., Amalou, M., Ghedamsi, A.: Test selection based on finite state models. IEEE Trans. Softw. Eng. 17(6), 591–603 (1991)

    Article  Google Scholar 

  18. Gonenc, G.: A method for the design of fault detection experiments. IEEE Trans. Comput. C–19(6), 551–558 (1970)

    Article  Google Scholar 

  19. Gurbuz, H.G., Tekinerdogan, B.: Model-based testing for software safety: a systematic mapping study. Softw. Qual. J. 26(4), 1327–1372 (2017). https://doi.org/10.1007/s11219-017-9386-2

    Article  Google Scholar 

  20. Hierons, R.M., Turker, U.C.: Parallel algorithms for generating harmonised state identifiers and characterising sets. IEEE Trans. Comput. 65(11), 3370–3383 (2016)

    Article  MathSciNet  Google Scholar 

  21. Khoury, R., Tawbi, N.: Corrective enforcement: a new paradigm of security policy enforcement by monitors. ACM Trans. Inf. Syst. Secur. 15(2), 1–27 (2012)

    Article  Google Scholar 

  22. Khoury, R., Tawbi, N.: Which security policies are enforceable by runtime monitors? A survey. Comput. Sci. Rev. 6(1), 27–45 (2012)

    Article  Google Scholar 

  23. Lee, D., Yannakakis, M.: Principles and methods of testing finite state machines-a survey. Proc. IEEE 84(8), 1090–1123 (1996)

    Article  Google Scholar 

  24. Li, Y., Ziyue, Y., Yao, G., Xiangqun, C.: DroidBot: a lightweight UI-guided test input generator for android. In: Proceedings of the International Conference on Software Engineering Companion (ICSE) (2017)

    Google Scholar 

  25. Ligatti, J., Bauer, L., Walker, D.: Run-time enforcement of nonsafety policies. ACM Trans. Inf. Syst. Secur. 12(3), 1–41 (2009)

    Article  Google Scholar 

  26. Ligatti, J., Bauer, L., Walker, D.: Edit automata: enforcement mechanisms for run-time security policies. Int. J. Inf. Secur. 4, 2–16 (2005)

    Article  Google Scholar 

  27. Ligatti, J., Reddy, S.: A theory of runtime enforcement, with results. In: Gritzalis, D., Preneel, B., Theoharidou, M. (eds.) ESORICS 2010. LNCS, vol. 6345, pp. 87–100. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15497-3_6

    Chapter  Google Scholar 

  28. Luo, G., Petrenko, A., Bochmann, G.V.: Selecting test sequences for partially-specified nondeterministic finite state machines. In: Mizuno, T., Higashino, T., Shiratori, N. (eds.) Protocol Test Systems. ITIFIP, pp. 95–110. Springer, Boston, MA (1995). https://doi.org/10.1007/978-0-387-34883-4_6

    Chapter  Google Scholar 

  29. Lynch, N.A.: An introduction to input/output automata. PN (1988)

    Google Scholar 

  30. Magalhães, J.A.P., Silva, L.M.: Shõwa: a self-healing framework for web-based applications. ACM Trans. Autonom. Adapt. Syst. 10(1), 4:1–4:28 (2015)

    Google Scholar 

  31. Memon, A.M., Banerjee, I., Nguyen, B.N., Robbins, B.: The first decade of GUI ripping: extensions, applications, and broader impacts. In: Proceedings of the Working Conference on Reverse Engineering (WCRE) (2013)

    Google Scholar 

  32. Petrenko, A., Yevtushenko, N., v. Bochmann, G.: Testing deterministic implementations from nondeterministic FSM specifications. In: Baumgarten, B., Burkhardt, H.-J., Giessler, A. (eds.) Testing of Communicating Systems. ITIFIP, pp. 125–140. Springer, Boston, MA (1996). https://doi.org/10.1007/978-0-387-35062-2_10

    Chapter  Google Scholar 

  33. Riganelli, O., Micucci, D., Mariani, L.: Healing data loss problems in android apps. In: Proceedings of the International Workshop on Software Faults (IWSF), Co-Located with the International Symposium on Software Reliability Engineering (ISSRE) (2016)

    Google Scholar 

  34. Riganelli, O., Micucci, D., Mariani, L.: Increasing the reusability of enforcers with lifecycle events. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11247, pp. 51–57. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-03427-6_7

    Chapter  Google Scholar 

  35. Riganelli, O., Micucci, D., Mariani, L.: Policy enforcement with proactive libraries. In: Proceedings of the IEEE/ACM International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS) (2017)

    Google Scholar 

  36. Riganelli, O., Micucci, D., Mariani, L.: Controlling interactions with libraries in android apps through runtime enforcement. ACM Trans. Autonom. Adapt. Syst. 14(2), 8:1–8:29 (2019)

    Google Scholar 

  37. Riganelli, O., Micucci, D., Mariani, L., Falcone, Y.: Verifying policy enforcers. In: Lahiri, S., Reger, G. (eds.) RV 2017. LNCS, vol. 10548, pp. 241–258. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-67531-2_15

    Chapter  Google Scholar 

  38. Sabnani, K., Dahbura, A.: A protocol test generation procedure. Comput. Netw. ISDN Syst. 15(4), 285–297 (1988)

    Article  Google Scholar 

  39. Sidhu, D.P., Leung, T.K.: Formal methods for protocol testing: a detailed study. IEEE Trans. Softw. Eng. 15(4), 413–426 (1989)

    Article  Google Scholar 

  40. Sidiroglou, S., Laadan, O., Perez, C., Viennot, N., Nieh, J., Keromytis, A.D.: ASSURE: automatic software self-healing using rescue points. In: Proceedings of the International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS) (2009)

    Google Scholar 

  41. Utting, M., Pretschner, A., Legeard, B.: A taxonomy of model-based testing approaches. Softw. Testing Verification Reliabil. 22(5), 297–312 (2012)

    Article  Google Scholar 

  42. XDA: Xposed (2020). http://repo.xposed.info/

  43. Xu, R., Saïdi, H., Anderson, R.: Aurasium: practical policy enforcement for android applications. In: Proceedings of the USENIX Conference on Security Symposium (Security) (2012)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Milano-Bicocca, 20126, Milan, Italy

    Michell Guzman, Oliviero Riganelli, Daniela Micucci & Leonardo Mariani

Authors
  1. Michell Guzman
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Oliviero Riganelli
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Daniela Micucci
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Leonardo Mariani
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Oliviero Riganelli .

Editor information

Editors and Affiliations

  1. University of Southern California, Los Angeles, CA, USA

    Jyotirmoy Deshmukh

  2. AIT Austrian Institute of Technology GmbH, Vienna, Austria

    Dejan Ničković

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Guzman, M., Riganelli, O., Micucci, D., Mariani, L. (2020). Test4Enforcers: Test Case Generation for Software Enforcers. In: Deshmukh, J., Ničković, D. (eds) Runtime Verification. RV 2020. Lecture Notes in Computer Science(), vol 12399. Springer, Cham. https://doi.org/10.1007/978-3-030-60508-7_15

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-60508-7_15

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-60507-0

  • Online ISBN: 978-3-030-60508-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation