On the automated verification of web applications with embedded SQL

TL;DR

This paper presents a formal method for automated verification of web applications with embedded SQL, connecting database theory to program analysis, and demonstrates its practical application through three case studies.

Contribution

Introduces a decidable SQL fragment and a decision procedure that enable integration of database query analysis into program verification tools.

Findings

Decidable SQL fragment captures query behavior in case studies.

Automated verification method applied successfully to real web systems.

Practical decision procedure facilitates analysis of embedded SQL in web applications.

Abstract

A large number of web applications is based on a relational database together with a program, typically a script, that enables the user to interact with the database through embedded SQL queries and commands. In this paper, we introduce a method for formal automated verification of such systems which connects database theory to mainstream program analysis. We identify a fragment of SQL which captures the behavior of the queries in our case studies, is algorithmically decidable, and facilitates the construction of weakest preconditions. Thus, we can integrate the analysis of SQL queries into a program analysis tool chain. To this end, we implement a new decision procedure for the SQL fragment that we introduce. We demonstrate practical applicability of our results with three case studies, a web administrator, a simple firewall, and a conference management system.