Skip to main content
SpringerLink
Log in

Verifying Policy Enforcers

  • Conference paper
  • First Online:
Book cover Runtime Verification (RV 2017)

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

Included in the following conference series:

Abstract

Policy enforcers are sophisticated runtime components that can prevent failures by enforcing the correct behavior of the software. While a single enforcer can be easily designed focusing only on the behavior of the application that must be monitored, the effect of multiple enforcers that enforce different policies might be hard to predict. So far, mechanisms to resolve interferences between enforcers have been based on priority mechanisms and heuristics. Although these methods provide a mechanism to take decisions when multiple enforcers try to affect the execution at a same time, they do not guarantee the lack of interference on the global behavior of the system.

In this paper we present a verification strategy that can be exploited to discover interferences between sets of enforcers and thus safely identify a-priori the enforcers that can co-exist at run-time. In our evaluation, we experimented our verification method with several policy enforcers for Android and discovered some incompatibilities.

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.

    Android apps are composed of multiple components called activities.

References

  1. Android: API Guides. https://developer.android.com/guide/index.html. Accessed 6 May 2017

  2. Android: MediaPlayer. https://developer.android.com/reference/android/media/MediaPlayer.html. Accessed 6 May 2017

  3. Android: Package Index. https://developer.android.com/reference/packages.html. Accessed 6 May 2017

  4. Android: The Activity Lifecycle. https://developer.android.com/guide/components/activities/activity-lifecycle.html. Accessed 6 May 2017

  5. Azim, M.T., Neamtiu, I., Marvel, L.M.: Towards self-healing smartphone software via automated patching. In: Proceedings of the International Conference on Automated Software Engineering (ASE) (2014)

    Google Scholar 

  6. Baier, C., Katoen, J.P., Larsen, K.G.: Principles of Model Checking. MIT Press, Cambridge (2008)

    MATH  Google Scholar 

  7. Banerjee, A., Chong, L.K., Chattopadhyay, S., Roychoudhury, A.: Detecting energy bugs and hotspots in mobile apps. In: Proceedings of the ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE) (2014)

    Google Scholar 

  8. Bauer, A., Küster, J., Vegliach, G.: Runtime verification meets Android security. In: Proceedings of the International Symposium on Formal Methods (NFM) (2012)

    Google Scholar 

  9. Bauer, L., Ligatti, J., Walker, D.: Composing security policies with polymer. In: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) (2005)

    Google Scholar 

  10. Bengtsson, J., Larsen, K., Larsson, F., Pettersson, P., Yi, W.: UPPAAL — a tool suite for automatic verification of real-time systems. In: Alur, R., Henzinger, T.A., Sontag, E.D. (eds.) HS 1995. LNCS, vol. 1066, pp. 232–243. Springer, Heidelberg (1996). doi:10.1007/BFb0020949

    Chapter  Google Scholar 

  11. Bielova, N., Massacci, F.: Do you really mean what you actually enforced? edited automata revisited. Int. J. Inform. Secur. (IJIS) 10(4), 239–254 (2011)

    Article  Google Scholar 

  12. Chircop, L., Colombo, C., Pace, G.J.: Device-centric monitoring for mobile device management. In: Proceedings of the International Workshop on Formal Engineering approaches to Software Components and Architectures (FESCA) (2016)

    Google Scholar 

  13. Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. (TOPLAS) 8(2), 244–263 (1986)

    Article  MATH  Google Scholar 

  14. 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). doi:10.1007/978-3-642-10665-1_5

    Chapter  Google Scholar 

  15. Daian, P., Falcone, Y., Meredith, P., Şerbănuţă, T.F., Shiriashi, S., Iwai, A., Rosu, G.: 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). doi:10.1007/978-3-319-23820-3_24

    Chapter  Google Scholar 

  16. Falcone, Y., Currea, S., Jaber, M.: Runtime verification and enforcement for Android applications with RV-Droid. In: Proceedings of the International Conference on Runtime Verification (RV) (2012)

    Google Scholar 

  17. Falcone, Y., Fernandez, J.C., Mounier, L.: What can you verify and enforce at runtime? Int. J. Softw. Tools Technol. Transfer 14(3), 349–382 (2012)

    Article  Google Scholar 

  18. Falcone, Y., Jéron, T., Marchand, H., Pinisetty, S.: Runtime enforcement of regular timed properties by suppressing and delaying events. Syst. Control Lett. 123, 2–41 (2016)

    Google Scholar 

  19. 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  MATH  Google Scholar 

  20. Guo, C., Zhang, J., Yan, J., Zhang, Z., Zhang, Y.: Characterizing and detecting resource leaks in android applications. In: Proceedings of the International Conference on Automated Software Engineering (ASE) (2013)

    Google Scholar 

  21. Hoare, C.A.R.: Communicating sequential processes. In: Hansen, P.B. (ed.) The Origin of Concurrent Programming, pp. 413–443. Springer, New York (1978)

    Chapter  Google Scholar 

  22. Hyrynsalmi, S., Suominen, A., Mäkilä, T., Knuutila, T.: Mobile application ecosystems: an analysis of android ecosystem. In: Encyclopedia of E-Commerce Development, Implementation, and Management, chap. 100, vol. II, pp. 1418–1434. IGI Global (2016)

    Google Scholar 

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

    Article  MATH  Google Scholar 

  24. Küster, J., Bauer, A.: Monitoring real android malware. In: Proceedings of the International Conference on Runtime Verification (RV) (2015)

    Google Scholar 

  25. Li, L., Bissyandé, T.F., Octeau, D., Klein, J.: DroidRA: taming reflection to support whole-program analysis of android apps. In: Proceedings of the International Symposium on Software Testing and Analysis (ISSTA) (2016)

    Google Scholar 

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

    Article  Google Scholar 

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

    Google Scholar 

  28. Lynch, N.A., Tuttle, M.R.: An introduction to input/output automata. CWI Q. 2(3), 219–246 (1988)

    MathSciNet  MATH  Google Scholar 

  29. Magalhães, J.P., Silva, L.M.: SHÕWA: a self-healing framework for web-based applications. ACM Trans. Auton. Adapt. Syst. 10(1), 4:1–4:28 (2015)

    Google Scholar 

  30. Pinisetty, S., Falcone, Y., Jéron, T., Marchand, H., Rollet, A., Nguena-Timo, O.: Runtime enforcement of timed properties revisited. Formal Methods Syst. Des. 45(3), 381–422 (2014). https://doi.org/10.1007/s10703-014-0215-y

    Article  MATH  Google Scholar 

  31. 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 

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

    Google Scholar 

  33. Schneider, F.B.: Enforceable security policies. ACM Trans. Inform. Syst. Secur. (TISSEC) 3(1), 30–50 (2000)

    Article  MathSciNet  Google Scholar 

  34. Shan, Z., Azim, T., Neamtiu, I.: Finding resume and restart errors in android applications. In: Proceedings of the ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA) (2016)

    Google Scholar 

  35. 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 

  36. Wei, L., Liu, Y., Cheung, S.C.: Taming android fragmentation: characterizing and detecting compatibility issues for android apps. In: Proceedings of the IEEE/ACM International Conference on Automated Software Engineering (ASE) (2016)

    Google Scholar 

  37. Wu, T., Liu, J., Xu, Z., Guo, C., Zhang, Y., Yan, J., Zhang, J.: Light-weight, inter-procedural and callback-aware resource leak detection for android apps. IEEE Trans. Softw. Eng. (TSE) 42(11), 1054–1076 (2016)

    Article  Google Scholar 

