SPaCiTE -- Web Application Testing Engine

Web applications and web services enjoy an ever-increasing popularity. Such applications have to face a variety of sophisticated and subtle attacks. The difficulty of identifying respective vulnerabilities steadily increases with the complexity of applications. Moreover, the art of penetration testing predominantly depends on the skills of highly trained test experts. The difficulty to test web applications hence represents a daunting challenge to their developers. As a step towards improving security analyses, model checking has, at the model level, been found capable of identifying complex attacks and thus moving security analyses towards a push-button technology. In order to bridge the gap with actual systems, we present Spa Cite. This tool relies on a dedicated model-checker for security analyses that generates potential attacks with regard to common vulnerabilities in web applications. Then, it semi-automatically runs those attacks on the System Under Validation (SUV) and reports which vulnerabilities were successfully exploited. We applied Spa Cite to Role-Based-Access-Control (RBAC) and Cross-Site Scripting (XSS) lessons of Web Goat, an insecure web application maintained by OWASP. The tool successfully reproduced RBAC and XSS attacks.