STORM - Refinement Types for Secure Web Applications

Explore a conference talk on STORM, a web framework that enables developers to build MVC applications with compile-time enforcement of centrally specified data-dependent security policies. Learn how STORM utilizes a Security Typed ORM to refine abstractions in each layer of the MVC API, ensuring security through logical assertions. Discover the framework's ability to specify diverse policies while centralizing trusted code to less than 1% of the application, and how it statically enforces security with minimal type annotation overhead and no runtime cost. Gain insights into the formally verified reference implementation using the Labeled IO (LIO) IFC framework, and examine case studies and end-to-end applications demonstrating STORM's effectiveness in web application security.