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