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

点击翻译按钮获取中文摘要

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.