Automated verification of role-based access control security models recovered from dynamic web applications

This paper presents an original Model-Driven-Engineering (MDE) approach to support the verification and testing of security properties in dynamic web applications. Based on a previously recovered UML-based fine-grained security model, the approach begins by transforming the model into a Prolog-based formal model. The Prolog model is then checked to verify whether the application conforms to specified access control security properties. We demonstrate the use of our method on the popular open source bulletin board system PhpBB 2.0, in the context of three test scenarios: testing for unauthorized access, web application security maintenance, and web application re-engineering.