Skip to main content
SpringerLink
Log in

Lifting String Analysis Domains

  • Chapter
  • First Online:
Challenges of Software Verification

Part of the book series: Intelligent Systems Reference Library ((ISRL,volume 238))

  • 170 Accesses

Abstract

Strings are characterized by properties that either refer to their content (e.g., the set of contained characters) and to their shape (e.g., the character position and the length of the strings). In this paper, we present a general framework providing a systematic lifting of string domains through a segmentation abstraction, yielding to a more accurate representation of strings without major impact on efficiency of the analysis. The proposed operator exploits the abstraction functor introduced by Cousot, Cousot and Logozzo for a fully parametric array representation, in the string scenario.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 129.00
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Hardcover Book
USD 169.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Amadini, R., Gange, G., Gauthier, F., Jordan, A., Schachte, P., Søndergaard, H., Stuckey, P.J., Zhang, C.: Reference abstract domains and applications to string analysis. Fundam. Informaticae 158(4), 297–326 (2018). https://doi.org/10.3233/FI-2018-1650

    Article  MathSciNet  MATH  Google Scholar 

  2. Amadini, R., Jordan, A., Gange, G., Gauthier, F., Schachte, P., Søndergaard, H., Stuckey, P.J., Zhang, C.: Combining string abstract domains for javascript analysis: An evaluation. In: A. Legay, T. Margaria (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part I, Lecture Notes in Computer Science, vol. 10205, pp. 41–57 (2017). https://doi.org/10.1007/978-3-662-54577-5_3

  3. Arceri, V., Mastroeni, I.: Static program analysis for string manipulation languages. In: A. Lisitsa, A. Nemytykh (eds.) Proceedings Seventh International Workshop on Verification and Program Transformation, Genova, Italy, 2nd April 2019, Electronic Proceedings in Theoretical Computer Science, vol. 299, pp. 19–33. Open Publishing Association

    Google Scholar 

  4. Arceri, V., Mastroeni, I.: An automata-based abstract semantics for string manipulation languages. In: A. Lisitsa, A.P. Nemytykh (eds.) Proceedings Seventh International Workshop on Verification and Program Transformation, VPT@Programming 2019, Genova, Italy, 2nd April 2019, EPTCS, vol. 299, pp. 19–33 (2019). https://doi.org/10.4204/EPTCS.299.5

  5. Arceri, V., Olliaro, M., Cortesi, A., Mastroeni, I.: Completeness of abstract domains for string analysis of javascript programs. In: R.M. Hierons, M. Mosbah (eds.) Theoretical Aspects of Computing - ICTAC 2019 - 16th International Colloquium, Hammamet, Tunisia, October 31 - November 4, 2019, Proceedings, Lecture Notes in Computer Science, vol. 11884, pp. 255–272. Springer (2019). 10.1007/978-3-030-32505-3_15

    Google Scholar 

  6. Codish, M., Mulkers, A., Bruynooghe, M., de la Banda, M.J.G., Hermenegildo, M.V.: Improving abstract interpretations by combining domains. ACM Trans. Program. Lang. Syst. 17(1), 28–44 (1995). https://doi.org/10.1145/200994.200998

    Article  Google Scholar 

  7. Cortesi, A.: Widening operators for abstract interpretation. In: A. Cerone, S. Gruner (eds.) Sixth IEEE International Conference on Software Engineering and Formal Methods, SEFM 2008, Cape Town, South Africa, 10-14 November 2008, pp. 31–40. IEEE Computer Society (2008). https://doi.org/10.1109/SEFM.2008.20

  8. Cortesi, A., Charlier, B.L., Hentenryck, P.V.: Combinations of abstract domains for logic programming. In: H. Boehm, B. Lang, D.M. Yellin (eds.) Conference Record of POPL’94: 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Portland, Oregon, USA, January 17-21, 1994, pp. 227–239. ACM Press (1994). https://doi.org/10.1145/174675.177880

  9. Cortesi, A., Charlier, B.L., Hentenryck, P.V.: Combinations of abstract domains for logic programming: open product and generic pattern construction. Sci. Comput. Program. 38(1–3), 27–71 (2000). https://doi.org/10.1016/S0167-6423(99)00045-3

    Article  MathSciNet  MATH  Google Scholar 

  10. Cortesi, A., Costantini, G., Ferrara, P.: A survey on product operators in abstract interpretation. In: A. Banerjee, O. Danvy, K. Doh, J. Hatcliff (eds.) Semantics, Abstract Interpretation, and Reasoning about Programs: Essays Dedicated to David A. Schmidt on the Occasion of his Sixtieth Birthday, Manhattan, Kansas, USA, 19-20th September 2013, EPTCS, vol. 129, pp. 325–336 (2013). https://doi.org/10.4204/EPTCS.129.19

  11. Cortesi, A., Lauko, H., Olliaro, M., Rockai, P.: String abstraction for model checking of C programs. In: F. Biondi, T. Given-Wilson, A. Legay (eds.) Model Checking Software - 26th International Symposium, SPIN 2019, Beijing, China, July 15-16, 2019, Proceedings, Lecture Notes in Computer Science, vol. 11636, pp. 74–93. Springer (2019). https://doi.org/10.1007/978-3-030-30923-7_5

  12. Cortesi, A., Olliaro, M.: M-string segmentation: A refined abstract domain for string analysis in C programs. In: J. Pang, C. Zhang, J. He, J. Weng (eds.) 2018 International Symposium on Theoretical Aspects of Software Engineering, TASE 2018, Guangzhou, China, August 29-31, 2018, pp. 1–8. IEEE Computer Society (2018). https://doi.org/10.1109/TASE.2018.00009

  13. Costantini, G., Ferrara, P., Cortesi, A.: A suite of abstract domains for static analysis of string values. Softw. Pract. Exp. 45(2), 245–287 (2015). https://doi.org/10.1002/spe.2218

    Article  Google Scholar 

  14. Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: R.M. Graham, M.A. Harrison, R. Sethi (eds.) Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977, pp. 238–252. ACM (1977). https://doi.org/10.1145/512950.512973

  15. Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: A.V. Aho, S.N. Zilles, B.K. Rosen (eds.) Conference Record of the Sixth Annual ACM Symposium on Principles of Programming Languages, San Antonio, Texas, USA, January 1979, pp. 269–282. ACM Press (1979). https://doi.org/10.1145/567752.567778

  16. Cousot, P., Cousot, R.: Abstract interpretation and application to logic programs. J. Log. Program. 13(2 &3), 103–179 (1992). https://doi.org/10.1016/0743-1066(92)90030-7

    Article  MathSciNet  MATH  Google Scholar 

  17. Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: The astreé analyzer. In: Programming Languages and Systems, 14th European Symposium on Programming,ESOP 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005, Proceedings, Lecture Notes in Computer Science, vol. 3444, pp. 21–30. Springer (2005). https://doi.org/10.1007/978-3-540-31987-0_3

  18. Cousot, P., Cousot, R., Logozzo, F.: A parametric segmentation functor for fully automatic and scalable array content analysis. In: T. Ball, M. Sagiv (eds.) Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011, pp. 105–118. ACM (2011). https://doi.org/10.1145/1926385.1926399

  19. Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: A.V. Aho, S.N. Zilles, T.G. Szymanski (eds.) Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, Tucson, Arizona, USA, January 1978, pp. 84–96. ACM Press (1978). https://doi.org/10.1145/512760.512770

  20. Filé, G., Giacobazzi, R., Ranzato, F.: A unifying view of abstract domain design. ACM Comput. Surv. 28(2), 333–336 (1996). https://doi.org/10.1145/234528.234742

    Article  Google Scholar 

  21. Giacobazzi, R., Ranzato, F.: Functional dependencies and moore-set completions of abstract interpretations and semantics. In: J.W. Lloyd (ed.) Logic Programming, Proceedings of the 1995 International Symposium, Portland, Oregon, USA, December 4-7, 1995, pp. 321–335. MIT Press (1995)

    Google Scholar 

  22. Giacobazzi, R., Ranzato, F.: Refining and compressing abstract domains. In: P. Degano, R. Gorrieri, A. Marchetti-Spaccamela (eds.) Automata, Languages and Programming, 24th International Colloquium, ICALP’97, Bologna, Italy, 7-11 July 1997, Proceedings, Lecture Notes in Computer Science, vol. 1256, pp. 771–781. Springer (1997). https://doi.org/10.1007/3-540-63165-8_230

  23. Giacobazzi, R., Ranzato, F., Scozzari, F.: Making abstract interpretations complete. J. ACM 47(2), 361–416 (2000). https://doi.org/10.1145/333979.333989

    Article  MathSciNet  MATH  Google Scholar 

  24. Gould, C., Su, Z., Devanbu, P.T.: JDBC checker: A static analysis tool for SQL/JDBC applications. In: A. Finkelstein, J. Estublier, D.S. Rosenblum (eds.) 26th International Conference on Software Engineering (ICSE 2004), 23-28 May 2004, Edinburgh, United Kingdom, pp. 697–698. IEEE Computer Society (2004). https://doi.org/10.1109/ICSE.2004.1317494

  25. Granger, P.: Improving the Results of Static Analyses of Programs by Local Decreasing Iterations. In: Shyamasundar R. (eds) Foundations of Software Technology and Theoretical Computer Science. FSTTCS 1992. Lecture Notes in Computer Science, vol 652. Springer, Berlin, Heidelberg (1992)

    Google Scholar 

  26. Gulwani, S., Tiwari, A.: Combining abstract interpreters. In: M.I. Schwartzbach, T. Ball (eds.) Proceedings of the ACM SIGPLAN 2006 Conference on Programming Language Design and Implementation, Ottawa, Ontario, Canada, June 11-14, 2006, pp. 376–386. ACM (2006). https://doi.org/10.1145/1133981.1134026

  27. Jana, A., Halder, R., Kalahasti, A., Ganni, S., Cortesi, A.: Extending abstract interpretation to dependency analysis of database applications. IEEE Trans. Software Eng. 46(5), 463–494 (2020). https://doi.org/10.1109/TSE.2018.2861707

    Article  Google Scholar 

  28. Jensen, S.H., Møller, A., Thiemann, P.: Type analysis for javascript. In: J. Palsberg, Z. Su (eds.) Static Analysis, 16th International Symposium, SAS 2009, Los Angeles, CA, USA, August 9-11, 2009. Proceedings, Lecture Notes in Computer Science, vol. 5673, pp. 238–255. Springer (2009). https://doi.org/10.1007/978-3-642-03237-0_17

  29. Kim, S., Chin, W., Park, J., Kim, J., Ryu, S.: Inferring grammatical summaries of string values. In: J. Garrigue (ed.) Programming Languages and Systems - 12th Asian Symposium, APLAS 2014, Singapore, November 17-19, 2014, Proceedings, Lecture Notes in Computer Science, vol. 8858, pp. 372–391. Springer (2014). https://doi.org/10.1007/978-3-319-12736-1_20

  30. Lee, H., Won, S., Jin, J., Cho, J., Ryu, S.: SAFE: Formal Specification and Implementation of a Scalable Analysis Framework for ECMAScript. In: Proceedings of the 19th International Workshop on Foundations of Object-Oriented Languages (FOOL’12) (2012)

    Google Scholar 

  31. Logozzo, F., Fähndrich, M.: Static contract checking with abstract interpretation. In: B. Beckert, C. Marché (eds.) Formal Verification of Object-Oriented Software - International Conference, FoVeOOS 2010, Paris, France, June 28-30, 2010, Revised Selected Papers, Lecture Notes in Computer Science, vol. 6528, pp. 10–30. Springer (2010). https://doi.org/10.1007/978-3-642-18070-5_2

  32. Madsen, M., Andreasen, E.: String analysis for dynamic field access. In: A. Cohen (ed.) Compiler Construction - 23rd International Conference, CC 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014. Proceedings, Lecture Notes in Computer Science, vol. 8409, pp. 197–217. Springer (2014). https://doi.org/10.1007/978-3-642-54807-9_12

  33. Mandal, A.K., Panarotto, F., Cortesi, A., Ferrara, P., Spoto, F.: Static analysis of android auto infotainment and on-board diagnostics II apps. Softw. Pract. Exp. 49(7), 1131–1161 (2019). https://doi.org/10.1002/spe.2698

    Article  Google Scholar 

  34. Minamide, Y.: Static approximation of dynamically generated web pages. In: A. Ellis, T. Hagino (eds.) Proceedings of the 14th international conference on World Wide Web, WWW 2005, Chiba, Japan, May 10-14, 2005, pp. 432–441. ACM (2005). https://doi.org/10.1145/1060745.1060809

  35. Miné, A.: The octagon abstract domain. High. Order Symb. Comput. 19(1), 31–100 (2006). https://doi.org/10.1007/s10990-006-8609-1

    Article  MATH  Google Scholar 

  36. Narodytska, N.: Formal verification of deep neural networks. In: N. Bjørner, A. Gurfinkel (eds.) 2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30 - November 2, 2018, p. 1. IEEE (2018). https://doi.org/10.23919/FMCAD.2018.8603017

  37. Nielson, F.: Tensor Products Generalize the Relational Data Flow Analysis Method. In: Proc. Fourth Hungarian Computer Science Conference, pp. 211–225 (1985)

    Google Scholar 

  38. Park, C., Im, H., Ryu, S.: Precise and scalable static analysis of jquery using a regular expression domain. In: R. Ierusalimschy (ed.) Proceedings of the 12th Symposium on Dynamic Languages, DLS 2016, Amsterdam, The Netherlands, November 1, 2016, pp. 25–36. ACM (2016). https://doi.org/10.1145/2989225.2989228

  39. Samimi, H., Schäfer, M., Artzi, S., Millstein, T.D., Tip, F., Hendren, L.J.: Automated repair of HTML generation errors in PHP applications using string constraint solving. In: M. Glinz, G.C. Murphy, M. Pezzè (eds.) 34th International Conference on Software Engineering, ICSE 2012, June 2-9, 2012, Zurich, Switzerland, pp. 277–287. IEEE Computer Society (2012). https://doi.org/10.1109/ICSE.2012.6227186

  40. Tateishi, T., Pistoia, M., Tripp, O.: Path- and index-sensitive string analysis based on monadic second-order logic. ACM Trans. Softw. Eng. Methodol. 22(4), 33:1–33:33 (2013). https://doi.org/10.1145/2522920.2522926

  41. Tripp, O., Ferrara, P., Pistoia, M.: Hybrid security analysis of web javascript code via dynamic partial evaluation. In: C.S. Pasareanu, D. Marinov (eds.) International Symposium on Software Testing and Analysis, ISSTA ’14, San Jose, CA, USA - July 21 - 26, 2014, pp. 49–59. ACM (2014). https://doi.org/10.1145/2610384.2610385

  42. Wassermann, G., Su, Z.: Sound and precise analysis of web applications for injection vulnerabilities. In: J. Ferrante, K.S. McKinley (eds.) Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, San Diego, California, USA, June 10-13, 2007, pp. 32–41. ACM (2007). https://doi.org/10.1145/1250734.1250739

  43. Wassermann, G., Su, Z.: Static detection of cross-site scripting vulnerabilities. In: W. Schäfer, M.B. Dwyer, V. Gruhn (eds.) 30th International Conference on Software Engineering (ICSE 2008), Leipzig, Germany, May 10-18, 2008, pp. 171–180. ACM (2008). https://doi.org/10.1145/1368088.1368112

  44. Yamaguchi, T., Brain, M., Ryder, C., Imai, Y., Kawamura, Y.: Application of abstract interpretation to the automotive electronic control system 11388, 425–445 (2019). https://doi.org/10.1007/978-3-030-11245-5_20

    Article  Google Scholar 

  45. Yu, F., Alkhalaf, M., Bultan, T.: Patching vulnerabilities with sanitization synthesis. In: R.N. Taylor, H.C. Gall, N. Medvidovic (eds.) Proceedings of the 33rd International Conference on Software Engineering, ICSE 2011, Waikiki, Honolulu , HI, USA, May 21-28, 2011, pp. 251–260. ACM (2011). https://doi.org/10.1145/1985793.1985828

  46. Yu, F., Bultan, T., Cova, M., Ibarra, O.H.: Symbolic string verification: An automata-based approach. In: K. Havelund, R. Majumdar, J. Palsberg (eds.) Model Checking Software, 15th International SPIN Workshop, Los Angeles, CA, USA, August 10-12, 2008, Proceedings, Lecture Notes in Computer Science, vol. 5156, pp. 306–324. Springer (2008). https://doi.org/10.1007/978-3-540-85114-1_21

  47. Yu, F., Bultan, T., Hardekopf, B.: String abstractions for string verification. In: A. Groce, M. Musuvathi (eds.) Model Checking Software - 18th International SPIN Workshop, Snowbird, UT, USA, July 14-15, 2011. Proceedings, Lecture Notes in Computer Science, vol. 6823, pp. 20–37. Springer (2011). https://doi.org/10.1007/978-3-642-22306-8_3

Download references

Acknowledgements

Work partially supported by SPIN-2021 projects “Ressa-Rob” and “Static Analysis for Data Scientists”, and Fondi di primo insediamento 2019 project “Static Taint Analysis for IoT Software” funded by Ca’ Foscari University, and by iNEST-Interconnected NordEst Innovation Ecosystem, funded by PNRR (Mission 4.2, Investment 1.5), NextGeneration EU—Project ID: ECS 00000043.

Author information

Authors and Affiliations

  1. Ca’ Foscari University of Venice, Venice, Italy

    Martina Olliaro, Agostino Cortesi & Pietro Ferrara

  2. University of Parma, Parma, Italy

    Vincenzo Arceri

Authors
  1. Martina Olliaro
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Vincenzo Arceri
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Agostino Cortesi
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Pietro Ferrara
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Martina Olliaro .

Editor information

Editors and Affiliations

  1. Department of Mathematical, Physical, and Computer Sciences, University of Parma, Parma, Italy

    Vincenzo Arceri

  2. Department of Environmental Sciences, Informatics and Statistics, Ca’ Foscari University of Venice, Venice, Italy

    Agostino Cortesi

  3. Department of Environmental Sciences, Informatics and Statistics, Ca’ Foscari University of Venice, Venice, Italy

    Pietro Ferrara

  4. Department of Environmental Sciences, Informatics and Statistics, Ca’ Foscari University of Venice, Venice, Italy

    Martina Olliaro

Rights and permissions

Reprints and permissions

Copyright information

© 2023 The Author(s), under exclusive license to Springer Nature Singapore Pte Ltd.

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Olliaro, M., Arceri, V., Cortesi, A., Ferrara, P. (2023). Lifting String Analysis Domains. In: Arceri, V., Cortesi, A., Ferrara, P., Olliaro, M. (eds) Challenges of Software Verification. Intelligent Systems Reference Library, vol 238. Springer, Singapore. https://doi.org/10.1007/978-981-19-9601-6_7

Download citation

  • DOI: https://doi.org/10.1007/978-981-19-9601-6_7

  • Published:

  • Publisher Name: Springer, Singapore

  • Print ISBN: 978-981-19-9600-9

  • Online ISBN: 978-981-19-9601-6

  • eBook Packages: EngineeringEngineering (R0)

Publish with us

Policies and ethics

Search

Navigation