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应用程序符合声明性安全策略，包括信息流和访问控制。元编程将支持基于组件的建设与模块本地推理，而静态分析，从安全的角度确保程序的全局一致性。