Securing Database-Backed Web Applications Through Lightweight, Automated Verification
We present a solution for automated verification of expressive properties in database-backed applications. We demonstrate how to use a
static, type-based approach for fully automated verification across application and database code, with lightweight annotations. Using our
solution, programmers specify high-level predicates over database schemas and can then rely on the type-checker to detect violations. We
show, perhaps surprisingly, how to combine existing type-based techniques with new system design approaches to support fully automated
verification of expressive properties, including high-level information flow security predicates. The key insight is to design an
object-relational mapping (ORM) that supports a uniform model of application-database code for verification purposes.