research-article

Symbolic execution of programs with strings

Authors:

Gideon Redelinghuys,

Jaco GeldenhuysAuthors Info & Claims

SAICSIT '12: Proceedings of the South African Institute for Computer Scientists and Information Technologists Conference

Pages 139 - 148

https://doi.org/10.1145/2389836.2389853

Published: 01 October 2012 Publication History

Abstract

Symbolic execution has long been a popular technique for automated test generation and for error detection in complex code. Most of the focus has however been on programs manipulating integers, booleans, and references in object oriented programs. Recently researchers have started looking at programs that do lots of string processing; this is motivated by the popularity of the web and the risk that errors in such programs may lead to security violations. Attempts to extend symbolic execution to the domain of strings have mainly been divided into one of two camps: automata-based approaches and approaches based on efficient bitvector analysis. Here we investigate these two approaches in one setting: the symbolic execution framework of Java PathFinder. First we describe the implementations of both approaches and then do an extensive evaluation to show under what circumstances each approach performs well (or not so well). We also illustrate the usefulness of the symbolic execution of strings by finding errors in real-world examples.

References

[1]

Nikolaj Bjørner, Nikolai Tillmann, and Andrei Voronkov. Path feasibility analysis for string-manipulating programs. In Proc 15th Intl Conf on Tools and Algorithms for the Construction and Analysis of Systems, LNCS #5505, pages 307--321. Springer, March 2009.

Digital Library

[2]

Cert Advisory. Multiple vulnerabilities in WU-FTPD. Technical Report CA-2001-33, CERT/CC, 2001.

[3]

Aske Simon Christensen, Anders Møller, and Michael I. Schwartzbach. Precise analysis of string expressions. In Proc 10th Intl Symposium on Static Analysis, LNCS #2694, pages 1--18. Springer, June 2003.

Digital Library

[4]

L. A. Clarke. A system to generate test data and symbolically execute programs. IEEE Trans Software Engineering, 2(3): 215--222, May 1976.

Digital Library

[5]

Leonardo de Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. In Proc 14th Intl Conf on Tools and Algorithms for the Construction and Analysis of Systems, LNCS #4963, pages 337--340. Springer, March 2008.

Digital Library

[6]

Pieter Hooimeijer, David Molnar, Prateek Saxena, and Margus Veanes. Modeling imperative string operations with transducers. Technical Report MSR-TR-2010-96, Microsoft, July 2010.

[7]

Pieter Hooimeijer and Westley Weimer. A decision procedure for subset constraints over regular languages. In Proc 2009 ACM SIGPLAN Conf on Programming Language Design and Implementation, pages 188--198. ACM, June 2009.

Digital Library

[8]

Pieter Hooimeijer and Westley Weimer. Solving string constraints lazily. In Proc 25th IEEE/ACM Intl Conf on Automated Software Engineering, pages 377--386. ACM, September 2010.

Digital Library

[9]

Adam Kieżun. Effective Software Testing with a String-Constraint Solver. PhD thesis, Massachusetts Institute of Technology, USA, June 2009.

[10]

Adam Kieżun, Vijay Ganesh, Philip J. Guo, Pieter Hooimeijer, and Michael D. Ernst. Hampi: a solver for string constraints. In Proc 18th ACM/SIGSOFT Intl Symposium on Software Testing and Analysis, pages 105--116. ACM, July 2009.

Digital Library

[11]

James C. King. Symbolic execution and program testing. Communications of the ACM, 19(7): 385--394, July 1976.

Digital Library

[12]

Corina S. Păsăreanu, Peter C. Mehlitz, David H. Bushnell, Karen Gundy-Burlet, Michael R. Lowry, Suzette Person, and Mark Pape. Combining unit-level symbolic execution and system-level concrete execution for testing NASA software. In Proc 17th ACM/SIGSOFT Intl Symposium on Software Testing and Analysis, pages 15--26. ACM, July 2008.

Digital Library

[13]

Francesca Rossi, Peter van Beek, and Toby Walsh. Handbook of Constraint Programming. Elsevier, 2006.

Digital Library

[14]

Prateek Saxena, Devdatta Akhawe, Steve Hanna, Feng Mao, Stephen McCamant, and Dawn Song. A symbolic execution framework for JavaScript. In Proc 31st IEEE Symposium on Security and Privacy, pages 513--528. IEEE Computer Society, May 2010.

