Thanks to the wide range of features offered by the World Wide Web (WWW), many web applications have been published and developed through different libraries and programming languages. Adapting to new changes, the Web quickly evolved into a complex ecosystem, introducing many security problems to its users. To solve these problems, instead of re-designing the Web, the vendors added the security patches (protocols, mechanisms)to the Web platform to provide a more convenient and more secure environment for web users. However, not only did these patches not completely resolve the security problems, but their implementations also introduced other security risks unbeknownst to website operators and users. In this thesis, I propose a novel research on two different security patches to understand and analyze their deployment in real-world scenarios and discover the unseen, neglected factors and the elements involved in exploiting their use: one security protocol, OAuth, and one security mechanism, CORS. As this thesis is based on offensive approaches, I develop automated methodologies, including novel strategies for analyzing and measuring the security qualities of the OAuth protocol and CORS mechanism in real-world scenarios.

The purpose of this thesis is to prevent websites located in public internet from accessing user's internal network through web browser. Acquired knowdledge about modern browser's security mechanism - same-origin policy and options of implementing the web browser extensions using WebExtensions, was used in the solution. Proposed solution is based on WebRequest API, which intercepts and modifies HTTP requests, and extends functionality of existing browser extension JavaScript Restrictor with the ability to detect and prevent the browser to be abused as a proxy for scanning and accessing user's internal network. The implemented solution was tested and accepted as a part of JavaScript Restrictor. The main benefit of this thesis is the protection from possible abusement of a web browser as a proxy, which is not present in existing extensions.

This diploma thesis first introduces the services of servers Prednasky.com and SuperLectures.com. After analyzing the solution it describes the design and development of a new dedicated video player that combines SuperLectures.com functionality as a web-embeddable HTML5 application.

