Discovering Concrete Attacks on Website Authorization by Formal Analysis

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. 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.Sous l'effet de la généralisation des réseaux sociaux tels que Facebook, Twitter et Google+, les modules d'authentification unique ont été intégré à une quantité croissante de sites internet, phénomène amplifié depuis l'adoption de protocoles standardisés comme OAuth 2.0. L'analyse de ces nouveaux protocoles doit tenir compte de la puissance d'un attaquant web, qui peut exploiter des failles largement répandues, par exemple, le cross-site request forgery ou les redirecteurs ouverts. Nous proposons des modèles en pi-calcul appliqué pour différentes configurations du protocole OAuth 2.0, que nous vérifions à l'aide de ProVerif. Ces modèles s'appuyent sur la librairie WebSpi pour la modélisation des applications web et les divers attaquants correspondants. Notre approche est validée par la découverte de plusieurs dizaines de nouvelles failles dans des services aussi populaires que Yahoo ou Wordpress, lorsque qu'on accès à eux depuis des réseaux sociaux comme Facebook ou Twitter