Run-time Prevention of Logic Flaws in Multi-Party Web Applications

Modern web applications often rely on third-party services to provide their functionality to users. The integration of these services is a non-trivial task and, as shown by the large number of attacks against Single-Sign-On and Cashier-as-a-Service protocols, often opens up possibilities for logic flaws in web security protocols. In this thesis we explore the design challenges of a run-time security monitor for web protocols, identifying the fundamental ingredients needed to mitigate logic flaws in multi-party web applications. We then present a black-box methodology to generate verified monitors from applied pi-calculus specifications of web protocols. These monitors are guaranteed to have the security properties defined in the specification phase and can be deployed on the browser-side (ServiceWorker) and the server-side (reverse proxy). We evaluate the effectiveness of the approach by testing it against a pool of vulnerable applications that use the OAuth 2.0 protocol and that integrate the PayPal payment system.