A Formal and Automated Approach to Exploiting Multi-Stage Attacks of Web Applications

The complexity of modern web applications, due to the imple- mentation of new services, has rapidly increased the need of new automatic security analysis methods and tools. Today, the leading methodology for the security analysis of web applications is a combination of vulnerability assess- ment and penetration testing. Vulnerability assessment has received much attention and several tools have been proposed to identify vulnerabilities. On the other hand, penetration testing has been left to the experience of the security analyst. In this thesis, I address this problem by proposing a formal, model-based testing approach for the security analysis of web applications that can support the penetration testing phase. The approach I propose is based on the formal definition of web applications and their vulnerabilities which allow one to (i) reason about vulnerabilities of web applications and (ii) combine multiple vulnerabilities for the identification of complex, multi-stage attacks. I have developed WAFEx, an automated tool that implements my approach and I show its efficiency by applying it to real-world case studies. WAFEx was able to find previously unknown attacks, which are witness to the fact that WAFEx can generate, and exploit, attacks that, to the best of my knowledge, no other tool for the security analysis of web applications can find.