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

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

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.