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 implement STORM as a plain Haskell library, on top of the persistent ORM, allowing the LiquidHaskell type-checker plugin to verify security policies at each build.

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 need 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.