Search

International audience; 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.

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.

Security-sensitive components, such as single sign-on APIs, need to be safely deployed on untrusted webpages. We present several new attacks on security components used in popular web applications that demonstrate how failing to isolate such components leaves them vulnerable to attacks both from the hosting website and other components loaded on the same page. These attacks are not prevented by browser security mechanisms alone, because they are caused by code interacting within the same origin. To mitigate these attacks, we propose to combine fine-grained component isolation at the JavaScript level with cryptographic mechanisms. We present Defensive JavaScript (DJS), a subset of the language that guarantees the behavioral integrity of trusted scripts loaded in an untrusted page. We give a sound type system, type inference tool and build defensive libraries for cryptography and data encodings. We show the effectiveness of our solution by implementing several isolation patterns that fix some of our original attacks. We use a translation of a fragment of DJS to to applied pi-calculus to verify concrete security policies of critical components against various classes of web attackers.; Certaines librairies critiques pour la sécurité, par exemple pour l'authentification unique (single sign-on), nécéssitent d'être chargées dans des sites tiers non sûrs. Nous montrons comment le manque d'isolation entre ces librairies et leur page hôte les rendent vulnérables aux scripts tiers qui partagent le même environnement, y compris pour des services très largements utilisés. Les mécanismes de sécurité des navigateurs sont impuissants face à ces attaques car elles interviennent en dessous de la granularité des politiques de sécurité, fixée par origine (protocole, nom de domaine et numéro de port). Afin de mitiger ces attaques, nous proposons de combiner une isolation fine de ces librairies au niveau du langage avec des protections cryptographiques. À cette fin, nous introduisons DJS, un fragment de JavaScript qui protège l'intégrité de l'exécution d'un script dans un environnement JavaScript hostile. Nous nous appuyons sur un système de types inférables et sur un ensemble de librairies (elles-même bien typées) pour implémenter des solutions génériques aux attaques que nous avons découvertes. Nous vérifions la validité de ces schémas à l'aide d'une traduction d'un sous-ensemble de DJS vers le pi-calcul appliqué contre différent types d'attaques.

Udgivelsesdato: Jul-Aug We extend the π-calculus with polyadic synchronisation, a generalisation of the communication mechanism which allows channel names to be composite. We show that this operator embeds nicely in the theory of π-calculus, we suggest that it permits divergence-free encodings of distributed calculi, and we show that a limited form of polyadic synchronisation can be encoded weakly in π-calculus. After showing that matching cannot be derived in π-calculus, we compare the expressivity of polyadic synchronisation, mixed choice and matching. In particular we show that the degree of synchronisation of a language increases its expressive power by means of a separation result in the style of Palamidessi's result for mixed choice.

Nowadays, many important activities in our lives involve the web. However, the software and protocols on which web applications are based were not designed with the appropriate level of security in mind. Many web applications have reached a level of complexity for which testing, code reviews and human inspection are no longer sufficient quality-assurance guarantees. Tools that employ static analysis techniques are needed in order to explore all possible execution paths through an application and guarantee the absence of undesirable behaviours. To make sure that an analysis captures the properties of interest, and to navigate the trade-offs between efficiency and precision, it is necessary to base the design and the development of static analysis tools on a firm understanding of the language to be analysed. When this underlying knowledge is missing or erroneous, tools can’t be trusted no matter what advanced techniques they use to perform their task. In this Thesis, we introduce KPHP, the first executable formal semantics of PHP, one of the most popular languages for server-side web programming. Then, we demonstrate its practical relevance by developing two verification tools, of increasing complexity, on top of it - a simple verifier based on symbolic execution and LTL model checking and a general purpose, fully configurable and extensible static analyser based on Abstract Interpretation. Our LTL-based tool leverages the existing symbolic execution and model checking support offered by K, our semantics framework of choice, and constitutes a first proof-of-concept of the usefulness of our semantics. Our abstract interpreter, on the other hand, represents a more significant and novel contribution to the field of static analysis of dynamic scripting languages (PHP in particular). Although our tool is still a prototype and therefore not well suited for handling large real-world codebases, we demonstrate how our semantics-based, principled approach to the development of verification tools has lead to the design of static analyses that outperform existing tools and approaches, both in terms of supported language features, precision, and breadth of possible applications. Open Access