Download references

Acknowledgment

This work has been partially supported by the H2020 Learn project, which has been funded under the ERC Consolidator Grant 2014 program (ERC Grant Agreement n. 646867), the GAUSS national research project, which has been funded by the MIUR under the PRIN 2015 program (Contract 2015KWREMX), and the COST Action ARVI IC1402, supported by COST (European Cooperation in Science and Technology).

Author information

Authors and Affiliations

  1. University of Milano Bicocca, Viale Sarca 336, 20126, Milan, Italy

    Oliviero Riganelli, Daniela Micucci & Leonardo Mariani

  2. Univ. Grenoble Alpes, CNRS, Inria, Grenoble INP, LIG, 38000, Grenoble, France

    Yliès Falcone

Authors
  1. Oliviero Riganelli
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Daniela Micucci
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Leonardo Mariani
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Yliès Falcone
    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. Microsoft Research, Redmond, Washington, USA

    Shuvendu Lahiri

  2. The University of Manchester, Manchester, United Kingdom

    Giles Reger

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Riganelli, O., Micucci, D., Mariani, L., Falcone, Y. (2017). Verifying Policy Enforcers. In: Lahiri, S., Reger, G. (eds) Runtime Verification. RV 2017. Lecture Notes in Computer Science(), vol 10548. Springer, Cham. https://doi.org/10.1007/978-3-319-67531-2_15

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-67531-2_15

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-67530-5

  • Online ISBN: 978-3-319-67531-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation