Title: Refinement Types for Secure Web Applications
We present STORM, a new web framework that lets developers build model-view-controller (MVC) applications, with compile-time enforcement of security policies.
With STORM, users specify all security policies in a declarative language, alongside the data model i.e. the description of the application database schema. Policies are logical assertions that describe which users are allowed to view, insert, or update particular rows and columns of each table in the database. STORM enforces these policies at compile-time by using refinement types to constrain STORM's API with logical assertions that describe the data produced and consumed by the underlying operation and the users allowed access to that data.
We evaluate STORM in three ways. First, we show that our centralized policy specification approach is expressive enough to describe, often more naturally, a large suite of policies from the literature. Second, we use STORM to write statically verified implementations of several case studies from the literature, including those that had previously only been amenable to dynamic policy enforcement. We show the verification effort is modest: the programmer needs to write 1 line of refinement type signatures per 20-30 lines of code (LOC). Third, we use STORM to build and deploy two new end-to-end web applications for collaborative text editing and video-based social interaction, that have been used at our university and at several academic workshops, respectively. We demonstrate that STORM distills the code that the developer has to get right down to compact, auditable policies (under 70 LOC) that comprise under 1% of the application.