Abstract
Several approaches dedicated to model access control policies (e.g. MDA-Security, SecureUML, UMLSec, etc.) have used the Model Driven Engineering paradigm in order to ensure a clear separation of business rules and constraints specific to a target technology. Their supporting techniques mainly focus on modeling and verification of security rules without taking into account the functional model of the application and its interaction with the security model. In order to take into account both models, we developed the B4MSecure platform. It is a Model Driven Engineering platform that allows to graphically model and formally reason on both functional and security models. It translates a UML class diagram associated to a SecureUML model into formal B specifications. The resulting B specifications follow the separation of concerns principles in order to be able to validate both models separately and then validate their interactions. This paper gives an overview of our platform.
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, New York (1996)
Basin, D.A., Clavel, M., Doser, J., Egea, M.: Automated analysis of security-design models. Inf. Soft. Technol. 51(5), 815–831 (2009)
Hazem, L., Levy, N., Marcano-Kamenoff, R.: UML2B: un outil pour la génération de modèles formels. In: Julliand, J. (ed.) AFADL 2004 - Session Outils (2004)
Laleau, R., Mammar, A.: An overview of a method and its support tool for generating B specifications from UML notations. In: 15th IEEE International Conference on Automated Software Engineering, pp. 269–272. IEEE Computer Society Press (2000)
Laleau, R., Polack, F.A.C.: Coming and going from UML to B: a proposal to support traceability in rigorous IS development. In: Bert, D., Bowen, J.P., C. Henson, M., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, pp. 517–534. Springer, Heidelberg (2002)
Ledang, H.: Automatic translation from UML specifications to B. In: Automated Software Engineering, p. 436. IEEE Computer Society (2001)
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)
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)
Meyer, E.: Développements formels par objets: utilisation conjointe de B et d’UML. Ph.D. thesis, Université de Nancy 2, Mars 2001
Milhau, J., Idani, A., Laleau, R., Labiadh, M.-A., Ledru, Y., Frappier, M.: Combining UML, ASTD and B for the formal specification of an access control filter. ISSE 7(4), 303–313 (2011)
OMG: Mda guide version 1.0.1, June 2003. http://www.omg.org/mda/
Radhouani, A., Idani, A., Ledru, Y., Rajeb, N.B.: Extraction of insider attack scenarios from a formal information system modeling. In: Proceedings of the Formal Methods for Security Workshop Co-located with the PetriNets-2014 Conference. CEUR Workshop Proceedings, vol. 1158, pp. 5–19. CEUR-WS.org (2014)
Snook, C., Butler, M.: U2B-A tool for translating UML-B models into B. In: Mermet, J. (ed) UML-B Specification for Proven Embedded Systems Design (2004)
Snook, C., Butler, M.: UML-B: formal modeling and design aided by UML. ACM Trans. Soft. Eng. Methodol. (TOSEM) 15(1), 92–122 (2006)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Idani, A., Ledru, Y. (2015). B for Modeling Secure Information Systems. In: Butler, M., Conchon, S., Zaïdi, F. (eds) Formal Methods and Software Engineering. ICFEM 2015. Lecture Notes in Computer Science(), vol 9407. Springer, Cham. https://doi.org/10.1007/978-3-319-25423-4_20
Download citation
DOI: https://doi.org/10.1007/978-3-319-25423-4_20
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-25422-7
Online ISBN: 978-3-319-25423-4
eBook Packages: Computer ScienceComputer Science (R0)