Skip to main content
Open Access Publications from the University of California

UC San Diego

UC San Diego Electronic Theses and Dissertations bannerUC San Diego

Encoding Security Policies as Refinement Types for Database Applications


This thesis presents an encoding of security policies for database-backed web applications

as refinement types. We add refinement types to the function calls which interact directly with

the database in order to attach a label to the output data. Any computation over the data retrieved

from the database also requires computing a new label as per the refinement types added to the

computation to enforce the security policies. The label on the data is verified against the security

policies at the point where data is being displayed to a viewer. The refinement types are verified

statically with LiquidHaskell which allows programmers to reason about the enforcement of the

security policies across the whole application.

Main Content
For improved accessibility of PDF content, download the file to your device.
Current View