More Web Proxy on the site http://driver.im/

research-article

Public Access

Badger: complexity analysis with fuzzing and symbolic execution

Authors:

Corina S. PăsăreanuAuthors Info & Claims

ISSTA 2018: Proceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis

Pages 322 - 332

https://doi.org/10.1145/3213846.3213868

Published: 12 July 2018 Publication History

Abstract

Hybrid testing approaches that involve fuzz testing and symbolic execution have shown promising results in achieving high code coverage, uncovering subtle errors and vulnerabilities in a variety of software applications. In this paper we describe Badger - a new hybrid approach for complexity analysis, with the goal of discovering vulnerabilities which occur when the worst-case time or space complexity of an application is significantly higher than the average case.

Badger uses fuzz testing to generate a diverse set of inputs that aim to increase not only coverage but also a resource-related cost associated with each path. Since fuzzing may fail to execute deep program paths due to its limited knowledge about the conditions that influence these paths, we complement the analysis with a symbolic execution, which is also customized to search for paths that increase the resource-related cost. Symbolic execution is particularly good at generating inputs that satisfy various program conditions but by itself suffers from path explosion. Therefore, Badger uses fuzzing and symbolic execution in tandem, to leverage their benefits and overcome their weaknesses.

We implemented our approach for the analysis of Java programs, based on Kelinci and Symbolic PathFinder. We evaluated Badger on Java applications, showing that our approach is significantly faster in generating worst-case executions compared to fuzzing or symbolic execution on their own.

References

[1]

Elvira Albert, Puri Arenas, Samir Genaim, and Germán Puebla. 2011. Closed-Form Upper Bounds in Static Cost Analysis. Journal of Automated Reasoning 46, 2 (February 2011), 161–203.

Digital Library

[2]

Glenn Ammons, Jong-Deok Choi, Manish Gupta, and Nikhil Swamy. 2004. Finding and Removing Performance Bottlenecks in Large Systems. In ECOOP 2004 - Object-Oriented Programming. 170–194.

[3]

ASM. 2017. http://asm.ow2.org/. Accessed August 11, 2017.

[4]

Pietro Braione, Giovanni Denaro, Andrea Mattavelli, and Mauro Pezzè. 2017. Combining Symbolic Execution and Search-based Testing for Programs with Complex Heap Inputs. In Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2017). ACM, New York, NY, USA, 90–101.

Digital Library

[5]

J. Burnim, S. Juvekar, and K. Sen. 2009. WISE: Automated test generation for worst-case complexity. In 2009 IEEE 31st International Conference on Software Engineering. 463–473.

Digital Library

[6]

Cristian Cadar, Daniel Dunbar, and Dawson Engler. 2008. KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In Proceedings of the 8th USENIX conference on Operating systems design and implementation (OSDI’08). USENIX Association, Berkeley, CA, USA, 209–224. http://dl.acm.org/citation.cfm?id=1855741.1855756

Digital Library

[7]

Sang Kil Cha, Thanassis Avgerinos, Alexandre Rebert, and David Brumley. 2012. Unleashing Mayhem on Binary Code. In Proceedings of the 2012 IEEE Symposium on Security and Privacy (SP ’12). IEEE Computer Society, Washington, DC, USA, 380–394.

Digital Library

[8]

Bihuan Chen, Yang Liu, and Wei Le. 2016. Generating performance distributions via probabilistic symbolic execution. In Proceedings of the 38th International Conference on Software Engineering, ICSE 2016, Austin, TX, USA, May 14-22, 2016.

Digital Library

[9]

49–60.

[10]

Vitaly Chipounov, Volodymyr Kuznetsov, and George Candea. 2011. S2E: A Platform for In-vivo Multi-path Analysis of Software Systems. In Proceedings of the Sixteenth International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS XVI). ACM, New York, NY, USA, 265–278.

Digital Library

[11]

L. A. Clarke. 1976. A System to Generate Test Data and Symbolically Execute Programs. IEEE Trans. Softw. Eng. 2, 3 (May 1976), 215–222. 1109/TSE.1976.233817

Digital Library

[12]

Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: an efficient SMT solver. In Proceedings of the 14th international conference on Tools and algorithms for the construction and analysis of systems (TACAS’08). Springer-Verlag, Berlin, Heidelberg, 337–340. http://dl.acm.org/citation.cfm?id=1792734.1792766

Digital Library

[13]

J. P. Galeotti, G. Fraser, and A. Arcuri. 2013. Improving search-based test suite generation with dynamic symbolic execution. In 2013 IEEE 24th International Symposium on Software Reliability Engineering (ISSRE). 360–369.

[14]

Patrice Godefroid, Nils Klarlund, and Koushik Sen. 2005. DART: directed automated random testing (PLDI ’05). ACM, 213–223.

