Finding More Property Violations in Model Checking via the Restart Policy

Model checking is an efficient formal verification technique that has been applied to a wide spectrum of applications in software engineering. Popular model checking algorithms include Bounded Model Checking (BMC) and Incremental Construction of Inductive Clauses for Indubitable Correctness/Property Directed Reachability(IC3/PDR). The recently proposed Complementary Approximate Reachability (CAR) model checking algorithm has a performance close to BMC in bug-finding, while its depth-first strategy sometimes leads the algorithm to a trap, which will waste lots of computation. In this paper, we enhance the recently proposed Complementary Approximate Reachability (CAR) model checking algorithm by integrating the restart policy, which yields a restartable CAR model (abbreviated as r-CAR). The restart policy can help avoid the trap problem caused by the depth-first strategy and has played an important role in modern SAT-solving algorithms to search for a satisfactory solution. As the bug-finding in model checking is reducible to a similar search problem, the restart policy can be useful to enhance the bug-finding capability. We made an extensive experiment to evaluate the new algorithm. Our results show that out of the 749 industrial instances, r-CAR is able to find 13 instances that the state-of-the-art BMC technique cannot find and can solve more than 11 instances than the original CAR. The new algorithm successfully contributes to the current model-checking portfolio in practice.

Not All Bugs Are Created Equal, But Robust Reachability Can Tell the Difference

This paper introduces a new property called robust reachability which refines the standard notion of reachability in order to take replicability into account. A bug is robustly reachable if a controlled input can make it so the bug is reached whatever the value of uncontrolled input. Robust reachability is better suited than standard reachability in many realistic situations related to security (e.g., criticality assessment or bug prioritization) or software engineering (e.g., replicable test suites and flakiness). We propose a formal treatment of the concept, and we revisit existing symbolic bug finding methods through this new lens. Remarkably, robust reachability allows differentiating bounded model checking from symbolic execution while they have the same deductive power in the standard case. Finally, we propose the first symbolic verifier dedicated to robust reachability: we use it for criticality assessment of 4 existing vulnerabilities, and compare it with standard symbolic execution.

Delay-Bounded Scheduling Without Delay!

We consider the broad problem of analyzing safety properties of asynchronous concurrent programs under arbitrary thread interleavings. Delay-bounded deterministic scheduling, introduced in prior work, is an efficient bug-finding technique to curb the large cost associated with full scheduling nondeterminism. In this paper we first present a technique to lift the delay bound for the case of finite-domain variable programs, thus adding to the efficiency of bug detection the ability to prove safety of programs under arbitrary thread interleavings. Second, we demonstrate how, combined with predicate abstraction, our technique can both refute and verify safety properties of programs with unbounded variable domains, even for unbounded thread counts. Previous work has established that, for non-trivial concurrency routines, predicate abstraction induces a highly complex abstract program semantics. Our technique, however, never statically constructs an abstract parametric program; it only requires some abstract-states set to be closed under certain actions, thus eliminating the dependence on the existence of verification algorithms for abstract programs. We demonstrate the efficiency of our technique on many examples used in prior work, and showcase its simplicity compared to earlier approaches on the unbounded-thread Ticket Lock protocol.

ConFuzz: Coverage-Guided Property Fuzzing for Event-Driven Programs

Bug-free concurrent programs are hard to write due to non-determinism arising out of concurrency and program inputs. Since concurrency bugs typically manifest under specific inputs and thread schedules, conventional testing methodologies for concurrent programs like stress testing and random testing, which explore random schedules, have a strong chance of missing buggy schedules.In this paper, we introduce a novel technique that combines property-based testing with mutation-based, grey box fuzzer, applied to event-driven OCaml programs. We have implemented this technique in , a directed concurrency bug-finding tool for event-driven OCaml programs. Using , programmers specify high-level program properties as assertions in the concurrent program. uses the popular greybox fuzzer AFL to generate inputs as well as concurrent schedules to maximise the likelihood of finding new schedules and paths in the program so as to make the assertion fail. does not require any modification to the concurrent program, which is free to perform arbitrary I/O operations. Our experimental results show that is easy-to-use, effective, detects concurrency bugs faster than Node.Fz - a random fuzzer for event-driven JavaScript programs, and is able to reproduce known concurrency bugs in widely used OCaml libraries.

Differential Testing of Static Analyzers

Program faults, best known as bugs, are practically unavoidable in today's ever growing software systems. One increasingly popular way of eliminating them, besides tests, dynamic analysis, and fuzzing, is using static analysis based bug-finding tools. Such tools are capable of finding surprisingly sophisticated bugs automatically by inspecting the source code. Their analysis is usually both unsound and incomplete, but still very useful in practice, as they can find non-trivial problems in a reasonable time (e.g. within hours, for an industrial project) without human intervention Because the problems that static analyzers try to solve are hard, usually intractable, they use various approximations that need to be fine-tuned in order to grant a good user experience (i.e. as many interesting bugs with as few distracting false alarms as possible). For each newly introduced heuristic, this normally happens by performing differential testing of the analyzer on a lot of widely used open source software projects that are known to use related language constructs extensively. In practice, this process is ad hoc, error-prone, poorly reproducible and its results are hard to share. We present a set of tools that aim to support the work of static analyzer developers by making differential testing easier. Our framework includes tools for automatic test suite selection, automated differential experiments, coverage information of increased granularity, statistics collection, metric calculations, and visualizations, all resulting in a convenient, shareable HTML report.

SHFuzz: Selective Hybrid Fuzzing with Branch Scheduling Based on Binary Instrumentation

Hybrid fuzzing is a popular software testing technique that combines random fuzzing with concolic execution. It is widely used in the security domain known for its ability to find deeply hidden vulnerabilities and reach high code coverage. Hybrid fuzzing is based on negating branches in the execution path of a specific input to generate new test cases. However, due to numerous inputs and related branches, it does not show the best of its effectiveness without input and branch selection methods. In this paper, we systematically analyze the branch scheduling problem in the internal attributes of hybrid fuzzing, focusing on the synchronization mechanism. To solve the problems, we propose the Selective Hybrid Fuzzing (SHF) approach with branch scheduling based on binary instrumentation. There are two major parts to the SHF approach: (1) we propose a critical branch selection algorithm to select critical branches by three metrics: hit accuracy, solvability, and complexity; (2) we propose a priority score calculation algorithm to select inputs by the number of critical branches. With the SHF approach, we choose only the branches that can be negated to generate new coverage, instead of repeatedly executing the same branches and generating duplicates of inputs. We implement a hybrid fuzzer called SHFuzz with our SHF approach and compare it with the state-of-the-art hybrid fuzzer QSYM. In the evaluation, SHFuzz outperforms QSYM in 20 real-world applications from the Google Fuzzer Test Suite and other program suites in a 12 h test. On average, SHFuzz achieves 8.40% more code coverage and 100 more unique crashes in each application. Our work also finds existing vulnerabilities 7.85× faster than QSYM. We also find new bugs by SHFuzz, which QSYM fails to find. Our evaluation shows that the selective hybrid fuzzing approach can reduce the number of branches executed in concolic execution, enhancing hybrid fuzzing on code coverage and bug finding capabilities.