Discovering concrete attacks on website authorization by formal analysis¹

Issue title: Web Application Security – Web @ 25

Guest editors: Lieven DesmetGuest Editor, Martin JohnsGuest Editor, Benjamin LivshitsGuest Editor and Andrei SabelfeldGuest Editor

Article type: Research Article

Authors: Bansal, Chetan^a | Bhargavan, Karthikeyan^{b; *} | Delignat-Lavaud, Antoine^b | Maffeis, Sergio^c

Affiliations: [a] BITS Pilani-Goa, Goa, India | [b] Inria Paris-Rocquencourt, Paris, France | [c] Imperial College London, London, UK

Correspondence: [*] Corresponding author: Karthikeyan Bhargavan, Prosecco, Inria Paris, 23 avenue d'Italie, CS 81321, 75214 Paris Cedex 13, France. E-mail: karthikeyan.bhargavan@inria.fr.

Note: [1] This paper is an extended and revised version of [13].

Abstract: Social sign-on and social sharing are becoming an ever more popular feature of web applications. This success is largely due to the APIs and support offered by prominent social networks, such as Facebook, Twitter and Google, on the basis of new open standards such as the OAuth 2.0 authorization protocol. A formal analysis of these protocols must account for malicious websites and common web application vulnerabilities, such as cross-site request forgery and open redirectors. We model several configurations of the OAuth 2.0 protocol in the applied pi-calculus and verify them using ProVerif. Our models rely on WebSpi, a new library for modeling web applications and web-based attackers that is designed to help discover concrete attacks on websites. To ease the task of writing formal models in our framework, we present a model extraction tool that automatically translates programs written in subsets of PHP and JavaScript to the applied pi-calculus. Our approach is validated by finding dozens of previously unknown vulnerabilities in popular websites such as Yahoo and WordPress, when they connect to social networks such as Twitter and Facebook.

Keywords: Web security, pi-calculus, formal verification, automated analysis, ProVerif, threat modeling, web attacks, cross-site request forgery, open redirectors, OAuth protocol

DOI: 10.3233/JCS-140503

Journal: Journal of Computer Security, vol. 22, no. 4, pp. 601-657, 2014