Symbolic execution of stored procedures in database management systems

ABSTRACT

Stored procedures in database management systems are often used to implement complex business logic. Correctness of these procedures is critical for correct working of the system. However, testing them remains difficult due to many possible states of data and database constraints. This leads to mostly manual testing. Newer tools offer automated execution for unit testing of stored procedures but the test cases are still written manually.

In this paper, we propose a novel approach of using dynamic symbolic execution to automatically generate test cases and corresponding database states for stored procedures. We treat values in database tables as symbolic, model the constraints on data imposed by the schema and by the SQL statements executed by the stored procedure. We use an SMT solver to find values that will drive the stored procedure on a particular execution path.

We instrument the internal execution plans generated by PostgreSQL database management system to extract constraints and use the Z3 SMT solver to generate test cases consisting of table data and procedure inputs. Our evaluation using stored procedures from a large business application shows that this technique can uncover bugs that lead to schema constraint violations and user defined exceptions.

References

1. C. Barrett and C. Tinelli. CVC3. In Proc. 19th International Conference on Computer Aided Verification (CAV), pages 298–302, 2007.
2. C. Binnig, D. Kossmann, and E. Lo. Reverse query processing. In IEEE 23rd International Conference on Data Engineering (ICDE), pages 506–515, 2007.
3. W. R. Bush, J. D. Pincus, and D. J. Sielaff. A Static Analyzer for Finding Dynamic Programming Errors. Software Practice Experience, 30(7):775–802, June 2000.
4. C. Cadar, D. Dunbar, and D. R. Engler. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In Proc. 8th Symposium on Operating Systems Design and Implementation (OSDI), pages 209–224, 2008.
5. C. Cadar and D. Engler. Execution Generated Test Cases: How to make systems code crash itself. In Proc. International SPIN Workshop on Model Checking of Software, pages 2–23, 2005.
6. C. Cadar, V. Ganesh, P. M. Pawlowski, D. L. Dill, and D. R. Engler. EXE: Automatically Generating Inputs of Death. In Proc. 13th Conference on Computer and Communications Security (CCS), pages 322–335, 2006.
7. L. A. Clarke. A System to Generate Test Data and Symbolically Execute Programs. IEEE Transactions on Software Engineering (TSE), 2(3):215–222, May 1976.
8. L. A. Clarke. Test Data Generation and Symbolic Execution of Programs as an aid to Program Validation. PhD thesis, University of Colorado at Boulder, 1976.
9. C. De La Riva, M. J. Suárez-Cabal, and J. Tuya. Constraint-based test database generation for SQL queries. In Proceedings of the 5th Workshop on Automation of Software Testing, pages 67–74, 2010.
10. L. de Moura and N. Bjørner. Z3: An Efficient SMT Solver. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 337–340, 2008.
11. Y. Deng, P. Frankl, and D. Chays. Testing database transactions with AGENDA. In Proceedings of the 27th international conference on Software engineering, pages 78–87, 2005.
12. B. Elkarablieh, I. Garcia, Y. L. Suen, and S. Khurshid. Assertion-based Repair of Complex Data Structures. In Proc. 22nd International Conference on Automated Software Engineering (ASE), pages 64–73, 2007.
13. M. Emmi, R. Majumdar, and K. Sen. Dynamic test input generation for database applications. In Proceedings of the 2007 International Symposium on Software Testing and Analysis, pages 151–162, 2007.
14. P. Godefroid. Compositional Dynamic Test Generation. In Proc. 34th Symposium on Principles of Programming Languages (POPL), pages 47–54, 2007.
15. P. Godefroid, N. Klarlund, and K. Sen. DART: Directed Automated Random Testing. In Proc. 2005 Conference on Programming Languages Design and Implementation (PLDI), pages 213–223, 2005.
16. D. Jackson. Alloy: a lightweight object modelling notation. ACM Transactions on Software Engineering and Methodology (TOSEM), 11(2):256–290, 2002.
17. S. A. Khalek and S. Khurshid. Systematic testing of database engines using a relational constraint solver. In Proceedings of the Fourth IEEE International Conference on Software Testing, Verification and Validation (ICST), pages 50–59, 2011.
18. S. Khurshid, C. S. Pasareanu, and W. Visser. Generalized Symbolic Execution for Model Checking and Testing. In Proc. 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 553–568, 2003.
19. J. C. King. Symbolic Execution and Program Testing. Communications ACM, 19(7):385–394, July 1976.
20. C. Li and C. Csallner. Dynamic symbolic database application testing. In Proceedings of the Third International Workshop on Testing Database Systems (DBTest), 2010.
21. M. Marcozzi, W. Vanhoof, and J.-L. Hainaut. A relational symbolic execution algorithm for constraint-based testing of database programs. In IEEE 13th International Working Conference on Source Code Analysis and Manipulation (SCAM), pages 179–188, 2013.
22. M. Marcozzi, W. Vanhoof, and J.-L. Hainaut. Towards testing of full-scale SQL applications using relational symbolic execution. In Proceedings of the 6th International Workshop on Constraints in Software Testing, Verification, and Analysis, pages 12–17, 2014.
23. K. Pan, X. Wu, and T. Xie. Database state generation via dynamic symbolic execution for coverage criteria. In Proceedings of the Fourth International Workshop on Testing Database Systems, page 4, 2011.
24. S. Person, G. Yang, N. Rungta, and S. Khurshid. Directed Incremental Symbolic Execution. In Proc. 2011 Conference on Programming Languages Design and Implementation (PLDI), pages 504–515, 2011.
25. D. A. Ramos and D. R. Engler. Practical, Low-Effort Equivalence Verification of Real Code. In Proc. 23rd International Conference on Computer Aided Verification (CAV), pages 669–685, 2011.
26. K. Sen, D. Marinov, and G. Agha. CUTE: A Concolic Unit Testing Engine for C. In Proc. 5th joint meeting of the European Software Engineering Conference and Symposium on Foundations of Software Engineering (ESEC/FSE), pages 263–272, 2005.
27. C. Seo, S. Malek, and N. Medvidovic. Component-Level Energy Consumption Estimation for Distributed Java-Based Software Systems. In Proc. 11th International Symposium on Component-Based Software Engineering, pages 97–113, 2008.
28. J. H. Siddiqui and S. Khurshid. ParSym: Parallel Symbolic Execution. In Proc. 2nd International Conference on Software Technology and Engineering (ICSTE), pages V1: 405–409, 2010.
29. J. H. Siddiqui and S. Khurshid. Scaling Symbolic Execution using Ranged Analysis. In Proc. 27th Annual Conference on Object Oriented Programming Systems, Languages, and Applications (OOPSLA), 2012.
30. J. H. Siddiqui and S. Khurshid. Staged Symbolic Execution. In Proc. 27th Symposium on Applied Computing (SAC): Software Verification and Testing Track (SVT), 2012.
31. N. Sörensson and N. Een. An Extensible SAT-solver. In Proc. 6th International Conference on Theory and Applications of Satisfiability Testing (SAT), pages 502–518, 2003.
32. M. Staats and C. Pˇ asˇ areanu. Parallel Symbolic Execution for Structural Test Generation. In Proc. 19th International Symposium on Software Testing and Analysis (ISSTA), pages 183–194, 2010.
33. J. Tuya, M. J. Suárez-Cabal, and C. de la Riva. Full predicate coverage for testing SQL database queries. Journal of Software Testing, Verification and Reliability, 20(3):237–288, 2010.
34. M. Veanes, P. Grigorenko, P. De Halleux, and N. Tillmann. Symbolic query exploration. In Formal Methods and Software Engineering, pages 49–68. Springer, 2009.
35. K. Wei, M. Muthuprasanna, and S. Kothari. Preventing sql injection attacks in stored procedures. In Proceedings of the Australian Software Engineering Conference (ASWEC), pages 191–198, 2006.
36. G. Yang, C. S. Păsăreanu, and S. Khurshid. Memoized Symbolic Execution. In Proc. 2012 International Symposium on Software Testing and Analysis (ISSTA), ISSTA 2012, pages 144–154, 2012.

Index Terms

• Software and its engineering

  • Software creation and management

    • Software verification and validation

      • Software defect analysis

        • Software testing and debugging