Advertisement

Inductive verification of data model invariants in web applications using first-order logic

  • Ivan Bocić
  • Tevfik Bultan
  • Nicolás RosnerEmail author
Article
  • 12 Downloads

Abstract

Modern software applications store their data in remote cloud servers. Users interact with these applications using web browsers or thin clients running on mobile devices. A key concern for these applications is the correctness of the actions that update the data store, which are triggered by user requests. Considering that modern applications store and manage data for millions (even billions) of users, misuse or loss of user data can have catastrophic consequences. In this paper, we focus on automated discovery of data store bugs in applications that use development frameworks that are RESTful, enforce the Model–View–Controller architecture, and use Object Relational Mapping libraries to manipulate data. We present a formal data model for data stores and data store manipulation in such applications. We have developed a framework for verification of data models via translation to First Order Logic (FOL), followed by automated theorem proving. Due to the undecidability of FOL, this automated approach does not always produce a conclusive answer. We investigate the use of many-sorted logic in data model verification in order to improve the effectiveness of this approach. Many-sorted logic allows us to specify type information explicitly, thus lightening the burden of reasoning about type information during theorem proving. Our experimental results demonstrate that our verification approach is scalable to real-world web applications and is able to detect bugs in them.

Keywords

Data model Automated verification First-order logic Many-sorted logic 

Notes

