Sandboxing untrusted JavaScript
Abstract/Contents
- Abstract
- Many contemporary Web sites incorporate third-party content in the form of advertisements, social-networking widgets, and maps. A number of sites like Facebook and Twitter also allow users to post comments that are then served to others, or allow users to add their own applications to the site. Such third-party content often comprises of executable code, commonly written in JavaScript, that runs together with Web site's code in the user's browser. While such interweaving of codes from multiple sources often enhances the user experience, the Web site may not always trust the source of the third-party code. Moreover due to proliferation of ad-networks and content distribution networks, the true source of content may be hidden behind multiple levels of indirection. With the rapid rise in e-commerce and social interaction on the Web, there is a vast amount of sensitive user data displayed on Web pages today -- typically in the form of user-profile information, pictures, comments, credit card numbers, etc. Unless suitable restrictions are imposed, malicious third-party code executing within a Web page can easily steal or alter such sensitive information and therefore pose a significant security threat. For instance, a malicious advertisement on a page with a login form could use JavaScript to read login credentials from the form and send them to a remote server. Even worse, it could use JavaScript to define a key-logger that surreptitiously logs all user key presses and then sends this data to a (malicious) remote server. Websites presently combat this threat by filtering and rewriting untrusted JavaScript before placing it on the page. There are a number of such JavaScript "sandboxing" tools, including Facebook FBJS, Yahoo! ADSafe, Google Caja, and Microsoft WebSandbox. Despite their popularity, these mechanisms do not come with any rigorous specifications or guarantees. Moreover, it is even unclear what the intended security goals behind these mechanisms are. In this dissertation, we systematically design provably-correct mechanisms for sandboxing third-party JavaScript code on Web pages. We first formally define the key security goals behind sandboxing JavaScript, using Facebook FBJS and Yahoo! ADSafe as motivating examples. We then define an operational semantics for JavaScript based on the ECMA-262 language specification, thereby establishing a mathematical basis for reasoning about JavaScript programs. To the best of our knowledge, this is the first formal semantics of the entire standards-compliant JavaScript language. Using the operational semantics, we carefully design language-based mechanisms for achieving the aforesaid security goals. We back each of these mechanisms by rigorous proofs of correctness carried out using our operational semantics. We present a comparison of our sandboxing mechanisms with Facebook FBJS and Yahoo! ADSafe, and show our mechanisms to be no more restrictive than each of them, besides having the advantage of being systematically designed and provably correct. In addition, we also uncover several previously undiscovered vulnerabilities in Facebook FBJS and Yahoo! ADSafe. These vulnerabilities have been reported to the respective vendors and the proposed fixes have since been adopted. While language-based sandboxing mechanisms have been studied previously in the contexts of OS kernels and the Java Virtual Machine, JavaScript's lack of lexical scoping and closure-based encapsulation pose significant new challenges. We address these challenges by adapting ideas from the theory of inlined reference monitoring, capability-based security, and programming language semantics. Armed with the insights gained from designing sandboxing mechanisms, we also define a sub-language of JavaScript, called SecureECMAScript (SES), that is amenable to static analysis and wields itself well to defensive programming. We develop an operational semantics for a core subset SES-light of SES, and develop a provably-correct and fully-automated tool for reasoning about confinement properties of APIs defined in it. The language SES has been under proposal by the ECMA-262 committee (TC39) for adoption within future versions of the JavaScript standard.
Description
| Type of resource | text |
|---|---|
| Form | electronic; electronic resource; remote |
| Extent | 1 online resource. |
| Publication date | 2013 |
| Issuance | monographic |
| Language | English |
Creators/Contributors
| Associated with | Taly, Ankur |
|---|---|
| Associated with | Stanford University, Department of Computer Science. |
| Primary advisor | Mitchell, John |
| Thesis advisor | Mitchell, John |
| Thesis advisor | Aiken, Alexander |
| Thesis advisor | Boneh, Dan |
| Advisor | Aiken, Alexander |
| Advisor | Boneh, Dan |
Subjects
| Genre | Theses |
|---|
Bibliographic information
| Statement of responsibility | Ankur Taly. |
|---|---|
| Note | Submitted to the Department of Computer Science. |
| Thesis | Ph.D. Stanford University 2013 |
| Location | electronic resource |
Access conditions
- Copyright
- © 2013 by Ankur Taly
- License
- This work is licensed under a Creative Commons Attribution Non Commercial 3.0 Unported license (CC BY-NC).
Also listed in
Loading usage metrics...