SHF: Small: Capitalizing on First-Class SQL Support in the Ur/Web Programming Language

点击翻译按钮获取中文摘要

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.