Abstract
The early detection of potential threats during the modelling and design phase of a Secure Information System is required because it favours the design of a robust access control policy and the prevention of malicious behaviours during system execution. This paper deals with internal attacks which can be made by people inside the organization. Such attacks are difficult to detect because insiders have authorized system access and also may be familiar with system policies and procedures. We are interested in finding attacks which conform to the access control policy, but lead to unwanted states. These attacks are favoured by policies involving authorization constraints, which grant or deny access depending on the evolution of the functional Information System state. In this context, we propose to model functional requirements and their Role Based Access Control (RBAC) policies using B machines and then to formally reason on both models. In order to extract insider attack scenarios from these B specifications, our approach first investigates symbolic behaviours. Then, the use of a model-checking tool allows to exhibit, from a symbolic behaviour, an observable concrete sequence of operations that can be followed by an attacker. In this paper, we show how this combination of symbolic analysis and model-checking allows to find out such insider attack scenarios.
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
References
Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)
Abrial, J.-R., Mussat, L.: Introducing dynamic constraints in B. In: Bert, D. (ed.) B 1998. LNCS, vol. 1393, pp. 83–128. Springer, Heidelberg (1998)
Anastasakis, K., Bordbar, B., Georg, G., Ray, I.: UML2Alloy: a challenging model transformation. In: Engels, G., Opdyke, B., Schmidt, D.C., Weil, F. (eds.) MODELS 2007. LNCS, vol. 4735, pp. 436–450. Springer, Heidelberg (2007)
Basin, D., Clavel, M., Doser, J., Egea, M.: Automated analysis of security-design models. Inf. Softw. Technol. 51, 815–831 (2009)
Basin, D., Doser, J., Lodderstedt, T.: Model driven security: from UML models to access control infrastructures. ACM Trans. Softw. Eng. Methodol. 15(1), 39–91 (2006)
Becker, M.Y., Nanz, S.: A logic for state-modifying authorization policies. ACM Trans. Inf. Syst. Secur. 13(3), 20:1–20:28 (2010)
Bert, D., Potet, M.-L., Stouls, N.: GeneSyst: a tool to reason about behavioral aspects of B event specifications. Application to security properties. In: Treharne, H., King, S., Henson, M., Schneider, S. (eds.) ZB 2005. LNCS, vol. 3455, pp. 299–318. Springer, Heidelberg (2005)
Fisler, K., Krishnamurthi, S., Meyerovich, L.A., Tschantz, M.C.: Verification and change-impact analysis of access-control policies. In: Proceedings of the 27th International Conference on Software Engineering, ICSE 2005, pp. 196–205. ACM, New York (2005)
Koleini, M., Ryan, M.: A knowledge-based verification method for dynamic access control policies. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 243–258. Springer, Heidelberg (2011)
Kuhlmann, M., Sohr, K., Gogolla, M.: Employing UML and OCL for designing and analysing role-based access control. Math. Struct. Comput. Sci. 23(4), 796–833 (2013)
Lano, K., Clark, D., Androutsopoulos, K.: UML to B: formal verification of object-oriented models. In: Boiten, E.A., Derrick, J., Smith, G. (eds.) IFM 2004. LNCS, vol. 2999, pp. 187–206. Springer, Heidelberg (2004)
Ledru, Y., Idani, A., Milhau, J., Qamar, N., Laleau, R., Richier, J.-L., Labiadh, M.-A.: Taking into account functional models in the validation of IS security policies. In: Salinesi, C., Pastor, O. (eds.) CAiSE Workshops 2011. LNBIP, vol. 83, pp. 592–606. Springer, Heidelberg (2011)
Ledru, Y., Idani, A., Milhau, J., Qamar, N., Laleau, R., Richier, J.-L., Labiadh, M.-A.: Validation of IS security policies featuring authorisation constraints. Int. J. Inf. Syst. Model. Des. (IJISMD) 6, 24–46 (2014)
Ledru, Y., Qamar, N., Idani, A., Richier, J.-L., Labiadh, M.-A.: Validation of security policies by the animation of Z specifications. In: Proceedings of the 16th ACM Symposium on Access Control Models and Technologies, SACMAT 2011. ACM, New York (2011)
Ledru, Y., Idani, A., Richier, J.-L.: Validation of a security policy by the test of its formal B specification - a case study. In: 3rd International Workshop on Formal Methods in Software Engineering (FormaliSE 2015), Colocated with International Conference on Software Engineering, pp. 13–22. IEEE Computer Society (2015)
Leuschel, M., Butler, M.: ProB: a model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855–874. Springer, Heidelberg (2003)
Mammar, A., Frappier, M.: Proof-based verification approaches for dynamic properties: application to the information system domain. Formal Aspects Comput. 27(2), 335–374 (2015)
Qamar, N., Ledru, Y., Idani, A.: Evaluating RBAC supported techniques and their validation and verification. In: 6th International Conference on Availability, Reliability and Security (ARES 2011). IEEE Computer Society, Vienna, Autriche, August 2011
Radhouani, A., Idani, A., Ledru, Y., Rajeb, N.B.: Extraction of insider attack scenarios from a formal information system modeling. In: 5th International Workshop on Formal Methods for Security (FMS) (2014)
Snook, C., Butler, M.: UML-B: formal modeling and design aided by UML. ACM Trans. Softw. Eng. Methodol. 15(1), 92–122 (2006)
Toahchoodee, M., Ray, I., Anastasakis, K., Georg, G., Bordbar, B.: Ensuring spatio-temporal access control for real-world applications. In: Proceedings of the 14th ACM Symposium on Access Control Models and Technologies, SACMAT 2009, pp. 13–22. ACM, New York (2009)
Woodcock, J., Larsen, P.G., Bicarregui, J., Fitzgerald, J.: Formal methods: practice and experience. ACM Comput. Surv. 41(4), 19:1–19:36 (2009)
Zao, J., Wee, H., Chu, J., Jackson, D.: RBAC schema verification using lightweight formal model and constraint analysis. In: Proceedings of the 8th ACM Symposium on Access Control Models and Technologies, SACMAT 2003. ACM (2003)
Zhang, N., Ryan, M.D., Guelev, D.P.: Evaluating access control policies through model checking. In: Zhou, J., López, J., Deng, R.H., Bao, F. (eds.) ISC 2005. LNCS, vol. 3650, pp. 446–460. Springer, Heidelberg (2005)
Zhang, N., Ryan, M., Guelev, D.P.: Synthesising verified access control systems through model checking. J. Comput. Secur. 16(1), 1–61 (2008)
Acknowledgments
This work is supported by the french MESR. The authors would like to thank the anonymous reviewers for their valuable comments which contributes to improve this paper.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Radhouani, A., Idani, A., Ledru, Y., Ben Rajeb, N. (2015). Symbolic Search of Insider Attack Scenarios from a Formal Information System Modeling. In: Koutny, M., Desel, J., Haddad, S. (eds) Transactions on Petri Nets and Other Models of Concurrency X. Lecture Notes in Computer Science(), vol 9410. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-48650-4_7
Download citation
DOI: https://doi.org/10.1007/978-3-662-48650-4_7
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-48649-8
Online ISBN: 978-3-662-48650-4
eBook Packages: Computer ScienceComputer Science (R0)