Programming abstractions and static analyses for the web 2.0 and beyond.

Lead Research Organisation: Imperial College London
Department Name: Computing

Abstract

Programming for the web is shifting from building applicationswhich feature network connectivity, to tying together, typicallyusing a scripting language, a set of functionalities alreadyoffered by several disparate sources available online.This new programming model involves many subtle issues, caused bythe interplay of concurrency, distribution, scripting, dataquerying and inter-operability. Moreover, it lacks the solidmathematical foundations that software science has provided, forexample, to imperative and functional programming.The purpose of this proposal is to study programming abstractionsand develop static analysis techniques to help support the robustand secure development of the next generation of web applications.It aims to develop a coherent set of ideas, calculi, and tools for dynamic web data and to use these theories to guide the implementation of a proof-of-concept scripting language for web programming.

Publications

10 25 50
publication icon
Bengtson J (2008) Refinement Types for Secure Implementations

publication icon
Bengtson J (2011) Refinement types for secure implementations in ACM Transactions on Programming Languages and Systems

publication icon
Maffeis S (2008) Behavioural equivalences for dynamic Web data in The Journal of Logic and Algebraic Programming

publication icon
Maffeis S (2009) Computer Security - ESORICS 2009 - 14th European Symposium on Research in Computer Security, Saint-Malo, France, September 21-23, 2009. Proceedings

publication icon
Maffeis S (2009) Language-Based Isolation of Untrusted JavaScript

publication icon
Maffeis S (2010) Object Capabilities and Isolation of Untrusted Web Applications

 
Description We developed formal models of security protocols and of a programming language for the web, and use them to improve the security of applications such as for example Facebook and Microsoft F#.
Exploitation Route Adopting our formal models and techniques to improve the security of web applications.
Sectors Digital/Communication/Information Technologies (including Software),Education,Security and Diplomacy
 
Description We reported security bugs in major web applications, used by millions of users, and help them fixing the bugs. We suggested ways applications can be made more secure. We provided intellectual tools to improve the design of web applications.
First Year Of Impact 2008
Sector Digital/Communication/Information Technologies (including Software),Security and Diplomacy
Impact Types Societal,Economic
 
Description CAF Fellowship
Amount £684,895 (GBP)
Funding ID EP/I004246/1 
Organisation Engineering and Physical Sciences Research Council (EPSRC) 
Sector Public
Country United Kingdom
Start 08/2010 
End 07/2015
 
Title Small-step Operational Semantics of JavaScript 
Description This website make publicly available the small-step operational semantics of ECMAScript 3.1, the standardised core of JavaScript, the most popular web programming language. The formal semantics was developed thanks to this project. 
Type Of Technology Webtool/Application 
Year Produced 2008 
Impact Researchers and practitioners used the website to improve their understanding of JavaScript. The corresponding research paper has already more than 100 citations. 
URL http://jssec.net/semantics