Skip to main content
SpringerLink
Log in

Introduction

  • Chapter
  • First Online:
String Analysis for Software Verification and Security

  • 672 Accesses

Abstract

In computing, a sequence of characters is called a string. For example, “Hello, World!” is a string (we use double quotes to indicate the beginning and end of the string). This particular string is very familiar to programmers since the first programming assignment in many programming textbooks is to write a program that outputs the string “Hello, World!” Although programmers become familiar with the creation and manipulation of strings very early on in their training, errors in string manipulating code is a major cause of software faults and vulnerabilities. This indicates that string manipulation is a challenging task for programmers, and automated techniques for analyzing string manipulating code, which is the topic of this monograph, are very desirable.

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

Access this chapter

Log in via an institution

Institutional subscriptions

References

  1. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukáš Holík, Ahmed Rezine, Philipp Rümmer, and Jari Stenman. Computer Aided Verification: 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18–24, 2015, Proceedings, Part I, chapter Norn: An SMT Solver for String Constraints, pages 462–469. Springer International Publishing, Cham, 2015.

    Google Scholar 

  2. Muath Alkhalaf, Abdulbaki Aydin, and Tevfik Bultan. Semantic differential repair for input validation and sanitization. In Proceedings of the 2014 International Symposium on Software Testing and Analysis (ISSTA 2014), 2014.

    Google Scholar 

  3. Muath Alkhalaf, Shauvik Roy Choudhary, Mattia Fazzini, Tevfik Bultan, Alessandro Orso, and Christopher Kruegel. Viewpoints: differential string analysis for discovering client- and server-side input validation inconsistencies. In Proceedings of the 2012 International Symposium on Software Testing and Analysis (ISSTA), pages 56–66, 2012.

    Google Scholar 

  4. Abdulbaki Aydin, Lucas Bang, and Tevfik Bultan. Computer Aided Verification: 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18–24, 2015, Proceedings, Part I, chapter Automata-Based Model Counting for String Constraints, pages 255–272. Springer International Publishing, Cham, 2015.

    Google Scholar 

  5. Davide Balzarotti, Marco Cova, Vika Felmetsger, Nenad Jovanovic, Engin Kirda, Christopher Kruegel, and Giovanni Vigna. Saner: Composing static and dynamic analysis to validate sanitization in web applications. In Proceedings of the 2008 IEEE Symposium on Security and Privacy, SP ’08, pages 387–401, Washington, DC, USA, 2008. IEEE Computer Society.

    Google Scholar 

  6. Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanović, Tim King, Andrew Reynolds, and Cesare Tinelli. Computer Aided Verification: 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14–20, 2011. Proceedings, chapter CVC4, pages 171–177. Springer Berlin Heidelberg, Berlin, Heidelberg, 2011.

    Google Scholar 

  7. Nikolaj Bjørner, Nikolai Tillmann, and Andrei Voronkov. Path feasibility analysis for string-manipulating programs. In Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems: Held As Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009,, TACAS ’09, pages 307–321, Berlin, Heidelberg, 2009. Springer-Verlag.

    Google Scholar 

  8. Eric Bodden, Andreas Sewe, Jan Sinschek, Hela Oueslati, and Mira Mezini. Taming reflection: Aiding static analysis in the presence of reflection and custom class loaders. In Proceedings of the 33rd International Conference on Software Engineering, ICSE ’11, pages 241–250, New York, NY, USA, 2011. ACM.

    Google Scholar 

  9. Aske Simon Christensen, Anders Møller, and Michael I. Schwartzbach. Precise analysis of string expressions. In Proc. 10th International Static Analysis Symposium, SAS ’03, volume 2694 of LNCS, pages 1–18. Springer-Verlag, June 2003.

    Google Scholar 

  10. CVE. Common Vulnerabilities and Exposures. http://www.cve.mitre.org.

  11. Loris D’antoni and Margus Veanes. Extended symbolic finite automata and transducers. Form. Methods Syst. Des., 47(1):93–119, August 2015.

    Article  MATH  Google Scholar 

  12. DroidBench. Droidbench benchmarks. https://github.com/secure-software-engineering/DroidBench.

  13. Pieter Hooimeijer and Westley Weimer. Strsolve: solving string constraints lazily. Automated Software Engineering, 19(4):531–559, 2012.

    Article  Google Scholar 

  14. Simon Holm Jensen, Peter A. Jonsson, and Anders Møller. Remedying the eval that men do. In Proceedings of the 2012 International Symposium on Software Testing and Analysis (ISSTA), pages 34–44, 2012.

    Google Scholar 

  15. Adam Kiezun, Vijay Ganesh, Philip J. Guo, Pieter Hooimeijer, and Michael D. Ernst. Hampi: a solver for string constraints. In Proceedings of the 18th International Symposium on Software Testing and Analysis (ISSTA), pages 105–116, 2009.

    Google Scholar 

  16. Guodong Li and Indradeep Ghosh. PASS: string solving with parameterized array and interval automaton. In Proceedings of the 9th International Haifa Verification Conference (HVC), pages 15–31, 2013.

    Google Scholar 

  17. Li Li, Tegawendé F Bissyandé, Damien Octeau, and Jacques Klein. Droidra: taming reflection to support whole-program analysis of android apps. In Proceedings of the 25th International Symposium on Software Testing and Analysis, pages 318–329. ACM, 2016.

    Google Scholar 

  18. Yasuhiko Minamide. Static approximation of dynamically generated web pages. In Proceedings of the 14th International World Wide Web Conference (WWW), pages 432–441, 2005.

    Google Scholar 

  19. Hung Viet Nguyen, Christian Kästner, and Tien N. Nguyen. Building call graphs for embedded client-side code in dynamic web applications. In Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE-22), pages 518–529, 2014.

    Google Scholar 

  20. Hung Viet Nguyen, Christian Kästner, and Tien N. Nguyen. Varis: IDE support for embedded client code in PHP web applications. In Proceedings of the 37th IEEE/ACM International Conference on Software Engineering (ICSE), pages 693–696, 2015.

    Google Scholar 

  21. OWASP. Top 10 2007. https://www.owasp.org/index.php/Top_10_2007.

  22. OWASP. Top 10 2013. https://www.owasp.org/index.php/Top_10_2013-T10.

  23. Prateek Saxena, Devdatta Akhawe, Steve Hanna, Feng Mao, Stephen McCamant, and Dawn Song. A symbolic execution framework for javascript. In Proceedings of the 31st IEEE Symposium on Security and Privacy, 2010.

    Google Scholar 

  24. Zhendong Su and Gary Wassermann. The essence of command injection attacks in web applications. In Conference Record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’06, pages 372–382, New York, NY, USA, 2006. ACM.

    Google Scholar 

  25. Margus Veanes, Peli de Halleux, and Nikolai Tillmann. Rex: Symbolic regular expression explorer. In Proceedings of the 2010 Third International Conference on Software Testing, Verification and Validation, ICST ’10, pages 498–507, Washington, DC, USA, 2010. IEEE Computer Society.

    Google Scholar 

  26. Margus Veanes, Pieter Hooimeijer, Benjamin Livshits, David Molnar, and Nikolaj Bjorner. Symbolic finite state transducers: algorithms and applications. In Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, POPL ’12, pages 137–150, New York, NY, USA, 2012. ACM.

    Google Scholar 

  27. Margus Veanes, Todd Mytkowicz, David Molnar, and Benjamin Livshits. Data-parallel string-manipulating programs. In Proceedings of the 42Nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’15, pages 139–152, New York, NY, USA, 2015. ACM.

    Google Scholar 

  28. Gary Wassermann, Carl Gould, Zhendong Su, and Premkumar Devanbu. Static checking of dynamically generated queries in database applications. volume 16, New York, NY, USA, September 2007. ACM.

    Google Scholar 

  29. Gary Wassermann and Zhendong Su. Sound and precise analysis of web applications for injection vulnerabilities. In Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation (PLDI), pages 32–41, 2007.

    Google Scholar 

  30. Fang Yu, Muath Alkhalaf, and Tevfik Bultan. Patching vulnerabilities with sanitization synthesis. In Proceedings of the 33rd International Conference on Software Engineering (ICSE), pages 251–260, 2011.

    Google Scholar 

  31. Fang Yu, Muath Alkhalaf, Tevfik Bultan, and Oscar H. Ibarra. Automata-based symbolic string analysis for vulnerability detection. Formal Methods in System Design, 44(1):44–70, 2014.

    Article  MATH  Google Scholar 

  32. Fang Yu, Tevfik Bultan, Marco Cova, and Oscar H. Ibarra. Symbolic string verification: An automata-based approach. In 15th International SPIN Workshop on Model Checking Software (SPIN), pages 306–324, 2008.

    Google Scholar 

  33. Fang Yu, Tevfik Bultan, and Ben Hardekopf. String abstractions for string verification. In Proceedings of the 18th International SPIN Conference on Model Checking Software, pages 20–37, Berlin, Heidelberg, 2011. Springer-Verlag.

    Google Scholar 

  34. Fang Yu, Tevfik Bultan, and Oscar H. Ibarra. Symbolic string verification: Combining string analysis and size analysis. In 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2009), pages 322–336, 2009.

    Google Scholar 

  35. Fang Yu, Tevfik Bultan, and Oscar H. Ibarra. Relational string verification using multi-track automata. In CIAA, pages 290–299, 2010.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of California, Santa Barbara, Santa Barbara, CA, USA

    Tevfik Bultan

  2. Department of Management, Information Systems, National Chenchi University, Taipei, Taiwan

    Fang Yu

  3. Computer Science Department, King Saud University, Riyadh, Saudi Arabia

    Muath Alkhalaf

  4. Microsoft (United States), Redmond, WA, USA

    Abdulbaki Aydin

Authors
  1. Tevfik Bultan
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Fang Yu
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Muath Alkhalaf
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Abdulbaki Aydin
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Bultan, T., Yu, F., Alkhalaf, M., Aydin, A. (2017). Introduction. In: String Analysis for Software Verification and Security. Springer, Cham. https://doi.org/10.1007/978-3-319-68670-7_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-68670-7_1

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-68668-4

  • Online ISBN: 978-3-319-68670-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation