Skip to main content
SpringerLink
Log in
Book cover

String Analysis for Software Verification and Security pp 155–164Cite as

A Brief Survey of Related Work

  • Chapter
  • First Online:

  • 692 Accesses

Abstract

In this chapter we provide a brief survey of related research work. We first give an overview of alternative approaches to string analysis, followed by a discussion on recent work on string constraint solvers. We discuss application of string analysis and string constraint solving techniques to bug and vulnerability detection in web applications. We conclude the section with a discussion in differential analysis and program repair techniques.

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

References

  1. Prateek Saxena, Devdatta Akhawe, Steve Hanna, Feng Mao, Stephen McCamant, and Dawn Song. A symbolic execution framework for javascript. In Proceedings of the IEEE Symposium on Security and Privacy, pages 513–528, 2010.

    Google Scholar 

  2. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukás Holík, Ahmed Rezine, Philipp Rümmer, and Jari Stenman. String constraints for verification. In Proceedings of the 26th International Conference on Computer Aided Verification (CAV), pages 150–166, 2014.

    Google Scholar 

  3. 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 

  4. 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 

  5. Muath Alkhalaf, Tevfik Bultan, and Jose L. Gallegos. Verifying client-side input validation functions using string analysis. In Proceedings of the 2012 International Conference on Software Engineering, pages 947–957, 2012.

    Google Scholar 

  6. 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 

  7. Jesper Andersen and Julia L. Lawall. Generic patch inference. In Proceedings of the 2008 23rd IEEE/ACM International Conference on Automated Software Engineering, ASE ’08, pages 337–346, Washington, DC, USA, 2008. IEEE Computer Society.

    Google Scholar 

  8. Christopher Anderson, Paola Giannini, and Sophia Drossopoulou. Towards type inference for javascript. In ECOOP 2005-Object-Oriented Programming, pages 428–452. Springer, 2005.

    Google Scholar 

  9. Shay Artzi, Adam Kiezun, Julian Dolby, Frank Tip, Daniel Dig, Amit Paradkar, and Michael D Ernst. Finding bugs in web applications using dynamic test generation and explicit-state model checking. Software Engineering, IEEE Transactions on, 36(4):474–494, 2010.

    Google Scholar 

  10. 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 

  11. 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 

  12. Mike Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K. Rustan M. Leino. Boogie: A modular reusable verifier for object-oriented programs. In Proceedings of the 4th International Conference on Formal Methods for Components and Objects, FMCO’05, pages 364–387, Berlin, Heidelberg, 2006. Springer-Verlag.

    Google Scholar 

  13. 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 

  14. Constantinos Bartzis and Tevfik Bultan. Widening arithmetic automata. In R. Alur and D. Peled, editors, Proceedings of the 16th International Conference on Computer Aided Verification (CAV 2004), volume 3114 of Lecture Notes in Computer Science, pages 321–333. Springer-Verlag, July 2004.

    Google Scholar 

  15. Prithvi Bisht, Timothy Hinrichs, Nazari Skrupsky, Radoslaw Bobrowicz, and V. N. Venkatakrishnan. Notamper: automatic blackbox detection of parameter tampering opportunities in web applications. In Proceedings of the 17th ACM conference on Computer and communications security, CCS ’10, pages 607–618, New York, NY, USA, 2010. ACM.

    Google Scholar 

  16. Prithvi Bisht, Timothy Hinrichs, Nazari Skrupsky, and V. N. Venkatakrishnan. Waptec: Whitebox analysis of web applications for parameter tampering exploit construction. In Proceedings of the 18th ACM Conference on Computer and Communications Security, CCS ’11, pages 575–586, New York, NY, USA, 2011. ACM.

    Google Scholar 

  17. 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 

  18. BRICS. The MONA project. http://www.brics.dk/mona/.

  19. Tae-Hyoung Choi, Oukseh Lee, Hyunha Kim, and Kyung-Goo Doh. A practical string analyzer by the widening approach. In APLAS, pages 374–388, 2006.

    Google Scholar 

  20. 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 

  21. Mihai Christodorescu, Nicholas Kidd, and Wen-Han Goh. String analysis for x86 binaries. In Proceedings of the 6th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering (PASTE 2005). ACM Press, September 2005.

    Google Scholar 

  22. Ravi Chugh, Jeffrey A Meister, Ranjit Jhala, and Sorin Lerner. Staged information flow for javascript. In ACM Sigplan Notices, volume 44, pages 50–62. ACM, 2009.

    Google Scholar 

  23. Johannes Dahse and Thorsten Holz. Simulation of built-in php features for precise static code analysis. In Proceedings of Network and Distributed System Security (NDSS’14) Symposium, 2014.

    Google Scholar 

  24. Loris D’Antoni and Margus Veanes. Equivalence of extended symbolic finite transducers. In Computer Aided Verification, pages 624–639. Springer, 2013.

    Google Scholar 

  25. Loris D’Antoni and Margus Veanes. Minimization of symbolic automata. In Proceedings of the 41st annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 541–554. ACM, 2014.

    Google Scholar 

  26. Mohan Dhawan and Vinod Ganapathy. Analyzing information flow in javascript-based browser extensions. In Computer Security Applications Conference, 2009. ACSAC’09. Annual, pages 382–391. IEEE, 2009.

    Google Scholar 

  27. Nurit Dor, Michael Rodeh, and Mooly Sagiv. Cssv: towards a realistic tool for statically detecting all buffer overflows in c. SIGPLAN Not., 38(5):155–167, 2003.

    Article  Google Scholar 

  28. Loris D’Antoni and Margus Veanes. Static analysis of string encoders and decoders. In Proceedings of the 14th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), pages 209–228, 2013.

    Google Scholar 

  29. Xiang Fu, Xin Lu, Boris Peltsverger, Shijun Chen, Kai Qian, and Lixin Tao. A static analysis framework for detecting sql injection vulnerabilities. In COMPSAC, pages 87–96, 2007.

    Google Scholar 

  30. Vinod Ganapathy, Somesh Jha, David Chandler, David Melski, and David Vitek. Buffer overrun detection using linear programming and static analysis. In Proceedings of the 10th ACM Conference on Computer and Communications Security, pages 345–354, 2003.

    Google Scholar 

  31. Vijay Ganesh, Mia Minnes, Armando Solar-Lezama, and Martin C. Rinard. Word equations with length constraints: What’s decidable? In Proceedings of the 8th International Haifa Verification Conference (HVC), pages 209–226, 2012.

    Google Scholar 

  32. Dale Gerdemann and Gertjan van Noord. Transducers from rewrite rules with backreferences. In Proceedings of the 9th Conference of the European Chapter of the Association for Computational Linguistics, pages 126–133, 1999.

    Google Scholar 

  33. Salvatore Guarnieri and Benjamin Livshits. Gatekeeper: mostly static enforcement of security and reliability policies for javascript code. In Proceedings of the 18th conference on USENIX security symposium, SSYM’09, pages 151–168, Berkeley, CA, USA, 2009. USENIX Association.

    Google Scholar 

  34. Salvatore Guarnieri, Marco Pistoia, Omer Tripp, Julian Dolby, Stephen Teilhet, and Ryan Berg. Saving the world wide web from vulnerable javascript. In Proceedings of the 2011 International Symposium on Software Testing and Analysis, pages 177–187. ACM, 2011.

    Google Scholar 

  35. Arjun Guha, Shriram Krishnamurthi, and Trevor Jim. Static analysis for ajax intrusion detection. In Proceedings of the International World Wide Web Conference. Citeseer, 2009.

    Google Scholar 

  36. Arjun Guha, Claudiu Saftoiu, and Shriram Krishnamurthi. The essence of javascript. In ECOOP 2010–Object-Oriented Programming, pages 126–150. Springer, 2010.

    Google Scholar 

  37. William G. J. Halfond and Alessandro Orso. Amnesia: analysis and monitoring for neutralizing sql-injection attacks. In ASE ’05: Proceedings of the 20th IEEE/ACM international Conference on Automated software engineering, pages 174–183, New York, NY, USA, 2005. ACM.

    Google Scholar 

  38. Jesper G. Henriksen, Jakob Jensen, Michael Jørgensen, Nils Klarlund, Robert Paige, Theis Rauhe, and Anders Sandholm. Mona: Monadic second-order logic in practice. In E. Brinksma, W. R. Cleaveland, K. G. Larsen, T. Margaria, and B. Steffen, editors, Tools and Algorithms for the Construction and Analysis of Systems: First International Workshop, TACAS ’95 Aarhus, Denmark, May 19–20, 1995 Selected Papers, pages 89–110, Berlin, Heidelberg, 1995. Springer Berlin Heidelberg.

    Google Scholar 

  39. Pieter Hooimeijer, Ben Livshits, David Molnar, Prateek Saxena, and Margus Veanes. Fast and Precise Sanitizer Analysis with Bek. In Usenix Security Symposium, 2011.

    Google Scholar 

  40. Pieter Hooimeijer and Westley Weimer. A decision procedure for subset constraints over regular languages. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 188–198, 2009.

    Google Scholar 

  41. Pieter Hooimeijer and Westley Weimer. Solving string constraints lazily. In Proceedings of the 25th IEEE/ACM International Conference on Automated Software Engineering (ASE), pages 377–386, 2010.

    Google Scholar 

  42. Simon Holm Jensen, Magnus Madsen, and Anders Møller. Modeling the html dom and browser api in static analysis of javascript web applications. In Proceedings of the 19th ACM SIGSOFT symposium and the 13th European conference on Foundations of software engineering, pages 59–69. ACM, 2011.

    Google Scholar 

  43. Simon Holm Jensen, Anders Møller, and Peter Thiemann. Type analysis for javascript. In Static Analysis, pages 238–255. Springer, 2009.

    Google Scholar 

  44. Nenad Jovanovic, Christopher Krügel, and Engin Kirda. Pixy: A static analysis tool for detecting web application vulnerabilities. In S&P, pages 258–263, 2006.

    Google Scholar 

  45. Lauri Karttunen. The replace operator. In Proceedings of the 33rd annual meeting on Association for Computational Linguistics, pages 16–23, 1995.

    Google Scholar 

  46. Vineeth Kashyap, John Sarracino, John Wagner, Ben Wiedermann, and Ben Hardekopf. Type refinement for static analysis of javascript. In Proceedings of the 9th symposium on Dynamic languages, pages 17–26. ACM, 2013.

    Google Scholar 

  47. 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 

  48. Haruka Kikuchi, Dachuan Yu, Ajay Chander, Hiroshi Inamura, and Igor Serikov. Javascript instrumentation in practice. In Programming Languages and Systems, pages 326–341. Springer, 2008.

    Google Scholar 

  49. Christian Kirkegaard, Anders Møller, and Michael I. Schwartzbach. Static analysis of xml transformations in java. IEEE Transactions on Software Engineering, 30(3), March 2004.

    Google Scholar 

  50. Etienne Kneuss, Philippe Suter, and Viktor Kuncak. Phantm: Php analyzer for type mismatch. In Proceedings of the Eighteenth ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE ’10, pages 373–374, New York, NY, USA, 2010. ACM.

    Google Scholar 

  51. Shuvendu K. Lahiri, Chris Hawblitzel, Ming Kawaguchi, and Henrique Rebêlo. Symdiff: A language-agnostic semantic diff tool for imperative programs. In Proceedings of the 24th International Conference on Computer Aided Verification (CAV), pages 712–717, 2012.

    Google Scholar 

  52. Shuvendu K. Lahiri, Kapil Vaswani, and C A. R. Hoare. Differential static analysis: Opportunities, applications, and challenges. In Proceedings of the FSE/SDP Workshop on Future of Software Engineering Research, pages 201–204, 2010.

    Google Scholar 

  53. 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 

  54. Tianyi Liang, Andrew Reynolds, Cesare Tinelli, Clark Barrett, and Morgan Deters. A DPLL(T) theory solver for a theory of strings and regular expressions. In Proceedings of the 26th International Conference on Computer Aided Verification (CAV), pages 646–662, 2014.

    Google Scholar 

  55. Benjamin Livshits and Stephen Chong. Towards fully automatic placement of security sanitizers and declassifiers. In Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’13, pages 385–398, New York, NY, USA, 2013. ACM.

    Google Scholar 

  56. Loi Luu, Shweta Shinde, Prateek Saxena, and Brian Demsky. A model counter for constraints over unbounded strings. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), page 57, 2014.

    Google Scholar 

  57. Microsoft Inc. Z3 SMT Solver. http://z3.codeplex.com.

  58. Microsoft Research. Pex. http://research.microsoft.com/en-us/projects/pex/.

  59. 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 

  60. Mehryar Mohri and Richard Sproat. An efficient compiler for weighted rewrite rules. In Proceedings of the 34th annual meeting on Association for Computational Linguistics, pages 231–238. Association for Computational Linguistics, 1996.

    Google Scholar 

  61. Hoang Duong Thien Nguyen, Dawei Qi, Abhik Roychoudhury, and Satish Chandra. Semfix: Program repair via semantic analysis. In Proceedings of the 2013 International Conference on Software Engineering, ICSE ’13, pages 772–781, Piscataway, NJ, USA, 2013. IEEE Press.

    Google Scholar 

  62. Suzette J. Person. Differential Symbolic Execution. PhD thesis, Lincoln, NB, USA, 2009. AAI3365729.

    Google Scholar 

  63. Gregor Richards, Sylvain Lebresne, Brian Burg, and Jan Vitek. An analysis of the dynamic behavior of javascript programs. In Proceedings of the 2010 ACM SIGPLAN conference on Programming language design and implementation, PLDI ’10, pages 1–12, New York, NY, USA, 2010. ACM.

    Google Scholar 

  64. Hesam Samimi, Max Schäfer, Shay Artzi, Todd Millstein, Frank Tip, and Laurie Hendren. Automated repair of html generation errors in php applications using string constraint solving. In Proceedings of the 2012 International Conference on Software Engineering, ICSE 2012, pages 277–287, Piscataway, NJ, USA, 2012. IEEE Press.

    Google Scholar 

  65. 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 

  66. Prateek Saxena, Steve Hanna, Pongsin Poosankam, and Dawn Song. Flax: Systematic discovery of client-side validation vulnerabilities in rich web applications. In Proceedings of the Network and Distributed System Security Symposium (NDSS), 2010.

    Google Scholar 

  67. Koushik Sen, Darko Marinov, and Gul Agha. Cute: a concolic unit testing engine for c. In Proceedings of the 10th European Software Engineering Conference held jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering (ESEC/FSE 05), pages 263–272, 2005.

    Google Scholar 

  68. Daryl Shannon, Sukant Hajra, Alison Lee, Daiqian Zhan, and Sarfraz Khurshid. Abstracting symbolic execution with string analysis. In TAICPART-MUTATION, pages 13–22, 2007.

    Google Scholar 

  69. Sooel Son, Kathryn S. McKinley, and Vitaly Shmatikov. Rolecast: Finding missing security checks when you do not know what checks are. In Proceedings of the 2011 ACM International Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA ’11, pages 1069–1084, New York, NY, USA, 2011. ACM.

    Google Scholar 

  70. Sooel Son, Kathryn S. McKinley, and Vitaly Shmatikov. Fix me up: Repairing access-control bugs in web applications. In NDSS, 2013.

    Google Scholar 

  71. Kunal Taneja, Nuo Li, Madhuri R. Marri, Tao Xie, and Nikolai Tillmann. Mitv: multiple-implementation testing of user-input validators for web applications. In ASE, pages 131–134, 2010.

    Google Scholar 

  72. Takaaki Tateishi, Marco Pistoia, and Omer Tripp. Path- and index-sensitive string analysis based on monadic second-order logic. In Proceedings of the 2011 International Symposium on Software Testing and Analysis, ISSTA ’11, pages 166–176, New York, NY, USA, 2011. ACM.

    Google Scholar 

  73. Minh-Thai Trinh, Duc-Hiep Chu, and Joxan Jaffar. S3: A symbolic string solver for vulnerability detection in web applications. In Proceedings of the ACM SIGSAC Conference on Computer and Communications Security (CCS), pages 1232–1243, 2014.

    Google Scholar 

  74. Minh-Thai Trinh, Duc-Hiep Chu, and Joxan Jaffar. S3: A symbolic string solver for vulnerability detection in web applications. In Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, CCS ’14, pages 1232–1243, New York, NY, USA, 2014. ACM.

    Google Scholar 

  75. Gertjan van Noord. FSA utilities toolbox. http://odur.let.rug.nl/~vannoord/Fsa/.

  76. Gertjan van Noord and Dale Gerdemann. An extendible regular expression compiler for finite-state approaches in natural language processing. In Proc. of the 4th International Workshop on Implementing Automata (WIA), pages 122–139. Springer-Verlag, July 1999.

    Google Scholar 

  77. Margus Veanes. Symbolic string transformations with regular lookahead and rollback. In Proceedings of the 9th Ershov Informatics Conference (PSI’14). Springer, 2014.

    Google Scholar 

  78. Margus Veanes and Nikolaj Bjørner. Symbolic automata: The toolkit. In TACAS, pages 472–477, 2012.

    Google Scholar 

  79. Margus Veanes, Nikolaj Bjørner, and Leonardo De Moura. Symbolic automata constraint solving. In Logic for Programming, Artificial Intelligence, and Reasoning, pages 640–654. Springer, 2010.

    Google Scholar 

  80. Margus Veanes, Peli De Halleux, and Nikolai Tillmann. Rex: Symbolic regular expression explorer. In Software Testing, Verification and Validation (ICST), 2010 Third International Conference on, pages 498–507. IEEE, 2010.

    Google Scholar 

  81. 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 

  82. 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 

  83. David Wagner, Jeffrey S. Foster, Eric A. Brewer, and Alexander Aiken. A first step towards automated detection of buffer overrun vulnerabilities. In In Network and Distributed System Security Symposium, pages 3–17, 2000.

    Google Scholar 

  84. 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 

  85. 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 

  86. Gary Wassermann and Zhendong Su. Static detection of cross-site scripting vulnerabilities. In Proceedings of the 30th International Conference on Software Engineering, ICSE ’08, pages 171–180, New York, NY, USA, 2008. ACM.

    Google Scholar 

  87. Gary Wassermann, Dachuan Yu, Ajay Chander, Dinakar Dhurjati, Hiroshi Inamura, and Zhendong Su. Dynamic test input generation for web applications. In Proceedings of the ACM/SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2008), pages 249–260, 2008.

    Google Scholar 

  88. Westley Weimer, Stephanie Forrest, Claire Le Goues, and ThanhVu Nguyen. Automatic program repair with evolutionary computation. Commun. ACM, 53(5):109–116, May 2010.

    Article  Google Scholar 

  89. Westley Weimer, ThanhVu Nguyen, Claire Le Goues, and Stephanie Forrest. Automatically finding patches using genetic programming. In Proceedings of the 31st International Conference on Software Engineering, ICSE ’09, pages 364–374, Washington, DC, USA, 2009. IEEE Computer Society.

    Google Scholar 

  90. Yichen Xie and Alex Aiken. Static detection of security vulnerabilities in scripting languages. In USENIX-SS’06: Proceedings of the 15th conference on USENIX Security Symposium, pages 13–13, Berkeley, CA, USA, 2006. USENIX Association.

    Google Scholar 

  91. Fang Yu, Muath Alkhalaf, and Tevfik Bultan. Generating vulnerability signatures for string manipulating programs using automata-based forward and backward symbolic analyses. In ASE, 2009.

    Google Scholar 

  92. Fang Yu, Muath Alkhalaf, and Tevfik Bultan. Stranger: An automata-based string analysis tool for php. In TACAS, 2010.

    Google Scholar 

  93. 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 

  94. 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 

  95. 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 

  96. 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 

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

    Google Scholar 

  98. Fang Yu, Tevfik Bultan, and Oscar H. Ibarra. Relational string verification using multi-track automata. Int. J. Found. Comput. Sci., 22(8):1909–1924, 2011.

    Article  MathSciNet  MATH  Google Scholar 

  99. Yunhui Zheng, Xiangyu Zhang, and Vijay Ganesh. Z3-str: A z3-based string solver for web application analysis. In Proceedings of the 9th Joint Meeting on Foundations of Software Engineering (ESEC/FSE), pages 114–124, 2013.

    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). A Brief Survey of Related Work. In: String Analysis for Software Verification and Security. Springer, Cham. https://doi.org/10.1007/978-3-319-68670-7_11

Download citation

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

  • 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