Abstract
Role-Based Access Control (RBAC) is a popular authorization model used to manage resource-access constraints in a wide range of systems. The standard RBAC framework adopts a static, state-independent approach to define the access rights to the system resources. It is often insufficient for correct implementation of the desired functionality and should be augmented with the dynamic, i.e., a state-dependant view on the access control. In this paper, we present a work in progress on creating a domain-specific language and the tool support for modelling and verification of dynamic RBAC. They support a tabular representation of the static RBAC constraints together with the graphical model of the scenarios and enable an automated translation of them into an Event-B model.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Abrial, J.R.: Modeling in Event-B. Cambridge University Press, Cambridge (2010)
Ferraiolo, D.F., Sandhu, R.S., Gavrila, S.I., Kuhn, D.R., Chandramouli, R.: Proposed NIST standard for role-based access control. ACM Trans. Inf. Syst. Secur. 4(3), 224–274 (2001)
Iliasov, A., Troubitsyna, E., Laibinis, L., Romanovsky, A., Varpaaniemi, K., Ilic, D., Latvala, T.: Developing mode-rich satellite software by refinement in event-B. Sci. Comput. Program. 78(7), 884–905 (2013)
Iliasov, A., Troubitsyna, E., Laibinis, L., Romanovsky, A.: Patterns for refinement automation. In: de Boer, F.S., Bonsangue, M.M., Hallerstede, S., Leuschel, M. (eds.) FMCO 2009. LNCS, vol. 6286, pp. 70–88. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-17071-3_4
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)
Leuschel, M., Butler, M.: ProB: an automated analysis toolset for the B method. Int. J. Softw. Tools Technol. Transf. 10(2), 185–203 (2008)
Lopatkin, I., Iliasov, A., Romanovsky, A., Prokhorova, Y., Troubitsyna, E.: Patterns for representing FMEA in formal specification of control systems. In: HASE 2011, pp. 146–151. IEEE Computer Society (2011)
Milhau, J., Idani, A., Laleau, R., Labiadh, M., Ledru, Y., Frappier, M.: Combining UML, ASTD and B for the formal specification of an access control filter. ISSE 7(4), 303–313 (2011)
Rodin: Event-B platform. http://www.event-b.org/
Tikhonova, U., Manders, M., Boudewijns, R.: Visualization of formal specifications for understanding and debugging an industrial DSL. In: Milazzo, P., Varró, D., Wimmer, M. (eds.) STAF 2016. LNCS, vol. 9946, pp. 179–195. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-50230-4_13
Voelter, M.: DSL Engineering (2013). dslbook.org
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG, part of Springer Nature
About this paper
Cite this paper
Vistbakka, I., Barash, M., Troubitsyna, E. (2018). Towards Creating a DSL Facilitating Modelling of Dynamic Access Control in Event-B. In: Butler, M., Raschke, A., Hoang, T., Reichl, K. (eds) Abstract State Machines, Alloy, B, TLA, VDM, and Z. ABZ 2018. Lecture Notes in Computer Science(), vol 10817. Springer, Cham. https://doi.org/10.1007/978-3-319-91271-4_28
Download citation
DOI: https://doi.org/10.1007/978-3-319-91271-4_28
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-91270-7
Online ISBN: 978-3-319-91271-4
eBook Packages: Computer ScienceComputer Science (R0)