UC San Diego

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.