ICFP 2021
Sun 22 - Sat 28 August 2021
Mon 23 Aug 2021 03:30 - 03:52 at HIW - Applications and Closing Chair(s): Edsko de Vries

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.

Mon 23 Aug

Displayed time zone: Seoul change

03:30 - 05:00
Applications and ClosingHIW at HIW
Chair(s): Edsko de Vries Well-Typed LLP
Securing Web-Applications with A Refinement Typed ORM
Nico Lehmann University of California, San Diego, Rose Kunkel University of California, San Diego, Niki Vazou IMDEA Software Institute, Nadia Polikarpova University of California at San Diego, Deian Stefan University of California at San Diego, USA, Ranjit Jhala University of California at San Diego
Generics for Hardware: Adding Haskell-inspired Generics to Bluespec
Ningning Xie University of Toronto