| NSF Org: |
CCF Division of Computing and Communication Foundations |
| Recipient: |
|
| Initial Amendment Date: | August 28, 2012 |
| Latest Amendment Date: | August 28, 2012 |
| Award Number: | 1217501 |
| Award Instrument: | Standard Grant |
| Program Manager: |
Anindya Banerjee
abanerje@nsf.gov (703)292-7885 CCF Division of Computing and Communication Foundations CSE Directorate for Computer and Information Science and Engineering |
| Start Date: | September 1, 2012 |
| End Date: | August 31, 2016 (Estimated) |
| Total Intended Award Amount: | $500,000.00 |
| Total Awarded Amount to Date: | $500,000.00 |
| Funds Obligated to Date: |
|
| History of Investigator: |
|
| Recipient Sponsored Research Office: |
77 MASSACHUSETTS AVE CAMBRIDGE MA US 02139-4301 (617)253-1000 |
| Sponsor Congressional District: |
|
| Primary Place of Performance: |
MA US 02139-4301 |
| Primary Place of
Performance Congressional District: |
|
| Unique Entity Identifier (UEI): |
|
| Parent UEI: |
|
| NSF Program(s): | Software & Hardware Foundation |
| Primary Program Source: |
|
| Program Reference Code(s): |
|
| Program Element Code(s): |
|
| Award Agency Code: | 4900 |
| Fund Agency Code: | 4900 |
| Assistance Listing Number(s): | 47.070 |
ABSTRACT
The World Wide Web has become one of the most popular platforms for deploying rich software applications, and most Web applications include interfaces to persistent databases, many implemented with the SQL language. Mainstream programming techniques provide programmers with little help in construction of correct database interface code. As a result, many Web applications include serious security vulnerabilities that allow attackers to read others' private data, or even delete or corrupt it. Furthermore, programmers expend substantial effort reimplementing similar functionality for each new application and its new data model. This project studies programming tool support that can help solve both of these problems, based on a programming language and compiler that in a sense "understand" SQL database access.
A connecting thread in the project's technical approach is real-world application of computer theorem proving technology. The programming language, Ur/Web, is based on dependent type theory, a language paradigm pioneered by interactive mathematical theorem proving tools. In the Web application context, type theory provides a unified framework for enforcing key program properties, such as invulnerability to code injection attacks and other common security problems. On top of this is built support for metaprogramming, or programs that generate programs, where the key security properties ought to be guaranteed for any code outputs of a metaprogram. One major thrust of the project is using metaprogramming to reify coding patterns as reusable libraries, dramatically reducing time and effort needed to construct a new application. The other major thrust is static program analysis, where symbolic execution and automated theorem proving are used to verify formally that Web applications conform to declarative security policies, covering information flow and access control. Metaprogramming will support component-based construction with module-local reasoning, while the static analysis ensures global consistency of programs from a security perspective.
PUBLICATIONS PRODUCED AS A RESULT OF THIS RESEARCH
Note:
When clicking on a Digital Object Identifier (DOI) number, you will be taken to an external
site maintained by the publisher. Some full text articles may not yet be available without a
charge during the embargo (administrative interval).
Some links on this page may take you to non-federal websites. Their policies may differ from
this site.
PROJECT OUTCOMES REPORT
Disclaimer
This Project Outcomes Report for the General Public is displayed verbatim as submitted by the Principal Investigator (PI) for this award. Any opinions, findings, and conclusions or recommendations expressed in this Report are those of the PI and do not necessarily reflect the views of the National Science Foundation; NSF has not approved or endorsed its content.
This project investigated new ways to take advantage of Ur/Web, a programming language specialized for building interactive Web sites (applications). In particular, Ur/Web is distinguished by more specialized features for accessing databases based on the popular SQL language. In a sense, the Ur/Web compiler "understands" how an application is using the database, where mainstream compilers and libraries lack any such understanding. As a result, the Ur/Web compiler can do a better job of checking programs for errors and making them run quickly.
One key outcome is the Ur/Web People Organizer (UPO), a production-ready code library written in Ur/Web. With UPO, applications can be assembled quickly by combining standard concepts like message forums and polls, where these standard concepts nontheless need to be customized to the application in subtle ways. Such a concept exists as a first-class module in UPO, with a formal specification of the dimensions of customization and of what functionality is offered in return. These specifications are type signatures, thus making them relatively accessible to programmers.
Another outcome is Sqlcache, a new compiler optimization that speeds up SQL-based Ur/Web programs without requiring any extra work by the programmer. From the same code that Ur/Web programmers would write anyway, Sqlcache infers opportunities to cache database results. That is, when a set of results is retrieved from the database, the program saves it in memory, so that the program can skip future executions of the same query. These caches are also used to save whole segments of generated web pages, some of which may depend on multiple different queries. The key challenge here is to also infer which invalidations are necessary: when the program makes database modifications, some of the old saved query results may no longer be up-to-date, so they must be removed from caches. The approach taken also scales to concurrent execution of Web applications, allowing many cache operations to execute simultaneously, in common workloads.
On the side of practice, the project has produced several artifacts that are usable for real-world programming today. The Ur/Web compiler is available as open source, including in popular package systems for Linux and Macintosh platforms. It compares favorably to alternative tools in dimensions like performance of compiled Web applications, as shown by a third-party initiative called the TechEmpower Web Framework Benchmarks, where Ur/Web places a close second out of 194 tool combinations used for the marquee benchmark. The UPO framework is also available as open source and has been used for a number of production Web applications within MIT, with a total of about 500 users between them.
Last Modified: 11/30/2016
Modified by: Adam J Chlipala
Please report errors in award information by writing to: awardsearch@nsf.gov.