References

  1. Ahrendt, W., Baar, T., Beckert, B., Bubel, R., Giese, M., Hahnle, R., Menzel, W., Mostowski, W., Roth, A., Schlager, S., Schmitt, P.H.: The KeY tool. Softw. Syst. Model. 4(1), 32–54 (2005)CrossRefGoogle Scholar
  2. Ball, T., Bjørner, N., Gember, A., Itzhaky, S., Karbyshev, A., Sagiv, M., Schapira, M., Valadarsky, A.: Vericon: towards verifying controller programs in software-defined networks. In: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’14), pp. 282–293. ACM, New York (2014)Google Scholar
  3. Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: Proceedings of the 4th International Symposium on Formal Methods for Components and Objects (FMCO 2005), pp. 364–387 (2005)Google Scholar
  4. Blanchette, J.C., Popescu, A., Wand, D., Weidenbach, C.: More SPASS with isabelle—superposition with hard sorts and configurable simplification. In: Interactive Theorem Proving—Third International Conference (ITP 2012), Princeton, NJ, USA, August 13–15, 2012. Proceedings, pp. 345–360 (2012)Google Scholar
  5. Bocic, I.: Data model verification via theorem proving. PhD thesis, University of California, Santa Barbara, Sept. 2016Google Scholar
  6. Bocic, I., Bultan, T.: Inductive verification of data model invariants for web applications. In: 36th International Conference on Software Engineering (ICSE 2014), Hyderabad, India—May 31–June 07, 2014, pp. 620–631 (2014)Google Scholar
  7. Bocic, I., Bultan, T.: Coexecutability for efficient verification of data model updates. In: 37th International Conference on Software Engineering (ICSE 2015) (2015a)Google Scholar
  8. Bocic, I., Bultan, T.: Data model bugs. In: NASA Formal Methods—7th International Symposium, NFM 2015, Pasadena, CA, USA, April 27–29, 2015, Proceedings, pp. 393–399 (2015b)Google Scholar
  9. Bocic, I., Bultan, T.: Efficient data model verification with many-sorted logic. In: 30th IEEE/ACM International Conference on Automated Software Engineering ASE 2015, Lincoln, Nebraska, USA, 9–13 Nov. (2015c)Google Scholar
  10. Bocic, I., Bultan, T.: Symbolic model extraction for web application verification. In: Proceedings of the 39th International Conference on Software Engineering, ICSE 2017, Buenos Aires, Argentina, May 20–28, 2017, pp. 724–734 (2017)Google Scholar
  11. Claessen, K., Lillieström, A., Smallbone, N.: Sort it out with monotonicity—translating between many-sorted and unsorted first-order logic. In: Automated Deduction—CADE-23–23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31–August 5, 2011. Proceedings, pp. 207–221 (2011)Google Scholar
  12. de Moura, L., Bjrner, N.: Efficient e-matching for SMT solvers. In: Automated Deduction—CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17–20, 2007, Proceedings, volume 4603 of Lecture Notes in Computer Science, pp. 183–198. Springer, Berlin (2007)Google Scholar
  13. de Moura, L.M., Bjørner, N.: Z3: an efficient SMT solver. In: Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29–April 6, 2008. Proceedings, pp. 337–340 (2008)Google Scholar
  14. Deutsch, A., Vianu, V.: WAVE: automatic verification of data-driven web services. IEEE Data Eng. Bull. 31(3), 35–39 (2008)Google Scholar
  15. Deutsch, A., Sui, L., Vianu, V., Zhou, D.: A system for specification and verification of interactive, data-driven web applications. In: SIGMOD Conference, pp. 772–774 (2006)Google Scholar
  16. Deutsch, A., Sui, L., Vianu, V.: Specification and verification of data-driven web applications. J. Comput. Syst. Sci. 73(3), 442–474 (2007)MathSciNetCrossRefGoogle Scholar
  17. Dutertre, B., de Moura, L.M.: A fast linear-arithmetic solver for DPLL(T). In: Computer Aided Verification, 18th International Conference, CAV 2006, Seattle, WA, USA, August 17–20, 2006, Proceedings, pp. 81–94 (2006)Google Scholar
  18. Karaca, E.: A collection/list of awesome projects, sites made with Rails, Jan. 2016. https://github.com/ekremkaraca/awesome-rails
  19. Fat Free CRM - Ruby on Rails-based open source CRM platform, Sept. 2013. http://www.fatfreecrm.com
  20. Fielding, R.T.: Architectural styles and the design of network-based software architectures. PhD thesis, University of California, Irvine (2000)Google Scholar
  21. Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for java. In: Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 234–245 (2002)Google Scholar
  22. Frias, M.F., Galeotti, J.P., Pombo, C.L., Aguirre, N.: Dynalloy: upgrading alloy with actions. In: 27th International Conference on Software Engineering (ICSE 2005), 15–21 May 2005, St. Louis, Missouri, USA, pp. 442–451 (2005)Google Scholar
  23. Frias, M.F., Pombo, C.L., Galeotti, J.P., Aguirre, N.: Efficient analysis of DynAlloy specifications. ACM Trans. Softw. Eng. Methodol. 17(1), 4:1–4:34 (2007)CrossRefGoogle Scholar
  24. Galeotti, J.P., Frias, M.F.: Dynalloy as a formal method for the analysis of java programs. In: Software Engineering Techniques: Design for Quality, SET 2006, October 17–20, 2006, Warsaw, Poland, pp. 249–260 (2006)Google Scholar
  25. Goguen, J.A., Meseguer, J.: Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theor. Comput. Sci. 105(2), 217–273 (1992)MathSciNetCrossRefGoogle Scholar
  26. Jackson, D.: Alloy: a lightweight object modelling notation. ACM Trans. Softw. Eng. Methodol. (TOSEM 2002) 11(2), 256–290 (2002)CrossRefGoogle Scholar
  27. Jackson, D.: Software Abstractions: Logic, Language, and Analysis. The MIT Press, Cambridge (2006)Google Scholar
  28. Kahsai, T., Rümmer, P., Sanchez, H., Schäf, M.: Jayhorn: a framework for verifying java programs. In: Computer Aided Verification—28th International Conference, CAV 2016, Toronto, ON, Canada, July 17–23, 2016, Proceedings, Part I, pp. 352–358 (2016)Google Scholar
  29. Kovács, L., Voronkov, A.: First-order theorem proving and vampire. In: Proceedings of the 25th International Conference on Computer Aided Verification (CAV 2013), Saint Petersburg, Russia, July 13–19, 2013, pp. 1–35 (2013)Google Scholar
  30. Krasner, G.E., Pope, S.T.: A cookbook for using the model-view controller user interface paradigm in Smalltalk-80. J. Object Oriented Program. 1(3), 26–49 (1988)Google Scholar
  31. Kuncak, V., Lam, P., Zee, K., Rinard, M.C.: Modular pluggable analyses for data structure consistency. IEEE Trans. Softw. Eng. 32(12), 988–1005 (2006)CrossRefGoogle Scholar
  32. Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Proceedings of the 16th International Conference on Logic Programming, Artificial Intelligence, and Reasoning (LPAR), pp. 348–370 (2010)Google Scholar
  33. Lesani, M., Millstein, T.D., Palsberg, J.: Automatic atomicity verification for clients of concurrent data structures. In: Computer Aided Verification—26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18–22, 2014. Proceedings, pp. 550–567 (2014)Google Scholar
  34. Near, J.P., Jackson, D.: Rubicon: bounded verification of web applications. In: Proceedings of the ACM SIGSOFT 20th International Symposium on Foundations of Software Engineering (FSE 2012), pp. 60:1–60:11 (2012)Google Scholar
  35. Nijjar, J., Bultan, T.: Bounded verification of Ruby on Rails data models. In: Proceedings of the 20th International Symposium on Software Testing and Analysis (ISSTA 2011), pp. 67–77 (2011)Google Scholar
  36. Nijjar, J., Bultan, T.: Unbounded data model verification using SMT solvers. In: Proceedings of the 27th IEEE/ACM International Conference on Automated Software Engineering (ASE 2012), pp. 210–219 (2012)Google Scholar
  37. Nijjar, J., Bocić, I., Bultan, T.: An integrated data model verifier with property templates. In: Proceedings of the ICSE Workshop on Formal Methods in Software Engineering (FormaliSE 2013), pp. 23–35. IEEE (2013)Google Scholar
  38. Object Management Group: UML Specification. http://www.omg.org
  39. Open Source Rails, Jan. 2016. http://www.opensourcerails.com
  40. Pelletier, F., Sutcliffe, G., Suttner, C.: The development of CASC. AI Commun. 15(2–3), 79–90 (2002)zbMATHGoogle Scholar
  41. Quine, W.V.: Quantification and the empty domain. J. Symb. Log. 19(3), 177–179 (1954)MathSciNetCrossRefGoogle Scholar
  42. Richters, M., Gogolla, M.: Validating UML models and OCL constraints. In: Proceedings of the 3rd International Conference on Unified Modeling Language (UML 2000), LNCS 1939 (2000)Google Scholar
  43. Ruby on Rails, Feb. 2013. http://rubyonrails.org
  44. SimilarTech: Website technology detection and tracking, Oct. 2018. https://similartech.com/
  45. SMT-LIB, 2016. http://www.smtlib.org/
  46. Spring Framework | SpringSource.org, Feb. 2013. http://www.springsource.org
  47. Stickel, M.E., Waldinger, R.J., Lowry, M.R., Pressburger, T., Underwood, I.: Deductive composition of astronomical software from subroutine libraries. In: Automated Deduction—CADE-12, 12th International Conference on Automated Deduction, Nancy, France, June 26–July 1, 1994, Proceedings, pp. 341–355 (1994)Google Scholar
  48. Sutcliffe, G., Suttner, C.: The state of CASC. AI Commun. 19(1), 35–48 (2006)MathSciNetzbMATHGoogle Scholar
  49. Sutcliffe, G., Suttner, C.B., Yemenis, T.: The TPTP problem library. In: Automated Deduction—CADE-12, 12th International Conference on Automated Deduction, Nancy, France, June 26–July 1, 1994, Proceedings, pp. 252–266 (1994)Google Scholar
  50. Sutcliffe, G., Schulz, S., Claessen, K., Baumgartner, P.: The TPTP typed first-order form with arithmetic. In: Logic for Programming, Artificial Intelligence, and Reasoning - 18th International Conference, LPAR-18, Mérida, Venezuela, March 11–15, 2012. Proceedings, pp. 406–419 (2012)Google Scholar
  51. The Web framework for perfectionists with deadlines | Django, Feb. 2013. http://www.djangoproject.com
  52. Tracks, Sept. 2013. http://getontracks.org
  53. Warmer, J., Kleppe, A.: The Object Constraint Language: Precise Modeling with UML. Addison-Wesley, Boston (1998)Google Scholar
  54. Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Proceedings of the 22nd International Conference on Automated Deduction (CADE 2009), LNCS 5663, pp. 140–145 (2009)Google Scholar
  55. Weidenbach, C.: SPASS input syntax version 1.5, 2016. http://www.spass-prover.org/download/binaries/spass-input-syntax15.pdf
  56. Zee, K., Kuncak, V., Rinard, M.: Full functional verification of linked data structures. In: Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’08), pp. 349–361. ACM, New York, NY (2008)Google Scholar

Copyright information

© Springer Science+Business Media, LLC, part of Springer Nature 2018

Authors and Affiliations

  1. 1.Google, Inc.Mountain ViewUSA
  2. 2.University of CaliforniaSanta BarbaraUSA

Personalised recommendations