AJACS

We all depend on web applications. We shop, bank, socialize, work, collaborate, or communicate thanks to them. In all these cases, we entrust our personal data to them. These applications have become pervasive because they are both powerful and very easy to use; they have thus had a tremendous impact, both from a societal or economic point of view. Unbeknownst to many users, most of these web applications consist of small programs, called scripts, that are downloaded and executed inside the user's browser. In some sense, the browser has become a virtual machine for web applications manipulating our data.

The combination of these aspects, namely the massive use of downloaded scripts running in parallel in the same context and working with our personal data, raises the following questions. How much can we trust these scripts? Are they malicious? Do they have bugs?

The practical answer to this question typically relies on a form of compartmentalization called same origin policy (SOP). In a nutshell, this policy ensures that a script sent by a web site can interact solely with data from the same web site. This data may be cookies set in the browser database or other scripts to be downloaded and run. Unfortunately, not only is the enforcement of this policy quite difficult, but the definition of the policy itself goes against the construction of mashups. Mashups are the integration of several web applications to provide a new service, such as the display of restaurant reviews on a map. This integration requires a way for the applications and their data to interact, going against the restrictions of the same origin policy. A second fundamental weakness in the SOP approach is the implicit trust in the visited web site: any script from the site may interact with any other script or data from the same site. This may cause issues for two reasons. First, a user may want to avoid running some of the scripts of a given site. For instance, social network sites often use scripts and cookies to gather information on the browsing habits of users (web tracking), usually without the user's consent. Some users may thus prefer a policy that would selectively prevent these scripts from running, but still allow other services to be performed. Second, a malicious script may have been injected on a site, using techniques such as cross site scripting. From a SOP point of view, these script are legitimate, yet they may allow an attacker to access sensitive data such as session identifiers. Recognizing these malicious scripts would foil these attacks.

The goal of the AJACS project is to provide strong security and privacy guarantees on the client side for web application scripts. To this end, we propose to define a mechanized semantics of the full JavaScript language, the most widely used language for the Web. We then propose to develop and prove correct analyses for JavaScript programs, in particular information flow analyses that guarantee no secret information is leaked to malicious parties. The definition of sub-languages of JavaScript, with certified compilation techniques targeting them, will allow us to derive more precise analyses. Finally, we propose to design and certify security and privacy enforcement mechanisms for web applications, including the APIs used to program real-world applications.