research-article

Higher-order test generation

Author:

Patrice GodefroidAuthors Info & Claims

PLDI '11: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation

Pages 258 - 269

https://doi.org/10.1145/1993498.1993529

Published: 04 June 2011 Publication History

Abstract

Symbolic reasoning about large programs is bound to be imprecise. How to deal with this imprecision is a fundamental problem in program analysis. Imprecision forces approximation. Traditional static program verification builds "may" over-approximations of the program behaviors to check universal "for-all-paths" properties, while automatic test generation requires "must" under-approximations to check existential "for-some-path" properties.

In this paper, we introduce a new approach to test generation where tests are derived from validity proofs of first-order logic formulas, rather than satisfying assignments of quantifier-free first-order logic formulas as usual. Two key ingredients of this higher-order test generation are to (1) represent complex/unknown program functions/instructions causing imprecision in symbolic execution by uninterpreted functions, and (2) record uninterpreted function samples capturing input-output pairs observed at execution time for those functions. We show that higher-order test generation generalizes and is more precise than simplifying complex symbolic expressions using their concrete runtime values. We present several program examples where our approach can exercise program paths and find bugs missed by previous techniques. We discuss the implementability and applications of this approach. We also explain in what sense dynamic test generation is more powerful than static test generation.

References

[1]

S. Anand, P. Godefroid, and N. Tillmann. Demand-Driven Compositional Symbolic Execution. In Proceedings of TACAS'2008, volume 4963 of Lecture Notes in Computer Science, pages 367--381, Budapest, April 2008. Springer-Verlag.

Digital Library

[2]

S. Artzi, A. Kiezun, J. Dolby, F. Tip, D. Dig, A. M. Paradkar, and M. D. Ernst. Finding Bugs in Web Applications Using Dynamic Test Generation and Explicit-State Model Checking. IEEE Trans. Software Eng., 36(4):474--494, 2010.

Digital Library

[3]

L. Bachmair and H. Ganzinger. Resolution Theorem Proving. In Handbook of Automated Reasoning, pages 19--99. 2001.

Digital Library

[4]

M. Barnett, B. E. Chang, R. DeLine, B. Jacobs, and K. R. M. Leino. Boogie: A modular reusable verifier for object-oriented programs. In Proceedings of FMCO'2005, volume 4111 of Lecture Notes in Computer Science, pages 364--387. Springer-Verlag, September 2006.

Digital Library

[5]

A. Blass, Y. Gurevich, L. Nachmanson, and M. Veanes. Play to Test. In Proceedings of FATES'2005, Edinburgh, July 2005.

Digital Library

[6]

C. Cadar, V. Ganesh, P. M. Pawlowski, D. L. Dill, and D. R. Engler. EXE: Automatically Generating Inputs of Death. In ACM CCS, 2006.

Digital Library

[7]

C. Cadar, P. Godefroid, S. Khurshid, C.S. Pasareanu, K. Sen, N. Tillmann, and W. Visser. Symbolic Execution for Software Testing in Practice -- Preliminary Assessment. In Proceedings of ICSE'2011, Honolulu, May 2011.

Digital Library

[8]

S. Chandra, S. J. Fink, and M. Sridharan. Snugglebug: A Powerful Approach to Weakest Preconditions. In Proceedings of PLDI'2009, Dublin, June 2009.

Digital Library

[9]

L. de Moura and N. Bjorner. Z3: An Efficient SMT Solver. In Proceedings of TACAS'2008, volume 4963 of Lecture Notes in Computer Science, pages 337--340, Budapest, April 2008. Springer-Verlag.

Digital Library

[10]

M. Emmi, R. Majumdar, and K. Sen. Dynamic Test Input Generation for Database Applications. In Proceedings of ISSTA'2007, pages 151--162, 2007.

Digital Library

[11]

P. Godefroid. Compositional Dynamic Test Generation. In Proceedings of POPL'2007, pages 47--54, Nice, January 2007.

Digital Library

[12]

P. Godefroid. Software Model Checking Improving Security of a Billion Computers. In Proceedings of SPIN'2009, volume 5578 of Lecture Notes in Computer Science, page 1, Grenoble, June 2009. Springer-Verlag.

Digital Library

[13]