Digital Library

[15]

Daryl Shannon, Indradeep Ghosh, Sreeranga P. Rajan, and Sarfraz Khurshid. Efficient symbolic execution of strings for validating web applications. In Proc 2nd Intl Workshop on Defects in Large Software Systems, pages 22--26. ACM, July 2009.

Digital Library

[16]

Daryl Shannon, Sukant Hajra, Alison Lee, Daiqian Zhan, and Sarfraz Khurshid. Abstracting symbolic execution with string analysis. In Proc Testing: Academic and Industrial Conf, Practice and Research Techniques, pages 13--22. IEEE Computer Society, July 2007.

Digital Library

[17]

Nikolai Tillmann and Jonathan de Halleux. Pex--white box test generation for .NET. In Proc 2nd Intl Conf on Tests and Proofs, LNCS #4966, pages 134--153. Springer, April 2008.

Digital Library

[18]

Margus Veanes, Peli de Halleux, and Nikolai Tillmann. Rex: Symbolic regular expression explorer. In Proc 3rd Intl Conf on Software Testing, Verification and Validation, pages 498--507. IEEE Computer Society, April 2010.

Digital Library

[19]

Fan Yu, Muath Alkhalaf, and Tevfik Bultan. Stranger: An automata-based string analysis tool for PHP. In Proc 16th Intl Conf on Tools and Algorithms for the Construction and Analysis of Systems, LNCS #6015, pages 154--157. Springer, March 2010. Tool paper.

Digital Library

[20]

Fan Yu, Tevfik Bultan, Marco Cova, and Oscar H. Ibarra. Symbolic string verification: An automata-based approach. In Proc 15th Intl SPIN Workshop on Model Checking Software, LNCS #5156, pages 306--324. Springer, August 2008.

Digital Library

[21]

Fan Yu, Tevfik Bultan, and Oscar H. Ibarra. Relational string verification using multi-track automata. In Proc 15th Intl Conf on Implementation and Application of Automata, LNCS #6482, pages 290--299. Springer, August 2010.

Digital Library

[22]

Fang Yu, Muath Alkhalaf, and Tevfik Bultan. Generating vulnerability signatures for string manipulating programs using automata-based forward and backward symbolic analyses. In Proc 24th IEEE/ACM Intl Conf on Automated Software Engineering, pages 605--609. IEEE Computer Society, November 2009.

Digital Library

[23]

Fang Yu, Tevfik Bultan, and Oscar H. Ibarra. Symbolic string verification: Combining string analysis and size analysis. In Proc 15th Intl Conf on Tools and Algorithms for the Construction and Analysis of Systems, LNCS #5505, pages 322--336. Springer, March 2009.

Digital Library

Cited By

Zhang YXie XLi YLin YChen SLiu YLi X(2023)Demystifying Performance Regressions in String SolversIEEE Transactions on Software Engineering10.1109/TSE.2022.316837349:3(947-961)Online publication date: 1-Mar-2023
https://doi.org/10.1109/TSE.2022.3168373
Lotz KKulczynski MNowotka DPoulsen DSchlichtkrull A(2023)Verified Verifying: SMT-LIB for Strings in IsabelleImplementation and Application of Automata10.1007/978-3-031-40247-0_15(206-217)Online publication date: 10-Aug-2023
https://doi.org/10.1007/978-3-031-40247-0_15
Berzish MDay JGanesh VKulczynski MManea FMora FNowotka D(2022)Towards more efficient methods for solving regular-expression heavy string constraintsTheoretical Computer Science10.1016/j.tcs.2022.12.009Online publication date: Dec-2022
https://doi.org/10.1016/j.tcs.2022.12.009
Show More Cited By

Index Terms

Symbolic execution of programs with strings
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Software defect analysis
        Software testing and debugging

Recommendations

Runtime exception detection in Java programs using symbolic execution

Most of the runtime failures of a software system can be revealed during test execution only, which has a very high cost. In Java programs, runtime failures are manifested as unhandled runtime exceptions.

In this paper we present an approach and tool ...
Improving symbolic execution for statechart formalisms
MoDeVVa '12: Proceedings of the Workshop on Model-Driven Engineering, Verification and Validation