Digital Library

[15]

1065036

[16]

Patrice Godefroid, Michael Y. Levin, and David Molnar. 2012. SAGE: Whitebox Fuzzing for Security Testing. Queue 10, 1, Article 20 (Jan. 2012), 8 pages.

Digital Library

[17]

Susan L. Graham, Peter B. Kessler, and Marshall K. Mckusick. 1982. Gprof: A Call Graph Execution Profiler. In Proceedings of the 1982 SIGPLAN Symposium on Compiler Construction (SIGPLAN ’82). ACM, 120–126.

Digital Library

[18]

BhargavS. Gulavani and Sumit Gulwani. 2008. A Numerical Abstract Domain Based on Expression Abstraction and Max Operator with Application in Timing Analysis. In Computer Aided Verification, Aarti Gupta and Sharad Malik (Eds.). Lecture Notes in Computer Science, Vol. 5123. Springer Berlin Heidelberg, 370– 384.

Digital Library

[19]

Sumit Gulwani. 2009. SPEED: Symbolic Complexity Bound Analysis. In CAV ’09: Proceedings of the 21st International Conference on Computer Aided Verification. Springer, 51–62.

Digital Library

[20]

Jan Gustafsson, Andreas Ermedahl, Christer Sandberg, and Bjorn Lisper. 2006. Automatic Derivation of Loop Bounds and Infeasible Paths for WCET Analysis Using Abstract Execution. In Proceedings of the 27th IEEE International Real-Time Systems Symposium (RTSS ’06). IEEE Computer Society, Washington, DC, USA, 57–66.

Digital Library

[21]

Christopher Healy, Mikael Sjödin, Viresh Rustagi, David Whalley, and Robert Van Engelen. 2000. Supporting Timing Analysis by Automatic Bounding of LoopIterations. Real-Time Syst. 18, 2/3 (May 2000), 129–156. 1008189014032

Digital Library

[22]

Rody Kersten, Kasper Luckow, and Corina S. Păsăreanu. 2017. POSTER: AFLbased Fuzzing for Java with Kelinci. In Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security (CCS ’17). ACM, New York, NY, USA, 2511–2513.

Digital Library

[23]

James C. King. 1976. Symbolic execution and program testing. Commun. ACM 19, 7 (July 1976), 385–394.

Digital Library

[24]

Yau-Tsun Steven Li, Sharad Malik, and Benjamin Ehrenberg. 1998. Performance Analysis of Real-Time Embeded Software. Kluwer Academic Publishers, Norwell, MA, USA.

Digital Library

[25]

Kasper Luckow, Rody Kersten, and Corina Pasareanu. 2017. Symbolic Complexity Analysis using Context-preserving Histories. In Proceedings of the 10th IEEE International Conference on Software Testing, Verification and Validation (ICST 2017). 58–68.

[26]

Theofilos Petsios, Jason Zhao, Angelos D. Keromytis, and Suman Jana. 2017. SlowFuzz: Automated Domain-Independent Detection of Algorithmic Complexity Vulnerabilities. In Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security (CCS ’17). ACM, New York, NY, USA, 2155–2168.

Digital Library

[27]

Corina S. Păsăreanu, Quoc-Sang Phan, and Pasquale Malacaria. 2016. Multi-run Side-Channel Analysis Using Symbolic Execution and Max-SMT. In Proceedings of the 2016 IEEE 29th Computer Security Foundations Symposium (CSF ’16). IEEE Computer Society, Washington, DC, USA, 387–400. 2016.34

[28]

Corina S. Păsăreanu, Willem Visser, David Bushnell, Jaco Geldenhuys, Peter Mehlitz, and Neha Rungta. 2013. Symbolic PathFinder: integrating symbolic execution with model checking for Java bytecode analysis. Automated Software Engineering (2013), 1–35.

[29]

Koushik Sen, Darko Marinov, and Gul Agha. 2005. CUTE: a concolic unit testing engine for C. In Proceedings of the 13th ACM SIGSOFT international symposium on Foundations of software engineering (ESEC/FSE-13). ACM, New York, NY, USA, 263–272.

Digital Library

[30]

K Serebryany. {n. d.}. Libfuzzer: A library for coverage-guided fuzz testing (within llvm). http://llvm.org/docs/LibFuzzer.html.

[31]

Gary Sevitsky, Wim De Pauw, and Ravi Konuru. 2001. An Information Exploration Tool for Performance Analysis of Java Programs. In TOOLS Europe 2001: 38th International Conference on Technology of Object-Oriented Languages and Systems, Components for Mobile Computing. 85–101.

Digital Library

[32]