P. Godefroid, M. Huth, and R. Jagadeesan. Abstraction-based Model Checking using Modal Transition Systems. In Proceedings of CONCUR'2001, volume 2154 of Lecture Notes in Computer Science, pages 426--440, Aalborg, August 2001. Springer-Verlag.

Digital Library

[14]

P. Godefroid, A. Kiezun, and M. Y. Levin. Grammar-based Whitebox Fuzzing. In Proceedings of PLDI'2008, pages 206--215, Tucson, June 2008.

Digital Library

[15]

P. Godefroid, N. Klarlund, and K. Sen. DART: Directed Automated Random Testing. In Proceedings of PLDI'2005, pages 213--223, Chicago, June 2005.

Digital Library

[16]

P. Godefroid, M.Y. Levin, and D. Molnar. Automated Whitebox Fuzz Testing. In Proceedings of NDSS'2008, pages 151--166, San Diego, February 2008.

[17]

P. Godefroid, A.V. Nori, S.K. Rajamani, and S.D. Tetali. Compositional May-Must Program Analysis: Unleashing The Power of Alternation. In Proceedings of POPL'2010, pages 43--55, Madrid, January 2010.

Digital Library

[18]

J. Hoenicke, K. R. M. Leino, A. Podelski, M. Schaf, and Th. Wies. It's doomed; we can prove it. In Proceedings of 2009 World Congress on Formal Methods, 2009.

Digital Library

[19]

Sarfraz Khurshid, Corina S. Păsăreanu, and Willem Visser. Generalized Symbolic Execution for Model Checking and Testing. In Proceeding of TACAS'2003, April 2003.

Digital Library

[20]

J. C. King. Symbolic Execution and Program Testing. Journal of the ACM, 19(7):385--394, 1976.

Digital Library

[21]

B. Korel. A Dynamic Approach of Test Data Generation. In IEEE Conference on Software Maintenance, pages 311--317, San Diego, November 1990.

[22]

D. Molnar, X. C. Li, and D. Wagner. Dynamic test generation to find integer bugs in x86 binary linux programs. In Proc. of the 18th Usenix Security Symposium, Aug 2009.

Digital Library

[23]

P. Saxena, D. Akhawe, S. Hanna, F. Mao, S. McCamant, and D. Song. A Symbolic Execution Framework for JavaScript. In IEEE Symposium on Security and Privacy, pages 513--528, 2010.

Digital Library

[24]

N. Tillmann and J. de Halleux. Pex - White Box Test Generation for .NET. In Proceedings of TAP'2008, volume 4966 of Lecture Notes in Computer Science, pages 134--153. Springer-Verlag, April 2008.

Digital Library

[25]

M. Yannakakis. Testing, Optimization, and Games. In Proceedings of LICS'2004, pages 78--88, Turku, July 2004.

Digital Library

Cited By

Lacombe GFeliot DBoespflug EPotet M(2023)Combining static analysis and dynamic symbolic execution in a toolchain to detect fault injection vulnerabilitiesJournal of Cryptographic Engineering10.1007/s13389-023-00310-814:1(147-164)Online publication date: 18-Jan-2023
https://doi.org/10.1007/s13389-023-00310-8
Girol GFarinier BBardin S(2022)Introducing robust reachabilityFormal Methods in System Design10.1007/s10703-022-00402-xOnline publication date: 21-Nov-2022
https://doi.org/10.1007/s10703-022-00402-x
Luo LZeng QYang BZuo FWang J(2021)Westworld: Fuzzing-Assisted Remote Dynamic Symbolic Execution of Smart Apps on IoT Cloud PlatformsProceedings of the 37th Annual Computer Security Applications Conference10.1145/3485832.3488022(982-995)Online publication date: 6-Dec-2021
https://dl.acm.org/doi/10.1145/3485832.3488022
Show More Cited By

Index Terms

Higher-order test generation

Recommendations

Higher-order test generation
PLDI '11

Symbolic reasoning about large programs is bound to be imprecise. How to deal with this imprecision is a fundamental problem in program analysis. Imprecision forces approximation. Traditional static program verification builds "may" over-approximations ...
Higher-order abstract syntax in classical higher-order logic
LFMTP '09: Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice

Higher-Order Abstract Syntax, or HOAS, is a technique for using a higher-order logic as a metalanguage for an object language with binding operators. It avoids formalizing syntactic details related to variable binding. This paper gives an extension to ...
Automating relatively complete verification of higher-order functional programs
POPL '13

