Yannic Noller
Rody Kersten
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.
- 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. Google Scholar
Digital Library
- 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.Google Scholar
- ASM. 2017. http://asm.ow2.org/. Accessed August 11, 2017.Google Scholar
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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 Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 49–60.Google Scholar
- 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. Google ScholarDigital Library
- 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 Google ScholarDigital Library
- 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 Google ScholarDigital Library
- 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.Google Scholar
- Patrice Godefroid, Nils Klarlund, and Koushik Sen. 2005. DART: directed automated random testing (PLDI ’05). ACM, 213–223. Google ScholarDigital Library
- 1065036Google Scholar
- Patrice Godefroid, Michael Y. Levin, and David Molnar. 2012. SAGE: Whitebox Fuzzing for Security Testing. Queue 10, 1, Article 20 (Jan. 2012), 8 pages. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Sumit Gulwani. 2009. SPEED: Symbolic Complexity Bound Analysis. In CAV ’09: Proceedings of the 21st International Conference on Computer Aided Verification. Springer, 51–62. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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 Google ScholarDigital Library
- 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. Google ScholarDigital Library
- James C. King. 1976. Symbolic execution and program testing. Commun. ACM 19, 7 (July 1976), 385–394. Google ScholarDigital Library
- Yau-Tsun Steven Li, Sharad Malik, and Benjamin Ehrenberg. 1998. Performance Analysis of Real-Time Embeded Software. Kluwer Academic Publishers, Norwell, MA, USA. Google ScholarDigital Library
- 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.Google ScholarCross Ref
- 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. Google ScholarDigital Library
- 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.34Google ScholarCross Ref
- 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.Google Scholar
- 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. Google ScholarDigital Library
- K Serebryany. {n. d.}. Libfuzzer: A library for coverage-guided fuzz testing (within llvm). http://llvm.org/docs/LibFuzzer.html.Google Scholar
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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.pdfGoogle Scholar
- Website. 2012. Regular Expressions. http: // www.mkyong .com /regularexpressions/10-java-regular-expression-examples-you-should-know/.Google Scholar
- Website. 2015. DARPA’s Space-Time Analysis for Cybersecurity program. http: //www.darpa.mil/program/space-time-analysis-for-cybersecurity.Google Scholar
- 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.Google Scholar
- Website. 2016. Cyber Grand Challenge Archive. http://archive.darpa.mil/ cybergrandchallenge/.Google Scholar
- Website. 2016. DARPA Cyber Grand Challenge. https://www.darpa.mil/newsevents/2016-08-04.Google Scholar
- Website. 2016. Microsoft Security Risk Detection. https://www.microsoft.com/ en-us/security-risk-detection/.Google Scholar
- 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.Google Scholar
- Reinhard Wilhelm. 2009. Determining Bounds on Execution Times. In Embedded Systems Design and Verification - Volume 1 of the Embedded Systems Handbook. 9.Google Scholar
- 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. Google ScholarDigital Library
- Michal Zalewski. 2017. American Fuzzy Lop (AFL). http://lcamtuf.coredump.cx/ afl/. Accessed August 11, 2017.Google Scholar
Index Terms
- Badger: complexity analysis with fuzzing and symbolic execution
Recommendations
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 ...
Improving function coverage with munch: a hybrid fuzzing and directed symbolic execution approach
SAC '18: Proceedings of the 33rd Annual ACM Symposium on Applied ComputingFuzzing 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 ...
A Survey of Hybrid Fuzzing based on Symbolic Execution
CIAT 2020: Proceedings of the 2020 International Conference on Cyberspace Innovation of Advanced TechnologiesFuzzing has now developed into an efficient method of vulnerability mining. Symbolic execution is also a popular software vulnerability mining technology. Both are research hotspots in the field of network and information security. Hybrid fuzzing is the ...
Comments