Symbolic execution is a program analysis technique that attempts to explore all possible paths through a program by using symbolic values rather than actual data values as inputs. When applied to Statecharts, a model-based formalism for reactive systems,...
Running symbolic execution forever
ISSTA 2020: Proceedings of the 29th ACM SIGSOFT International Symposium on Software Testing and Analysis

When symbolic execution is used to analyse real-world applications, it often consumes all available memory in a relatively short amount of time, sometimes making it impossible to analyse an application for an extended period. In this paper, we present a ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Other conferences

SAICSIT '12: Proceedings of the South African Institute for Computer Scientists and Information Technologists Conference

October 2012

402 pages

ISBN:9781450313087

DOI:10.1145/2389836

Conference Chairs:
Jan Kroeze
Unisa
,
Ruth de Villiers
Unisa

Copyright © 2012 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

UNISA: UNIVERSITY OF SOUTH AFRICA
Microsoft: Microsoft
Pearson: Pearson Education
Masterskill

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 October 2012

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

SAICSIT '12

Sponsor:

UNISA
Microsoft
Pearson

SAICSIT '12: 2012 South African Institute of Computer Scientists and Information Technologists Conference

October 1 - 3, 2012

Pretoria, South Africa

Acceptance Rates

Overall Acceptance Rate 187 of 439 submissions, 43%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

30
Total Citations
View Citations
309
Total Downloads

Downloads (Last 12 months)25
Downloads (Last 6 weeks)1

Reflects downloads up to 12 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Zhang YXie XLi YLin YChen SLiu YLi X(2023)Demystifying Performance Regressions in String SolversIEEE Transactions on Software Engineering10.1109/TSE.2022.316837349:3(947-961)Online publication date: 1-Mar-2023
https://doi.org/10.1109/TSE.2022.3168373
Lotz KKulczynski MNowotka DPoulsen DSchlichtkrull A(2023)Verified Verifying: SMT-LIB for Strings in IsabelleImplementation and Application of Automata10.1007/978-3-031-40247-0_15(206-217)Online publication date: 10-Aug-2023
https://doi.org/10.1007/978-3-031-40247-0_15
Berzish MDay JGanesh VKulczynski MManea FMora FNowotka D(2022)Towards more efficient methods for solving regular-expression heavy string constraintsTheoretical Computer Science10.1016/j.tcs.2022.12.009Online publication date: Dec-2022
https://doi.org/10.1016/j.tcs.2022.12.009
Mues MHowar FDierl S(2022)SPouT: Symbolic Path Recording During Testing - A Concolic Executor for the JVMSoftware Engineering and Formal Methods10.1007/978-3-031-17108-6_6(91-107)Online publication date: 26-Sep-2022
https://dl.acm.org/doi/10.1007/978-3-031-17108-6_6
Mues MHowar FGrundy J(2021)Data-driven design and evaluation of SMT meta-solving strategiesProceedings of the 36th IEEE/ACM International Conference on Automated Software Engineering10.1109/ASE51524.2021.9678881(179-190)Online publication date: 15-Nov-2021
https://dl.acm.org/doi/10.1109/ASE51524.2021.9678881
Mora FBerzish MKulczynski MNowotka DGanesh V(2021)Z3str4: A Multi-armed String SolverFormal Methods10.1007/978-3-030-90870-6_21(389-406)Online publication date: 10-Nov-2021
https://doi.org/10.1007/978-3-030-90870-6_21
Berzish MKulczynski MMora FManea FDay JNowotka DGanesh V(2021)An SMT Solver for Regular Expressions and Linear Arithmetic over String LengthComputer Aided Verification10.1007/978-3-030-81688-9_14(289-312)Online publication date: 15-Jul-2021
https://doi.org/10.1007/978-3-030-81688-9_14
Winterer DZhang CSu Z(2020)On the unusual effectiveness of type-aware operator mutations for testing SMT solversProceedings of the ACM on Programming Languages10.1145/34282614:OOPSLA(1-25)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3428261
Trinh MChu DJaffar J(2020)Inter-theory dependency analysis for SMT string solversProceedings of the ACM on Programming Languages10.1145/34282604:OOPSLA(1-27)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3428260
Yefet NAlon UYahav E(2020)Adversarial examples for models of codeProceedings of the ACM on Programming Languages10.1145/34282304:OOPSLA(1-30)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3428230
Show More Cited By

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents