Title: Refinement Types for Secure Web Applications

Speaker: Ranjit Jhala    (bio) (bio)

Ranjit Jhala is a Professor of Computer Science Engineering in the Jacobs School of Engineering at the University of California, San Diego. His research interest lies in Programming Languages and Software Engineering, specifically, in techniques for building reliable computer systems. His work draws from, combines and contributes to the areas of Type Systems, Model Checking, Program Analysis and Automated Deduction.

When: Tuesday, 07 December 2021 at 1900 hrs (IST)    

Abstract:
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.