A transformation-driven approach to the verification of security policies in web designs

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. © Springer-Verlag Berlin Heidelberg 2007.