JavaScript has transformed the way in which software systems are developed, deployed and extended. It is now used to build complex, security sensitive applications for communications, retail, and banking, and is even a primary building block of web browsers themselves. Unfortunately, the advent of JavaScript has also opened the door to new classes of security vulnerabilities, as applications manipulate security critical client information like browsing history, passwords, bank account numbers, social security numbers and so on. Worse, the absence of language-level isolation mechanisms makes it hard to establish confidentiality and integrity of key software components.
We believe that the key to making the web more secure is to develop a practical, precise and expressive type system for JavaScript and to use it as a foundation for developing security policies, analyses and enforcement mechanisms for JavaScript browser extensions and applications. Thus, we propose to develop a type system for JavaScript that is expressive enough to support JavaScript's dynamic idioms, practical enough to require minimal programmer intervention and hence, be capable of highly automated analysis of large code bases, and easily extensible enough to allow developers to specify and enforce different kinds of fine-grained security policies.
Our research will lead to the following contributions: End Users will be able to freely run extensions, plugins and rich browser applications from trusted sites, without having to suffer the plagues of code-injection, information exfiltration or the unpalatable cures of fully dynamic enforcement whose overhead can render sites unusable. Developers will be able to fully enjoy the fruits of static verification, in a familiar package: namely types. Types will allow developers to specify at the right granularity, the permissions required for some functionality, and will prevent the inadvertent vulnerabilities that are introduced by overprovisioning, or under-sanitization of data. Curators that aggregate third party applications (e.g. ``app stores" for various mobile platforms) will be able to use type-based certificates to quickly vet applications, thereby determining if an application is safe to host without compromising the reputation of the platform.