We present an automated approach to relatively completely verifying safety (i.e., reachability) property of higher-order functional programs. Our contribution is two-fold. First, we extend the refinement type system framework employed in the recent work ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

PLDI '11: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation

June 2011

668 pages

ISBN:9781450306638

DOI:10.1145/1993498

General Chair:
Mary Hall
University of Utah
,
Program Chair:
David Padua
University of Illinois at Urbana-Champaign

ACM SIGPLAN Notices Volume 46, Issue 6
PLDI '11
June 2011
652 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1993316
Issue’s Table of Contents

Copyright © 2011 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

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 04 June 2011

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

PLDI '11

Sponsor:

SIGPLAN

PLDI '11: ACM SIGPLAN Conference on Programming Language Design and Implementation

June 4 - 8, 2011

California, San Jose, USA

Acceptance Rates

Overall Acceptance Rate 406 of 2,067 submissions, 20%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

37
Total Citations
View Citations
530
Total Downloads

Downloads (Last 12 months)7
Downloads (Last 6 weeks)0

Reflects downloads up to 01 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Lacombe GFeliot DBoespflug EPotet M(2023)Combining static analysis and dynamic symbolic execution in a toolchain to detect fault injection vulnerabilitiesJournal of Cryptographic Engineering10.1007/s13389-023-00310-814:1(147-164)Online publication date: 18-Jan-2023
https://doi.org/10.1007/s13389-023-00310-8
Girol GFarinier BBardin S(2022)Introducing robust reachabilityFormal Methods in System Design10.1007/s10703-022-00402-xOnline publication date: 21-Nov-2022
https://doi.org/10.1007/s10703-022-00402-x
Luo LZeng QYang BZuo FWang J(2021)Westworld: Fuzzing-Assisted Remote Dynamic Symbolic Execution of Smart Apps on IoT Cloud PlatformsProceedings of the 37th Annual Computer Security Applications Conference10.1145/3485832.3488022(982-995)Online publication date: 6-Dec-2021
https://dl.acm.org/doi/10.1145/3485832.3488022
Ge XNiu BBrotzman RChen YHan HGodefroid PCui WKim YKim JVigna GShi E(2021)HyperFuzzer: An Efficient Hybrid Fuzzer for Virtual CPUsProceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security10.1145/3460120.3484748(366-378)Online publication date: 12-Nov-2021
https://dl.acm.org/doi/10.1145/3460120.3484748
Li PMeng WLu KLuo C(2021)On the Feasibility of Automated Built-in Function Modeling for PHP Symbolic ExecutionProceedings of the Web Conference 202110.1145/3442381.3450002(58-69)Online publication date: 19-Apr-2021
https://dl.acm.org/doi/10.1145/3442381.3450002
Karim IHussain SBertino E(2021)ProChecker: An Automated Security and Privacy Analysis Framework for 4G LTE Protocol Implementations2021 IEEE 41st International Conference on Distributed Computing Systems (ICDCS)10.1109/ICDCS51616.2021.00079(773-785)Online publication date: Jul-2021
https://doi.org/10.1109/ICDCS51616.2021.00079
Girol GFarinier BBardin S(2021)Not All Bugs Are Created Equal, But Robust Reachability Can Tell the DifferenceComputer Aided Verification10.1007/978-3-030-81685-8_32(669-693)Online publication date: 15-Jul-2021
https://doi.org/10.1007/978-3-030-81685-8_32
Godefroid P(2020)FuzzingCommunications of the ACM10.1145/336382463:2(70-76)Online publication date: 22-Jan-2020
https://dl.acm.org/doi/10.1145/3363824
Pandey AKotcharlakota PRoy SZhang DMøller A(2019)Deferred concretization in symbolic execution via fuzzingProceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3293882.3330554(228-238)Online publication date: 10-Jul-2019
https://dl.acm.org/doi/10.1145/3293882.3330554
Candea GGodefroid P(2019)Automated Software Test Generation: Some Challenges, Solutions, and Recent AdvancesComputing and Software Science10.1007/978-3-319-91908-9_24(505-531)Online publication date: 2019
https://doi.org/10.1007/978-3-319-91908-9_24
Show More Cited By

View Options

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