Foundations of Secure Web Programming

Many important activities in our lives involve the web. We socialize on Facebook, have fun on YouTube, bank online, store our work in the cloud, find a job on LinkedIn and some of us even get married on Second Life. What makes web technology so exciting is that people and companies keep finding new and creative ways of using it for applications not foreseen by its designers: for example, using the web to make phone calls and mobile phones to browse the web.Unfortunately, for this very reason, the software and protocols on which web applications are based are not designed with the appropriate level of security in mind. Some of the information we share with web applications is very valuable, and should be protected carefully. News stories often remind us how cyber-crime negatively affects our finances, privacy and well-being.Web companies are strongly innovation-driven and focus on delivering new applications and features as quickly as possible, selecting which ones to maintain based on popularity or profitability. While the importance of security is acknowledged, the most common approach is to enforce security by monitoring the system and intervening when a security violation is detected. As this industry matures, there is a raising awareness that security must to be built into the languages and tools used to program web applications, and there is a growing need to gain some level of confidence that an application is effectively secure.In my career so far, I have studied in depth the foundations and principles for understanding computer programs and making sure that they work correctly without security breaches. Over the next few years, I will face the challenge of applying these principles to lay web programming on a sound formal ground. I want to understand deeply the current and emerging technologies that are used on the web, find ways to make them more secure, and contribute to the design of future web technologies and tools. This process will involve lots of creative thinking, and lead to innovative scientific results, because a secure web application must combine securely non-trivial components such as databases, internet protocols, scripting languages and web browsers.Here is an example of a first step in the direction of my proposal. Facebook users write Facebook applications in JavaScript (the language that sits inside web pages and makes them interactive) and share them with other users. This raises the problem of restricting such JavaScript, written by a potentially malicious user, to make sure that it is safe for all the other Facebook users. With colleagues in Stanford, I modelled JavaScript as a set of simple mathematical formulas with a very precise meaning, and once I understood the language and its security properties (by proving several mathematical results), I studied the way Facebook restricts JavaScript and found several flaws. A malicious user could have written bad Facebook applications, able to steal information and damage the profile or the web browser of other users. I contacted the Facebook team and discussed possible solutions, and they modified their restriction mechanism accordingly.This is just an example of how the work I am proposing consists in original foundational research that also has direct impact on the life of millions of people. Following a similar approach I will also model the languages that are used to program web servers, such as PHP, and the browser with its DOM libraries, and study their security properties. I will participate in the definition of standards related to web security, and influence the design of several major web applications such as the future versions of the iGoogle portal, Yahoo!'s advertising platform and the Microsoft Web Sandbox framework for mashups. I have already met researchers from these companies, all interested in receiving input from this line of research.

The proposed research will fulfill the need, acknowledged by the community of browser vendors and web application providers, to complement existing response and mitigation based approaches to web security with a principled approach based on formal methods, that includes security at the design stage of web applications and tools. Who will benefit from the proposed research? The main beneficiaries of this research are academics in related areas and industry-leading web companies. Other beneficiaries are web security consultants, practitioners, university students, online businesses, web users in general, and the project participants themselves. How will they benefit? This research will produce formal models of key components of web applications. These models will be used as a basis for further analysis by other academics, practitioners and industry. The techniques and tools developed to analyze the security properties of such models will constitute building blocks to develop further analyses and verification techniques, suitable to the requirements of these heterogeneous groups of users. Google, Yahoo! and Microsoft are working on projects aiming to develop programming languages, based on JavaScript, that enable mutually distrusting web content to interact safely. The ECMA standardization committee in charge of JavaScript plans to propose a new standard for a Secure ECMAScript. All these projects expressed interest in the models of web components and the security analyses developed by my project, and will benefit from them. Consultants and practitioners will benefit from the overall knowledge produced by the project, and by the static analysis tools. The knowledge produced by this project will also provide undergraduate students in Computer Science with a coherent resource where to learn about web security, its practice, its underlying principles and its applications. A byproduct of the research will be to enhance the quality of life of Internet users, and the economic competitiveness of Internet-enabled business by making web applications more secure, as for example demonstrated by my discovery of vulnerabilities in Facebook. This will be of special benefit to the UK, that has a large financial services sector that is seriously exposed to expensive online fraud. Besides the expected career outcomes of pursuing this research (reputation, publications, PhD award, etc.), the researchers involved (fellow, PhD student and collaborators) will develop transferable skills on web application vulnerability testing that could be used for consultancy-related activities. What will be done to ensure that they benefit? Academics will be informed about the research outcomes by direct collaboration, research visits and publications in major conferences, workshops and journals. The formal models and analysis tools produced by the project will be made available on a dedicated web site. I will visit and maintain an email-based dialogue with the ECMA working group and the research teams at Google, Yahoo! and Microsoft. Consultants and practitioners will be informed about the research outcomes through the OWASP organization and dedicated events organized by OWASP or the ISST centre at Imperial. For the students, I plan to design and teach the syllabus of an undergraduate course at Imperial College centered on web application security. The material for the course will be available to use or modify at other academic institutions. To the benefit of Internet companies and users, as I validate my research results by testing against popular web sites, I will follow responsible disclosure practices to inform the site providers of any vulnerabilities, and help them to prevent exploitation and secure their sites.