Olha Shkaravska, Rody Kersten, and Marko Van Eekelen. 2010. Test-Based Inference of Polynomial Loop-Bound Functions. In PPPJ’10: Proceedings of the 8th International Conference on the Principles and Practice of Programming in Java (ACM Digital Proceedings Series), Andreas Krall and Hanspeter Mössenböck (Eds.). 99–108.

Digital Library

[33]

Nick Stephens, John Grosen, Christopher Salls, Andrew Dutcher, Ruoyu Wang, Jacopo Corbetta, Yan Shoshitaishvili, Christopher Kruegel, and Giovanni Vigna. 2016. Driller: Augmenting Fuzzing Through Selective Symbolic Execution. In 23nd Annual Network and Distributed System Security Symposium, NDSS 2016, San Diego, California, USA, February 21-24, 2016. http://www.internetsociety.org/ sites/default/files/blogs-media/driller-augmenting-fuzzing-through-selectivesymbolic-execution.pdf

[34]

Website. 2012. Regular Expressions. http: // www.mkyong .com /regularexpressions/10-java-regular-expression-examples-you-should-know/.

[35]

Website. 2015. DARPA’s Space-Time Analysis for Cybersecurity program. http: //www.darpa.mil/program/space-time-analysis-for-cybersecurity.

[36]

Website. 2015. Debian Bug report log 800564 – php5: trivial hash complexity DoS attack. https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=800564. Accessed Jan 28, 2018.

[37]

Website. 2016. Cyber Grand Challenge Archive. http://archive.darpa.mil/ cybergrandchallenge/.

[38]

Website. 2016. DARPA Cyber Grand Challenge. https://www.darpa.mil/newsevents/2016-08-04.

[39]

Website. 2016. Microsoft Security Risk Detection. https://www.microsoft.com/ en-us/security-risk-detection/.

[40]

Website. 2017. OSS-Fuzz: Five months later, and rewarding projects. https:// testing.googleblog.com/2017/05/oss-fuzz-five-months-later-and.html. Accessed Jan 28, 2018.

[41]

Reinhard Wilhelm. 2009. Determining Bounds on Execution Times. In Embedded Systems Design and Verification - Volume 1 of the Embedded Systems Handbook. 9.

[42]

Guowei Yang, Corina S. Păsăreanu, and Sarfraz Khurshid. 2012. Memoized Symbolic Execution. In Proceedings of the 2012 International Symposium on Software Testing and Analysis (ISSTA 2012). ACM, New York, NY, USA, 144–154.

Digital Library

[43]

Michal Zalewski. 2017. American Fuzzy Lop (AFL). http://lcamtuf.coredump.cx/ afl/. Accessed August 11, 2017.

Cited By

Wang ZBu DTian WCui B(2024)Analyzing and Discovering Spatial Algorithm Complexity Vulnerabilities in RecursionApplied Sciences10.3390/app1405185514:5(1855)Online publication date: 23-Feb-2024
https://doi.org/10.3390/app14051855
Alshmrany KAldughaim MBhayat ACordeiro L(2024)FuSeBMC v4: Improving Code Coverage with Smart Seeds via BMC, Fuzzing and Static AnalysisFormal Aspects of Computing10.1145/366533736:2(1-25)Online publication date: 20-May-2024
https://dl.acm.org/doi/10.1145/3665337
Kadron INoller YPadhye RBultan TPăsăreanu CSen K(2024)Fuzzing, Symbolic Execution, and Expert Guidance for Better TestingIEEE Software10.1109/MS.2023.323798141:1(98-104)Online publication date: 1-Jan-2024
https://dl.acm.org/doi/10.1109/MS.2023.3237981
Show More Cited By

Index Terms

Badger: complexity analysis with fuzzing and symbolic execution
1. Security and privacy
  1. Formal methods and theory of security
2. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Formal software verification
      2. Software defect analysis
        Software testing and debugging

Recommendations

Improving function coverage with munch: a hybrid fuzzing and directed symbolic execution approach
SAC '18: Proceedings of the 33rd Annual ACM Symposium on Applied Computing

Fuzzing and symbolic execution are popular techniques for finding vulnerabilities and generating test-cases for programs. Fuzzing, a blackbox method that mutates seed input values, is generally incapable of generating diverse inputs that exercise all ...
FDSE: Enhance Symbolic Execution by Fuzzing-based Pre-Analysis (Competition Contribution)
Fundamental Approaches to Software Engineering
Abstract
FDSE serves as an automatic test generation tool designed for C programs based on symbolic execution. FDSE employs fuzzing-based pre-analysis and combines static symbolic execution and dynamic symbolic execution to improve the effectiveness of ...
Accelerating Fuzzing through Prefix-Guided Execution

Coverage-guided fuzzing is one of the most effective approaches for discovering software defects and vulnerabilities. It executes all mutated tests from seed inputs to expose coverage-increasing tests. However, executing all mutated tests incurs ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ISSTA 2018: Proceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis

