JMLKelinci+: Detecting Semantic Bugs and Covering Branches with Valid Inputs using Coverage-Guided Fuzzing and Runtime Assertion Checking

Testing to detect semantic bugs is essential, especially for critical systems. Coverage-guided fuzzing and runtime assertion checking (RAC) are two well-known approaches for detecting semantic bugs. Coverage-guided fuzzing aims to generate inputs tests with high code coverage. However, while coverage-guided fuzzers are equipped with sanitizers that can detect a fixed set of semantic bugs, they can otherwise only detect bugs that lead to a crash. Thus, the first problem we address is how to help fuzzers detect previously unknown semantic bugs that do not lead to a crash. Moreover, a coverage-guided fuzzer may not necessarily cover all branches with valid inputs, although invalid inputs are useless for detecting semantic bugs.  So, the second problem is how to guide a fuzzer to cover all branches in a program using only valid inputs.  On the other hand, RAC monitors the expected behavior of a program dynamically and can only detect a semantic bug when a valid input test shows that the program does not satisfy its specification.  
Thus, the third problem is how to provide high-quality input tests for a RAC that can trigger potential bugs.
The combination of a coverage-guided fuzzer and RAC solves these problems and can cover branches with valid inputs and detect semantic bugs effectively. Our study uses RAC to guarantee that only valid inputs reach the program under test using the program's specified preconditions and it also uses RAC to detect semantic bugs using specified postconditions.  A prototype tool was developed for this study, named JMLKelinci+. Our results show that combining a coverage-guided fuzzer with RAC will lead to executing the program under test only with valid inputs and that this technique can effectively detect semantic bugs. 
Also, this idea improves the feedback given to a coverage-guided fuzzer, enabling it to cover all branches faster in programs with non-trivial preconditions.