Verified Software Frameworks / Ranjit Jhala
Web applications play a crucial role in every aspect of our lives. Despite their importance and ubiquity, they remain notoriously hard to design, develop and deploy, as they span several tiers: an HTML/JavaScript client that runs in browsers, a central server that implements the application’s logic and a database stores persistent user data. To mitigate the impedance mismatch across tiers, developers use web frameworks like Express (JS), RUBY ON RAILS (Ruby), DJANGO (Python), STRUTS and PLAY (Java/Scala), and SNAP and YESOD (Haskell). Though frameworks have simplified the construction of web applications, information still must flow across, and hence reliability and security concerns cut across, multiple tiers and languages, making them hard to achieve. We aim to build upon recent advances in software verification to develop reliable and secure web frameworks and applications. Our solution will be:(1) modular: enabling the specification of rich interfaces that suitably capture the high-level semantics of the frameworkâs API and the verification of the framework itself against the interfaces, (2) expressive: providing compile time guarantees of critical high-level application specific properties for applications constructed using the framework API, (3) incremental: enabling adoption by being applicable to existing mainstream frameworks and languages, without requiring the creation of a new research language or framework from scratch.