Abstract
Combination of formal and semi-formal methods is more and more required to produce specifications that can be, on the one hand, understood and thus validated by both designers and users and, on the other hand, precise enough to be verified by formal methods. This motivates our aim to use these complementary paradigms in order to deal with security aspects of information systems. This paper presents a methodology to specify access control policies starting with a set of graphical diagrams: UML for the functional model, SecureUML for static access control and ASTD for dynamic access control. These diagrams are then translated into a set of B machines. Finally, we present the formal specification of an access control filter that coordinates the different kinds of access control rules and the specification of functional operations. The goal of such B specifications is to rigorously check the access control policy of an information system taking advantage of tools from the B method.
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.References
Abrial JR (1996) The B-book: assigning programs to meanings. Cambridge University Press
Andrews T, Curbera F, Dholakia H, Goland Y, Klein J, Leymann F, Liu K, Roller D, Smith D, Thatte S, Trickovic I, Weerawarana S (2003) Business process execution language for Web services
Cuppens F, Miège A (2003) Modelling contexts in the Or-BAC model. In: Proceedings of the 19th annual computer security applications conference, ACSAC ’03. IEEE Computer Society, Washington, p 416
El Kalam AA, Benferhat S, Miège A, El Baida R, Cuppens F, Saurel C, Balbiani P, Deswarte Y, Trouessin G (2003) Organization based access control. In: POLICY ’03: proceedings of the 4th IEEE international workshop on policies for distributed systems and networks. IEEE Computer Society, Washington, p 120
Embe Jiague M, Frappier M., Gervais F, Laleau R, St-Denis R (2011) Enforcing ASTD access control policies to WS-BPEL processes deployed in a SOA environment. Int J Syst Service-Oriented Eng 2(2): 37–59
Ferraiolo DF, Kuhn DR, Chandramouli R (2003) Role-based access control. Artech House Inc., Norwood
Frappier M, Diagne F, Amel Mammar A (2011) Proving reachability in B using substitution refinement. In: B 2011 Workshop. Electronic Notes in Theoretical Computer Science (to appear)
Frappier M, Gervais F, Laleau R, Fraikin B, St-Denis R (2008) Extending statecharts with process algebra operators. Innov Syst Softw Eng 4(3): 285–292
Frappier M, St-Denis R (2003) EB3: an entity-based black-box specification method for information systems. Softw Syst Model 2: 134–149
Fraser MD, Kumar K, Vaishnavi VK (1991) Informal and formal requirements specification languages: bridging the gap. IEEE Trans Softw Eng 17(5): 454–465
Harel D (1987) Statecharts: a visual formalism for complex systems. Sci Comput Program 8(3): 231–274
Idani A, Labiadh MA, Ledru Y (2010) Infrastructure dirigée par les modèles pour une intégration adaptable et évolutive de UML et B. Ingénierie des Systèmes d’Information 15(3): 87–112
Jürjens J (2002) Umlsec: extending UML for secure systems development. In: Jézéquel JM, Hussmann H, Cook S (eds) UML 2002—the unified modeling language. Lecture notes in computer science, vol 2460. Springer, Heidelberg, pp 1–9
Laleau R, Mammar A (2000) An overview of a method and its support tool for generating B specifications from UML notations. In: Proceedings of the 15th IEEE international conference on automated software engineering, ASE ’00. IEEE Computer Society, Washington, pp 269–272
Lano K, Clark D, Androutsopoulos K (2004) UML to B: formal verification of object-oriented models. In: Integrated formal methods. Lecture notes in computer science, vol 2999. Springer, pp 187–206
Ledru Y, Idani A, Milhau J, Qamar N, Laleau R, Richier JL, Labiadh MA (2011) Taking into account functional models in the validation of is security policies. In: Salinesi C, Pastor Q, Aalst W, Mylopoulos J, Sadeh NM, Shaw MJ, Szyperski C (eds) Advanced information systems engineering workshops. Lecture notes in business information processing, vol 83. Springer, Heidelberg, pp 592–606
Leuschel M, Butler M (2003) ProB: a model checker for B. In: Araki K, Gnesi S, Mandrioli D (eds) FME 2003: formal methods. Lecture notes in computer science, vol 2805. Springer, Heidelberg, pp 855–874
Leuschel M, Butler MJ (2008) ProB: an automated analysis toolset for the B method. STTT 10(2): 185–203
Lodderstedt T, Basin DA, Doser J (2002) Secureuml: a UML-based modeling language for model-driven security. In: 5th International conference on the unified modeling language (UML). LNCS, vol 2460. Springer, Berlin, pp 426–441
Mammar A, Frappier M, Diagne F (2011) A proof-based approach to verifying reachability properties. In: Proceedings of the 2011 ACM symposium on applied computing, SAC ’11. ACM, New York, pp 1651–1657
Milhau J, Frappier M, Gervais F, Laleau R (2010) Systematic translation of EB3 and ASTD specifications in B and EventB. Technical report 30 v3.0, Université de Sherbrooke
Milhau J, Frappier M, Gervais F, Laleau R (2010) Systematic translation rules from ASTD to Event-B. In: Méry D, Merz S (eds) Integrated formal methods. Lecture notes in computer science, vol 6396. Springer, Berlin, pp 245–259
Preda S, Cuppens-Boulahia N, Cuppens F, Garcia-Alfaro J, Toutain L (2010) Model-driven security policy deployment: property oriented approach. In: International symposium on engineering secure software and systems (ESSOS’10). LNCS, vol 5965. Springer, Berlin, pp 123–139
Sandhu R, Coyne E, Feinstein H, Youman C (1996) Role-based access control models. IEEE Comput 29(2): 38–47
Snook C, Butler M (2004) U2B-A tool for translating UML-B models into B. In: Mermet J (ed) UML-B specification for proven embedded systems design
Snook C, Butler M (2006) UML-B: formal modeling and design aided by UML . ACM Trans Softw Eng Methodol 15(1): 92–122
Toahchoodee M, Ray I, Anastasakis K, Georg G, Bordbar B (2009) Ensuring spatio-temporal access control for real-world applications. In: Proceedings of the 14th ACM symposium on access control models and technologies, SACMAT ’09. ACM, New York, pp 13–22
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Milhau, J., Idani, A., Laleau, R. et al. Combining UML, ASTD and B for the formal specification of an access control filter. Innovations Syst Softw Eng 7, 303–313 (2011). https://doi.org/10.1007/s11334-011-0166-z
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11334-011-0166-z