Encoding Security Policies as Refinement Types for Database Applications
- Author(s): Anand, Sourav
- Advisor(s): Polikarpova, Nadia
- et al.
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.