Est-il possible de démontrer un théorème prouvant que l’accès aux données confidentielles d’un utilisateur d’un service Web (tel que GMail) nécessite la connaissance de son mot de passe, en supposant certaines hypothèses sur ce qu’un attaquant est incapable de faire (par exemple, casser des primitives cryptographiques ou accéder directement aux bases de données de Google), sans toutefois le restreindre au point d’exclure des attaques possibles en pratique?Il existe plusieurs facteurs spécifiques aux protocoles du Web qui rendent impossible une application directe des méthodes et outils existants issus du domaine de l’analyse des protocoles cryptographiques.Tout d’abord, les capacités d’un attaquant sur le Web vont largement au-delà de la simple manipulation des messages échangés entre le client et le serveur sur le réseau. Par exemple, il est tout à fait possible (et même fréquent en pratique) que l’utilisateur ait dans son navigateur un onglet contenant un site contrôlé par l’adversaire pendant qu’il se connecte à sa messagerie (par exemple, via une bannière publicitaire) ; cet onglet est, comme n’importe quel autre site, capable de provoquer l’envoi de requêtes arbitraires vers le serveur de GMail, bien que la politique d’isolation des pages du navigateur empêche la lecture directe de la réponse à ces requêtes. De plus, la procédure pour se connecter à GMail implique un empilement complexe de protocoles : tout d’abord, un canal chiffré, et dont le serveur est authentifié, est établi avec le protocole TLS ; puis, une session HTTP est créée en utilisant un cookie ; enfin, le navigateur exécute le code JavaScript retourné par le client, qui se charge de demander son mot de passe à l’utilisateur.Enfin, même en imaginant que la conception de ce système soit sûre, il suffit d’une erreur minime de programmation (par exemple, une simple instruction goto mal placée) pour que la sécurité de l’ensemble de l’édifice s’effondre.Le but de cette thèse est de bâtir un ensemble d’outils et de librairies permettant de programmer et d’analyser formellement de manière compositionelle la sécurité d’applicationsWeb confrontées à un modère plausible des capacités actuelles d’un attaquant sur le Web. Dans cette optique, nous étudions la conception des divers protocoles utilisés à chaque niveau de l’infrastructure du Web (TLS, X.509, HTTP, HTML, JavaScript) et évaluons leurs compositions respectives. Nous nous intéressons aussi aux implémentations existantes et en créons de nouvelles que nous prouvons correctes afin de servir de référence lors de comparaisons. Nos travaux mettent au jour un grand nombre de vulnérabilités aussi bien dans les protocoles que dans leurs implémentations, ainsi que dans les navigateurs, serveurs, et sites internet ; plusieurs de ces failles ont été reconnues d’importance critiques. Enfin, ces découvertes ont eu une influence sur les versions actuelles et futures du protocole TLS. / As ever more private user data gets stored on the Web, ensuring proper protection of this data (in particular when it transits through untrusted networks, or when it is accessed by the user from her browser) becomes increasingly critical. However, in order to formally prove that, for instance, email from GMail can only be accessed by knowing the user’s password, assuming some reasonable set of assumptions about what an attacker cannot do (e.g. he cannot break AES encryption), one must precisely understand the security properties of many complex protocols and standards (including DNS, TLS, X.509, HTTP, HTML,JavaScript), and more importantly, the composite security goals of the complete Web stack.In addition to this compositional security challenge, onemust account for the powerful additional attacker capabilities that are specific to the Web, besides the usual tampering of network messages. For instance, a user may browse a malicious pages while keeping an active GMail session in a tab; this page is allowed to trigger arbitrary, implicitly authenticated requests to GMail using JavaScript (even though the isolation policy of the browser may prevent it from reading the response). An attacker may also inject himself into honest page (for instance, as a malicious advertising script, or exploiting a data sanitization flaw), get the user to click bad links, or try to impersonate other pages.Besides the attacker, the protocols and applications are themselves a lot more complex than typical examples from the protocol analysis literature. Logging into GMail already requires multiple TLS sessions and HTTP requests between (at least) three principals, representing dozens of atomic messages. Hence, ad hoc models and hand written proofs do not scale to the complexity of Web protocols, mandating the use of advanced verification automation and modeling tools.Lastly, even assuming that the design of GMail is indeed secure against such an attacker, any single programming bug may completely undermine the security of the whole system. Therefore, in addition to modeling protocols based on their specification, it is necessary to evaluate implementations in order to achieve practical security.The goal of this thesis is to develop new tools and methods that can serve as the foundation towards an extensive compositional Web security analysis framework that could be used to implement and formally verify applications against a reasonably extensive model of attacker capabilities on the Web. To this end, we investigate the design of Web protocols at various levels (TLS, HTTP, HTML, JavaScript) and evaluate their composition using a broad range of formal methods, including symbolic protocol models, type systems, model extraction, and type-based program verification. We also analyze current implementations and develop some new verified versions to run tests against. We uncover a broad range of vulnerabilities in protocols and their implementations, and propose countermeasures that we formally verify, some of which have been implemented in browsers and by various websites. For instance, the Triple Handshake attack we discovered required a protocol fix (RFC 7627), and influenced the design of the new version 1.3 of the TLS protocol.

