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

SHF：小型：利用 Ur/Web 编程语言中的一流 SQL 支持

• 批准号: 1217501
• 负责人: Adam Chlipala
• 金额: $ 50万
• 依托单位: Massachusetts Institute of Technology
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2012
• 资助国家: 美国
• 起止时间: 2012-09-01 至 2016-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1217501&HistoricalAwards=false
• 关键词: SHF; Small; Capitalizing; First; Class

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.

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