Web sites are often a mixture of static sites and programs that integrate relational databases as a back-end. As they evolve to meet ever-changing user needs, new versions of programs, interactions and functionalities may be added and existing ones may be removed or modified. Web sites require configuration and programming attention to assure security, confidentiality, and trust of the published information. During evolution of Web software, from one version to the next one, security properties may change and possible changes may include new flaws or corrections. Changes to security properties, including access control privileges, can be monitored by observing and analyzing changes between security models extracted from different versions of an application. This paper defines Property Satisfaction Profiles (PSP) as the satisfaction values of properties computed on the extracted models. This paper presents also an investigation of the evolution of the changes in the PSP computed on security models of different versions of a Web application. Model extraction and PSP computation can be performed in linear time on one version. Comparison between two versions is also linear and practical performance is fast. This paper reports results about experiments performed on 31 versions of phpBB, that is a publicly available bulletin board written in PHP. Version 1.0.0 (9547 LOC) to version 2.0.22 (40663 LOC) have been considered as a case study. Results show that the proposed approach can be used to observe and monitor the evolution of PSP in successive versions of the same software package. Suggestions for further research are also presented.

Whether for development, maintenance or refactoring, multiple steps in software development cycle require comprehension of a program's access control model (AC model). In this paper, we present a novel approach to reverse-engineer AC model structure from PHP source code. Using an hybrid approach combining static analysis and model checking techniques, we are able to extract AC model structure in a fast and precise way. An experimental tool was developed to evaluate the presented approach and report AC models using source code coloring. For this case study, Moodle, a medium-scale (approx. 625K lines of code), open-source PHP application with a rich AC model was investigated. Results revealed that, although very complex by design, implemented AC models may comparatively be very simple, suggesting that developers tend to maintain a low complexity level when implementing ACs. Detailed figures and distributions are reported. We believe the presented tool and approach may help in understanding and evaluating the implemented AC models in Web systems. Discussion of findings, limitations, and further research are presented.

Large scale software model checking is a difficult problem in part because of the complexity created by inter-procedural function calling. Fastest current solution for this problem claim a polynomial time for only a partial resolution. Static analysis suffers of the same complexity but some work has observed linear time and space complexity for some specific problems. Our research describes how we can adapt these specific inter-procedural static analysis to model-checking and prove the linear complexity of the analysis. Construction of the graph automaton for model checking is described using graph rewriting rules applied on the control flow graph and its application to a medium scale real application.

A new representation for inter-procedural analysis is presented. The representation only uses regular graph theory with guarded edges and variables for easy integration with model checkers but is limited to binary lattice inter-procedural analysis only.