Dans cette thèse, nous nous sommes intéressés aux problématiques de sécurité et de confidentialité liées à l'utilisation d'applications web et à l'installation d'extensions de navigateurs. Parmi les attaques dont sont victimes les applications web, il y a celles très connues de type XSS (ou Cross-Site Scripting). Les extensions sont des logiciels tiers que les utilisateurs peuvent installer afin de booster les fonctionnalités des navigateurs et améliorer leur expérience utilisateur. Content Security Policy (CSP) est une politique de sécurité qui a été proposée pour contrer les attaques de type XSS. La Same Origin Policy (SOP) est une politique de sécurité fondamentale des navigateurs, régissant les interactions entre applications web. Par exemple, elle ne permet pas qu'une application accède aux données d'une autre application. Cependant, le mécanisme de Cross-Origin Resource Sharing (CORS) peut être implémenté par des applications désirant échanger des données entre elles. Tout d'abord, nous avons étudié l'intégration de CSP avec la Same Origin Policy (SOP) et démontré que SOP peut rendre CSP inefficace, surtout quand une application web ne protège pas toutes ses pages avec CSP, et qu'une page avec CSP imbrique ou est imbriquée dans une autre page sans ou avec un CSP différent et inefficace. Nous avons aussi élucidé la sémantique de CSP, en particulier les différences entre ses 3 versions, et leurs implémentations dans les navigateurs. Nous avons ainsi introduit le concept de CSP sans dépendances qui assure à une application la même protection contre les attaques, quelque soit le navigateur dans lequel elle s'exécute. Finalement, nous avons proposé et démontré comment étendre CSP dans son état actuel, afin de pallier à nombre de ses limitations qui ont été révélées dans d'autres études. Les contenus tiers dans les applications web permettent aux propriétaires de ces contenus de pister les utilisateurs quand ils naviguent sur le web. Pour éviter cela, nous avons introduit une nouvelle architecture web qui une fois déployée, supprime le pistage des utilisateurs. Dans un dernier temps, nous nous sommes intéressés aux extensions de navigateurs. Nous avons d'abord démontré que les extensions qu'un utilisateur installe et/ou les applications web auxquelles il se connecte, peuvent le distinguer d'autres utilisateurs. Nous avons aussi étudié les interactions entre extensions et applications web. Ainsi avons-nous trouvé plusieurs extensions dont les privilèges peuvent être exploités par des sites web afin d'accéder à des données sensibles de l'utilisateur. Par exemple, certaines extensions permettent à des applications web d'accéder aux contenus d'autres applications, bien que cela soit normalement interdit par la Same Origin Policy. Finalement, nous avons aussi trouvé qu'un grand nombre d'extensions a la possibilité de désactiver la Same Origin Policy dans le navigateur, en manipulant les entêtes CORS. Cela permet à un attaquant d'accéder aux données de l'utilisateur dans n'importe qu'elle autre application, comme par exemple ses mails, son profile sur les réseaux sociaux, et bien plus. Pour lutter contre ces problèmes, nous préconisons aux navigateurs un système de permissions plus fin et une analyse d'extensions plus poussée, afin d'alerter les utilisateurs des dangers réels liés aux extensions. / In this thesis, we studied security and privacy threats in web applications and browser extensions. There are many attacks targeting the web of which XSS (Cross-Site Scripting) is one of the most notorious. Third party tracking is the ability of an attacker to benefit from its presence in many web applications in order to track the user has she browses the web, and build her browsing profile. Extensions are third party software that users install to extend their browser functionality and improve their browsing experience. Malicious or poorly programmed extensions can be exploited by attackers in web applications, in order to benefit from extensions privileged capabilities and access sensitive user information. Content Security Policy (CSP) is a security mechanism for mitigating the impact of content injection attacks in general and in particular XSS. The Same Origin Policy (SOP) is a security mechanism implemented by browsers to isolate web applications of different origins from one another. In a first work on CSP, we analyzed the interplay of CSP with SOP and demonstrated that the latter allows the former to be bypassed. Then we scrutinized the three CSP versions and found that a CSP is differently interpreted depending on the browser, the version of CSP it implements, and how compliant the implementation is with respect to the specification. To help developers deploy effective policies that encompass all these differences in CSP versions and browsers implementations, we proposed the deployment of dependency-free policies that effectively protect against attacks in all browsers. Finally, previous studies have identified many limitations of CSP. We reviewed the different solutions proposed in the wild, and showed that they do not fully mitigate the identified shortcomings of CSP. Therefore, we proposed to extend the CSP specification, and showed the feasibility of our proposals with an example of implementation. Regarding third party tracking, we introduced and implemented a tracking preserving architecture, that can be deployed by web developers willing to include third party content in their applications while preventing tracking. Intuitively, third party requests are automatically routed to a trusted middle party server which removes tracking information from the requests. Finally considering browser extensions, we first showed that the extensions that users install and the websites they are logged into, can serve to uniquely identify and track them. We then studied the communications between browser extensions and web applications and demonstrate that malicious or poorly programmed extensions can be exploited by web applications to benefit from extensions privileged capabilities. Also, we demonstrated that extensions can disable the Same Origin Policy by tampering with CORS headers. All this enables web applications to read sensitive user information. To mitigate these threats, we proposed countermeasures and a more fine-grained permissions system and review process for browser extensions. We believe that this can help browser vendors identify malicious extensions and warn users about the threats posed by extensions they install.