SHF: Small: Refinement Types For Verified Web Frameworks and Applications

SHF：小型：经过验证的 Web 框架和应用程序的细化类型

• 批准号: 1422471
• 负责人: Ranjit Jhala
• 金额: $ 50万
• 依托单位: University of California-San Diego
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2014
• 资助国家: 美国
• 起止时间: 2014-09-01 至 2018-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1422471&HistoricalAwards=false
• 关键词: SHF; Small; Refinement; Types; Verified

Title: SHF: Small: Refinement Types For Verified Web Frameworks and ApplicationsWeb applications play a crucial role in every aspect of our lives, including banking, commerce, education and healthcare and travel. Despite their importance and ubiquity, they remain notoriously hard to design, develop and deploy as they span several tiers and languages: an HTML/JavaScript client that runs on users' browsers, a central server that implements the application's logic in the "cloud" and a database that stores persistent user data. The goal of this research is to build upon recent advances in SMT-based software verification to develop reliable and secure web frameworks. The intellectual merits of this research are new techniques for specifying and verifying multi-lingual systems spanning databases, scripting languages and service protocols, which are essential ingredients of large software systems. Thus, the project's broader significance and importance is that it will lower the cost of constructing robust web applications, with strong guarantees about the protection of sensitive data about the users' health, finances and other personal information.To mitigate the impedance mismatch across tiers, developers use web frameworks which have simplified the construction of web applications. However, reliability and security concerns still cut across multiple tiers and languages, making them hard to achieve. This research will use refinement types to specify and verify properties for frameworks and end-to-end safety and security properties for applications. In particular, it will build on the refinement type system of LiquidHaskell, developed in preliminary research, to verify existing frameworks like Haskell's popular SNAP framework, and use it to develop a suite of applications with strong guarantees, thereby showing how the idea can be widely adopted in mainstream frameworks and languages.

标题：SHF：小型：经过验证的 Web 框架和应用程序的细化类型 Web 应用程序在我们生活的各个方面发挥着至关重要的作用，包括银行、商业、教育、医疗保健和旅行。尽管它们很重要且无处不在，但它们仍然很难设计、开发和部署，因为它们跨越多个层和语言：在用户浏览器上运行的 HTML/JavaScript 客户端、在“云”中实现应用程序逻辑的中央服务器以及存储持久用户数据的数据库。本研究的目标是利用基于 SMT 的软件验证的最新进展来开发可靠且安全的 Web 框架。这项研究的智力优点是指定和验证跨数据库、脚本语言和服务协议的多语言系统的新技术，这些是大型软件系统的基本组成部分。因此，该项目更广泛的意义和重要性在于，它将降低构建强大的 Web 应用程序的成本，并为保护有关用户健康、财务和其他个人信息的敏感数据提供强有力的保证。为了减轻跨层的阻抗不匹配，开发人员使用 Web 框架简化了 Web 应用程序的构建。然而，可靠性和安全性问题仍然跨越多个层次和语言，使得它们难以实现。这项研究将使用细化类型来指定和验证框架的属性以及应用程序的端到端安全和保障属性。特别是，它将建立在LiquidHaskell前期研究的细化类型系统的基础上，验证现有的框架，如Haskell流行的SNAP框架，并用它来开发一套有强大保障的应用程序，从而展示该想法如何广泛推广被主流框架和语言采用。