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
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
Android apps are composed of multiple components called activities.
References
Android: API Guides. https://developer.android.com/guide/index.html. Accessed 6 May 2017
Android: MediaPlayer. https://developer.android.com/reference/android/media/MediaPlayer.html. Accessed 6 May 2017
Android: Package Index. https://developer.android.com/reference/packages.html. Accessed 6 May 2017
Android: The Activity Lifecycle. https://developer.android.com/guide/components/activities/activity-lifecycle.html. Accessed 6 May 2017
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)
Baier, C., Katoen, J.P., Larsen, K.G.: Principles of Model Checking. MIT Press, Cambridge (2008)
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)
Bauer, A., Küster, J., Vegliach, G.: Runtime verification meets Android security. In: Proceedings of the International Symposium on Formal Methods (NFM) (2012)
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)
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
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)
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)
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)
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
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
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)
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)
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)
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)
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)
Hoare, C.A.R.: Communicating sequential processes. In: Hansen, P.B. (ed.) The Origin of Concurrent Programming, pp. 413–443. Springer, New York (1978)
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)
Khoury, R., Tawbi, N.: Which security policies are enforceable by runtime monitors? a survey. Comput. Sci. Rev. 6(1), 27–45 (2012)
Küster, J., Bauer, A.: Monitoring real android malware. In: Proceedings of the International Conference on Runtime Verification (RV) (2015)
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)
Ligatti, J., Bauer, L., Walker, D.: Edit automata: enforcement mechanisms for run-time security policies. Int. J. Inform. Secur. 4(1), 2–16 (2005)
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)
Lynch, N.A., Tuttle, M.R.: An introduction to input/output automata. CWI Q. 2(3), 219–246 (1988)
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)
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
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)
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)
Schneider, F.B.: Enforceable security policies. ACM Trans. Inform. Syst. Secur. (TISSEC) 3(1), 30–50 (2000)
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)
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)
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)
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)
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
Corresponding author
Editor information
Editors and Affiliations
Rights 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)