Document Open Access Logo

On the Automated Verification of Web Applications with Embedded SQL

Authors Shachar Itzhaky, Tomer Kotek, Noam Rinetzky, Mooly Sagiv, Orr Tamir, Helmut Veith, Florian Zuleger

PDF
Thumbnail PDF

File

LIPIcs.ICDT.2017.16.pdf
  • Filesize: 0.61 MB
  • 18 pages

Document Identifiers

Author Details

Shachar Itzhaky
Tomer Kotek
Noam Rinetzky
Mooly Sagiv
Orr Tamir
Helmut Veith
Florian Zuleger

Cite As Get BibTex

Shachar Itzhaky, Tomer Kotek, Noam Rinetzky, Mooly Sagiv, Orr Tamir, Helmut Veith, and Florian Zuleger. On the Automated Verification of Web Applications with Embedded SQL. In 20th International Conference on Database Theory (ICDT 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 68, pp. 16:1-16:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.ICDT.2017.16

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.

Subject Classification

Keywords
  • SQL; scripting language; web services; program verification; two-variable fragment of first order logic; decidability; reasoning

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Serge Abiteboul, Richard Hull, and Victor Vianu. Foundations of databases, volume 8. Addison-Wesley Reading, 1995. Google Scholar
  2. Shqiponja Ahmetaj, Diego Calvanese, Magdalena Ortiz, and Mantas Simkus. Managing change in graph-structured data using description logics. In Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence, July 27 -31, 2014, Québec City, Québec, Canada., pages 966-973, 2014. URL: http://www.aaai.org/ocs/index.php/AAAI/AAAI14/paper/view/8238.
  3. Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanović, Tim King, Andrew Reynolds, and Cesare Tinelli. Cvc4. In Proceedings of the 23rd International Conference on Computer Aided Verification, CAV'11, pages 171-177, Berlin, Heidelberg, 2011. Springer-Verlag. URL: http://dl.acm.org/citation.cfm?id=2032305.2032319.
  4. Clark Barrett, Aaron Stump, and Cesare Tinelli. The SMT-LIB standard: Version 2.0. In Aarti Gupta and Daniel Kroening, editors, Satisfiability Modulo Theories (SMT 2010), 2010. URL: http://www.SMT-LIB.org.
  5. Armin Biere. Lingeling, Plingeling, PicoSAT and PrecoSAT at SAT race 2010. FMV report series technical report 10/1, Johannes Kepler University, Linz, Austria, 2010. Google Scholar
  6. Armin Biere, Marijn Heule, and Hans van Maaren. Handbook of satisfiability, volume 185. IOS press, 2009. Google Scholar
  7. Jasmin Christian Blanchette and Tobias Nipkow. Nitpick: A counterexample generator for higher-order logic based on a relational model finder. In International Conference on Interactive Theorem Proving, pages 131-146. Springer, 2010. Google Scholar
  8. Diego Calvanese, Tomer Kotek, Mantas Šimkus, Helmut Veith, and Florian Zuleger. Shape and content. In Integrated Formal Methods, pages 3-17. Springer, 2014. Google Scholar
  9. Diego Calvanese, Magdalena Ortiz, and Mantas Simkus. Verification of evolving graph-structured data under expressive path constraints. In 19th International Conference on Database Theory, ICDT 2016, Bordeaux, France, March 15-18, 2016, pages 15:1-15:19, 2016. URL: http://dx.doi.org/10.4230/LIPIcs.ICDT.2016.15.
  10. Stefano Ceri, Georg Gottlob, and Letizia Tanca. What you always wanted to know about datalog (and never dared to ask). Knowledge and Data Engineering, IEEE Transactions on, 1(1):146-166, 1989. Google Scholar
  11. Edmund M. Clarke, E. Allen Emerson, and A. Prasad Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems (TOPLAS), 8(2):244-263, 1986. Google Scholar
  12. Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. Counterexample-guided abstraction refinement. In Computer Aided Verification, 12th International Conference, 2000, Chicago, IL, USA, July 15-19, 2000, Proceedings, pages 154-169, 2000. URL: http://dx.doi.org/10.1007/10722167_15.
  13. Edgar F Codd. Relational completeness of data base sublanguages. IBM Corporation, 1972. Google Scholar
  14. Leonardo De Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. In Tools and Algorithms for the Construction and Analysis of Systems, pages 337-340. Springer, 2008. Google Scholar
  15. Alin Deutsch, Richard Hull, and Victor Vianu. Automatic verification of database-centric systems. SIGMOD Record, 43(3):5-17, 2014. URL: http://dx.doi.org/10.1145/2694428.2694430.
  16. Alin Deutsch, Monica Marcus, Liying Sui, Victor Vianu, and Dayou Zhou. A verifier for interactive, data-driven web applications. In Proceedings of the 2005 ACM SIGMOD International Conference on Management of Data, SIGMOD'05, pages 539-550, New York, NY, USA, 2005. ACM. URL: http://dx.doi.org/10.1145/1066157.1066219.
  17. Edsger W Dijkstra. Guarded commands, nondeterminacy and formal derivation of programs. Communications of the ACM, 18(8):453-457, 1975. Google Scholar
  18. Michael Felderer, Matthias Büchler, Martin Johns, Achim D Brucker, Ruth Breu, and Alexander Pretschner. Security testing: A survey. Advances in Computers, 2015. Google Scholar
  19. Mary F. Fernández, Daniela Florescu, Alon Y. Levy, and Dan Suciu. Declarative specification of web sites with Strudel. VLDB J., 9(1):38-55, 2000. URL: http://dx.doi.org/10.1007/s007780050082.
  20. Daniela Florescu, Valerie Issarny, Patrick Valduriez, and Khaled Yagoub. Weave: A data-intensive web site management system. In In Proc. of the Conf. on Extending Database Technology (EDBT, 2000. Google Scholar
  21. Erich Grädel, Phokion G Kolaitis, and Moshe Y Vardi. On the decision problem for two-variable first-order logic. Bulletin of symbolic logic, 3(01):53-69, 1997. Google Scholar
  22. Alessandro Grassi and Marco Nenciarini. Panda - the php-based email administrator. http://panda-admin.sourceforge.net/index.php?mode=home, 2007-2015.
  23. Charles A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576-580, 1969. Google Scholar
  24. Ranjit Jhala and Rupak Majumdar. Software model checking. ACM Computing Surveys (CSUR), 41(4):21, 2009. Google Scholar
  25. Laura Kovács and Andrei Voronkov. First-order theorem proving and Vampire. In Computer Aided Verification, pages 1-35. Springer, 2013. Google Scholar
  26. S. Kumaran, P. Nandi, T. Heath, K. Bhaskaran, and R. Das. Adoc-oriented programming. In In Symp. on Applications and the Internet (SAINT), 2003. Google Scholar
  27. Leonid Libkin. Expressive power of SQL. Theoretical Computer Science, 296(3):379-404, 2003. Google Scholar
  28. William Mccune. A davis-putnam program and its application to finite first-order model search: Quasigroup existence problems. Technical report, Argonne National Laboratory, 1994. Google Scholar
  29. Moodle. http://sourceforge.net/projects/moodle/, 2001-2015. Google Scholar
  30. Michael Mortimer. On languages with two variables. Mathematical Logic Quarterly, 21(1):135-140, 1975. Google Scholar
  31. A. Nigam and N. S. Caswell. Business artifacts: An approach to operational specification. IBM Systems Journal, 42, 2003. Google Scholar
  32. Amir Pnueli. The temporal logic of programs. In Foundations of Computer Science, 1977., 18th Annual Symposium on, pages 46-57. IEEE, 1977. Google Scholar
  33. Arend Rensink. Canonical graph shapes. In David Schmidt, editor, Programming Languages and Systems, volume 2986 of Lecture Notes in Computer Science, pages 401-415. Springer Berlin Heidelberg, 2004. URL: http://dx.doi.org/10.1007/978-3-540-24725-8_28.
  34. Alexandre Riazanov and Andrei Voronkov. The design and implementation of Vampire. AI communications, 15(2, 3):91-110, 2002. Google Scholar
  35. Boris Trakhtenbrot. The impossibility of an algorithm for the decidability problem on finite classes. In Proceedings of the USSR Academy of Sciences, volume 70, pages 569-572, 1950. Google Scholar
  36. Grigori S Tseitin. On the complexity of derivation in propositional calculus. In Automation of reasoning, pages 466-483. Springer, 1983. Google Scholar
  37. Hugh E Williams and David Lane. Web database applications with PHP and MySQL. O'Reilly Media, Inc., 2004. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact