Abstract
In this paper, we present a verification framework for security policies of Web designs. The framework is based on the transformation of the models that conform the system design into a formalism where further analysis can be performed. The transformation is specified as a triple graph transformation system, which in addition creates mappings between the elements in the source and target models. This allows the back-annotation of the analysis results to the original model by means of triple graphical patterns. The verification mechanisms are provided by the designer of the Web design language, together with the language specification. However, the complexities of the formalisms are hidden to the developer who uses the language.
As case study, we apply these ideas to Labyrinth, a domain specific language oriented to the design of Web applications. The analysis is done by a transformation into the Petri nets formalism, and then performing model checking on the coverability graph. The framework is supported by the meta-modelling tool AToM3.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Aedo, I., Díaz, P., Montero, S.: A methodological approach for hypermedia security modelling. Inform. Software Technol. 45(5), 229–239 (2003)
ANSI INCITS 359-2004. Role Based Access Control (2004)
Ayachit, M.M., Xu, H.: A Petri Net based XML Firewall Security Model for Web Services Invocation. In: Proc. (547) Communication, Network, and Information Security (2006)
Berry, D.M.: Formal methods: the very idea. Some thoughts about why they work when they work. Science of Computer Programming 42(1), 11–27 (2002)
Ceri, S., Fraternali, P., Bongio, A., Brambilla, M., Comai, S., Matera, M.: Designing Data-Intensive Web Applications. Elsevier, Amsterdam (2003)
Clarke, E.M., Grumberg, O., Long, D.: Model Checking. In: Broy, M. (ed.) Deductive Program Design. Proceedings of the International Summer School on Deductive Program Design Marktoberdorf, Germany, 1994. NATO ASI Series F, vol. 152, Springer, Heidelberg (1996)
Díaz, P., Aedo, I., Panetsos, F.: Labyrinth, an abstract model for hypermedia applications. description of its static components. Information Systems 22(8), 447–464 (1997)
Díaz, P., Montero, S., Aedo, I.: Modelling hypermedia and web applications: the Ariadne Development Method. Information Systems 30(8), 649–673 (2005)
Ehrig, H., Engels, G., Kreowski, H.-J., Rozenberg, G.: Handbook of Graph Grammars and Computing by Graph Transformation, vol. 1. World Scientific, Singapore (1997)
Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamentals of Algebraic Graph Transformation. In: Monographs in Theoretical Computer Science, Springer, Heidelberg (2006)
Furuta, R., Na, J.: Applying programmable browsing semantics within the context of the world-wide web. In: Proc. of Hypertext’02, pp. 23–24. ACM Press, New York (2002)
Guerra, E., Díaz, P., de Lara, J.: A formal approach to the generation of visual language environments supporting multiple views. In: Proc. VL/HCC’05, pp. 284–286. IEEE Computer Society Press, Los Alamitos (2005)
Guerra, E., de Lara, J.: Attributed typed triple graph transformation with inheritance in the double pushout approach. Tech. Report UC3M-TR-CS-06-01, Universidad Carlos III (2006)
Guerra, E., de Lara, J.: Model View Management with Triple Graph Transformation Systems. In: Corradini, A., Ehrig, H., Montanari, U., Ribeiro, L., Rozenberg, G. (eds.) ICGT 2006. LNCS, vol. 4178, pp. 351–366. Springer, Heidelberg (2006)
Koch, N., Kraus, A.: Towards a Common Metamodel for the Development of Web Applications. In: Lovelle, J.M.C., Rodríguez, B.M.G., Gayo, J.E.L., Ruiz, M.d.P.P., Aguilar, L.J. (eds.) ICWE 2003. LNCS, vol. 2722, pp. 497–506. Springer, Heidelberg (2003)
Koch, M., Parisi-Presicce, F.: Visual Specifications of Policies and Their Verification. In: Pezzé, M. (ed.) ETAPS 2003 and FASE 2003. LNCS, vol. 2621, pp. 278–293. Springer, Heidelberg (2003)
de Lara, J., Vangheluwe, H.: AToM 3: A tool for multi-formalism modelling and meta-modelling. In: Kutsche, R.-D., Weber, H. (eds.) ETAPS 2002 and FASE 2002. LNCS, vol. 2306, pp. 174–188. Springer, Heidelberg (2002)
Li, N., Tripunitara, M.V.: Security Analysis in Role-Based Access Control. ACM Transactions on Information and System Security 9(4), 391–420 (2006)
Machado, R.J., Lassen, K.B., Oliveira, S., Couto, M., Pinto, P.: Execution of UML Models with CPN Tools for Workflow Requirements Validation. In: Proc. of the Sixth Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools. pp. 231–250 (2005)
Murata, T.: Petri nets: Properties, analysis and applications. In: Proceedings of the IEEE, vol. 77(4) pp. 541–580 (1989)
Schaad, A., Lotz, V., Sohr, K.: A Model-checking Approach to Analysing Organisational Controls in a Loan Origination Process SACMAT 2006. pp. 139–149 (2006)
Shin, W., Lee, J.G., Kim, H.K., Sakurai, K.: Procedural Constraints in the Extended RBAC and the Coloured Petri Net Modeling. IEICE Trans. on Fundamentals 88(1), 327–330 (2005)
Varró, D., Varró, G., Pataricza, A.: Designing the automatic transformation of visual languages. Sci. Comp. Programming 44(2), 205–227 (2002)
Xie, F., Levin, V., Browne, J.C.: ObjectCheck: A Model Checking Tool for Executable Object-oriented Software System Designs. In: Kutsche, R.-D., Weber, H. (eds.) ETAPS 2002 and FASE 2002. LNCS, vol. 2306, pp. 331–335. Springer, Heidelberg (2002)
Zhang, N., Ryan, M., Guelev, D.P.: Evaluating Access Control Policies Through Model Checking. In: Zhou, J., Lopez, J., Deng, R.H., Bao, F. (eds.) ISC 2005. LNCS, vol. 3650, pp. 446–460. Springer, Heidelberg (2005)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Guerra, E., Sanz, D., Díaz, P., Aedo, I. (2007). A Transformation-Driven Approach to the Verification of Security Policies in Web Designs. In: Baresi, L., Fraternali, P., Houben, GJ. (eds) Web Engineering. ICWE 2007. Lecture Notes in Computer Science, vol 4607. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73597-7_22
Download citation
DOI: https://doi.org/10.1007/978-3-540-73597-7_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73596-0
Online ISBN: 978-3-540-73597-7
eBook Packages: Computer ScienceComputer Science (R0)