License: 
Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ICDT.2017.16
URN: urn:nbn:de:0030-drops-70509
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2017/7050/
Itzhaky, Shachar ;
Kotek, Tomer ;
Rinetzky, Noam ;
Sagiv, Mooly ;
Tamir, Orr ;
Veith, Helmut ;
Zuleger, Florian
On the Automated Verification of Web Applications with Embedded SQL
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.
BibTeX - Entry
@InProceedings{itzhaky_et_al:LIPIcs:2017:7050,
author = {Shachar Itzhaky and Tomer Kotek and Noam Rinetzky and Mooly Sagiv and Orr Tamir and Helmut Veith and Florian Zuleger},
title = {{On the Automated Verification of Web Applications with Embedded SQL}},
booktitle = {20th International Conference on Database Theory (ICDT 2017)},
pages = {16:1--16:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-024-8},
ISSN = {1868-8969},
year = {2017},
volume = {68},
editor = {Michael Benedikt and Giorgio Orsi},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2017/7050},
URN = {urn:nbn:de:0030-drops-70509},
doi = {10.4230/LIPIcs.ICDT.2017.16},
annote = {Keywords: SQL; scripting language; web services; program verification; two-variable fragment of first order logic; decidability; reasoning}
}
|
Keywords: |
|
SQL; scripting language; web services; program verification; two-variable fragment of first order logic; decidability; reasoning |
|
Collection: |
|
20th International Conference on Database Theory (ICDT 2017) |
|
Issue Date: |
|
2017 |
|
Date of publication: |
|
17.03.2017 |
