jFuzz: A Concolic Whitebox Fuzzer for JavaWe present jFuzz, a automatic testing tool for Java programs. jFuzz is a concolic whitebox fuzzer, built on the NASA Java PathFinder, an explicit-state Java model checker, and a framework for developing reliability and analysis tools for Java. Starting from a seed input, jFuzz automatically and systematically generates inputs that exercise new program paths. jFuzz uses a combination of concrete and symbolic execution, and constraint solving. Time spent on solving constraints can be significant. We implemented several well-known optimizations and name-independent caching, which aggressively normalizes the constraints to reduce the number of calls to the constraint solver. We present preliminary results due to the optimizations, and demonstrate the effectiveness of jFuzz in creating good test inputs. The source code of jFuzz is available as part of the NASA Java PathFinder. jFuzz is intended to be a research testbed for investigating new testing and analysis techniques based on concrete and symbolic execution. The source code of jFuzz is available as part of the NASA Java PathFinder.
Jayaraman, Karthick (Syracuse Univ. NY, United States)
Harvison, David (Massachusetts Inst. of Tech. Cambridge, MA, United States)
Ganesh, Vijay (Massachusetts Inst. of Tech. Cambridge, MA, United States)
Kiezun, Adam (Massachusetts Inst. of Tech. Cambridge, MA, United States)
August 24, 2013
April 1, 2009
Publication: Proceedings of the First NASA Formal Methods Symposium