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

万维网已经成为部署富软件应用程序的最流行的平台之一，并且大多数Web应用程序都包含到持久数据库的接口，其中许多是用SQL语言实现的。主流编程技术在构建正确的数据库接口代码方面给程序员提供的帮助很少。因此，许多Web应用程序包含严重的安全漏洞，这些漏洞允许攻击者读取他人的私有数据，甚至删除或破坏这些数据。此外，程序员花费大量精力为每个新应用程序及其新数据模型重新实现类似的功能。本项目研究的编程工具支持可以帮助解决这两个问题，基于某种意义上“理解”SQL数据库访问的编程语言和编译器。项目技术方法的一个连接点是计算机定理证明技术的实际应用。编程语言Ur/Web基于依赖类型理论，这是一种由交互式数学定理证明工具开创的语言范式。在Web应用程序上下文中，类型理论提供了一个统一的框架，用于强制执行关键的程序属性，例如不受代码注入攻击和其他常见安全问题的影响。在此基础上构建了对元编程或生成程序的程序的支持，其中应该保证元程序的任何代码输出的关键安全属性。该项目的一个主要推动力是使用元编程将编码模式具体化为可重用的库，从而大大减少了构建新应用程序所需的时间和精力。另一个主要推动力是静态程序分析，其中使用符号执行和自动定理证明来正式验证Web应用程序是否符合声明性安全策略，包括信息流和访问控制。元编程将通过模块局部推理支持基于组件的构造，而静态分析从安全角度确保程序的全局一致性。

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.