Abstract
Verification and validation of access-control policies for information systems is a difficult yet necessary task. In order to take advantage of the formal properties and tools of the B method, we introduce in this paper a metamodel of the B modeling of access control policies. This metamodel lead to the development of a formal prototype of an access control filter combined to the system. It allows verification and validation of policies before implementation.
This research is funded by ANR (France) as part of the SELKIS project (ANR-08-SEGI-018) and by NSERC (Canada).
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
Preview
Unable to display preview. Download preview PDF.
References
Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press (1996)
Consortium, T.O.: ORKA — Organizational Control Architecture (2010), http://www.organisatorische-kontrolle.de/index-en.htm
Embe-Jiague, M., St-Denis, R., Laleau, R., Gervais, F.: A bpel implementation of a security filter. In: PhD Symposium of 8th European Conference on Web Services (2010)
Fraikin, B., Gervais, F., Frappier, M., Laleau, R., Richard, M.: Synthesizing information systems: the apis project. In: First International Conference on Research Challenges in Information Science (RCIS), Ouarzazate, Morocco, p. 12 (April 2007)
Frappier, M., Gervais, F., Laleau, R., Fraikin, B., St-Denis, R.: Extending statecharts with process algebra operators. Innovations in Systems and Software Engineering 4(3), 285–292 (2008)
Idani, A.: B/UML: Mise en relation de spécifications B et de descriptions UML pour l’aide à la validation externe de développements formels en B (2006)
Leuschel, M., Butler, M.J.: 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)
Lodderstedt, T., Basin, D., Doser, J.: SecureUML: A UML-Based Modeling Language for Model-Driven Security. In: Jézéquel, J.-M., Hussmann, H., Cook, S. (eds.) UML 2002. LNCS, vol. 2460, pp. 426–441. Springer, Heidelberg (2002)
Milhau, J., Frappier, M., Gervais, F., Laleau, R.: Systematic Translation Rules from astd to Event-B. In: Méry, D., Merz, S. (eds.) IFM 2010. LNCS, vol. 6396, pp. 245–259. Springer, Heidelberg (2010)
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. Innovations in Systems and Software Engineering 7(4), 303–313 (2011)
Neumann, G., Strembeck, M.: An approach to engineer and enforce context constraints in an rbac environment. In: Proceedings of the 8th ACM Symposium on Access Control Models and Technologies, SACMAT 2003, pp. 65–79 (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Milhau, J., Frappier, M., Laleau, R. (2012). A Metamodel of the B Modeling of Access-Control Policies: Work in Progress. In: Garcia-Alfaro, J., Lafourcade, P. (eds) Foundations and Practice of Security. FPS 2011. Lecture Notes in Computer Science, vol 6888. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-27901-0_19
Download citation
DOI: https://doi.org/10.1007/978-3-642-27901-0_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-27900-3
Online ISBN: 978-3-642-27901-0
eBook Packages: Computer ScienceComputer Science (R0)