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框架，并使用它开发一套具有强有力保证的应用程序，从而展示该想法如何在主流框架和语言中广泛采用。