July 2018

379 pages

ISBN:9781450356992

DOI:10.1145/3213846

General Chair:
Frank Tip
Northeastern University, USA
,
Program Chair:
Eric Bodden
University of Paderborn, Germany / Fraunhofer IEM, Germany

Copyright © 2018 ACM.

© 2018 Association for Computing Machinery. ACM acknowledges that this contribution was authored or co-authored by an employee, contractor or affiliate of the United States government. As such, the United States Government retains a nonexclusive, royalty-free right to publish or reproduce this article, or to allow others to do so, for Government purposes only.

Sponsors

SIGSOFT: ACM Special Interest Group on Software Engineering

In-Cooperation

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 12 July 2018

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Conference

ISSTA '18

Sponsor:

SIGSOFT

ISSTA '18: International Symposium on Software Testing and Analysis

July 16 - 21, 2018

Amsterdam, Netherlands

Acceptance Rates

Overall Acceptance Rate 58 of 213 submissions, 27%

Upcoming Conference

ISSTA '25

Sponsor:
sigsoft

34th ACM SIGSOFT International Symposium on Software Testing and Analysis

June 25 - 28, 2025

Trondheim , Norway

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

40
Total Citations
View Citations
1,213
Total Downloads

Downloads (Last 12 months)220
Downloads (Last 6 weeks)33

Reflects downloads up to 07 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Wang ZBu DTian WCui B(2024)Analyzing and Discovering Spatial Algorithm Complexity Vulnerabilities in RecursionApplied Sciences10.3390/app1405185514:5(1855)Online publication date: 23-Feb-2024
https://doi.org/10.3390/app14051855
Alshmrany KAldughaim MBhayat ACordeiro L(2024)FuSeBMC v4: Improving Code Coverage with Smart Seeds via BMC, Fuzzing and Static AnalysisFormal Aspects of Computing10.1145/366533736:2(1-25)Online publication date: 20-May-2024
https://dl.acm.org/doi/10.1145/3665337
Kadron INoller YPadhye RBultan TPăsăreanu CSen K(2024)Fuzzing, Symbolic Execution, and Expert Guidance for Better TestingIEEE Software10.1109/MS.2023.323798141:1(98-104)Online publication date: 1-Jan-2024
https://dl.acm.org/doi/10.1109/MS.2023.3237981
Haltermann JJakobs MRichter CWehrheim H(2024)Parallel program analysis on path rangesScience of Computer Programming10.1016/j.scico.2024.103154238:COnline publication date: 1-Dec-2024
https://dl.acm.org/doi/10.1016/j.scico.2024.103154
Haltermann JWehrheim H(2024)Exchanging information in cooperative software validationSoftware and Systems Modeling (SoSyM)10.1007/s10270-024-01155-323:3(695-719)Online publication date: 1-Jun-2024
https://dl.acm.org/doi/10.1007/s10270-024-01155-3
Zhao XQu HXu JLi XLv WWang G(2024)A systematic review of fuzzingSoft Computing - A Fusion of Foundations, Methodologies and Applications10.1007/s00500-023-09306-228:6(5493-5522)Online publication date: 1-Mar-2024
https://dl.acm.org/doi/10.1007/s00500-023-09306-2
Nilizadeh ALeavens GPăsăreanu CNoller Y(2023)JMLKelinci+: Detecting Semantic Bugs and Covering Branches with Valid Inputs Using Coverage-guided Fuzzing and Runtime Assertion CheckingFormal Aspects of Computing10.1145/360753836:1(1-24)Online publication date: 5-Aug-2023
https://dl.acm.org/doi/10.1145/3607538
Li SSu Z(2023)Accelerating Fuzzing through Prefix-Guided ExecutionProceedings of the ACM on Programming Languages10.1145/35860277:OOPSLA1(1-27)Online publication date: 6-Apr-2023
https://dl.acm.org/doi/10.1145/3586027
Hassan SAamir ZLee DDavis JServant F(2023)Improving Developers’ Understanding of Regex Denial of Service Tools through Anti-Patterns and Fix Strategies2023 IEEE Symposium on Security and Privacy (SP)10.1109/SP46215.2023.10179442(1238-1255)Online publication date: May-2023
https://doi.org/10.1109/SP46215.2023.10179442
Wang XZhang CLi YXu ZHuang SLiu YYao YXiao YZou YLiu YHuo W(2023)Effective ReDoS Detection by Principled Vulnerability Modeling and Exploit Generation2023 IEEE Symposium on Security and Privacy (SP)10.1109/SP46215.2023.10179328(2427-2443)Online publication date: May-2023
https://doi.org/10.1109/SP46215.2023.10179328
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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

Media

Figures

Other

Tables

View Table of Contents