Testing Program Analyzers and Verifiers

In this talk, I presented our recent and ongoing work on enhancing grammar-based fuzzing via grammar mutation and repair.

Our project GMutator aims to generate edge inputs, particularly those incorrectly accepted by a program, via the novel concept of grammar mutation – where the grammar is first mutated before being used for fuzzing.

Our project AFLRepair combines grammar-based fuzzing with greybox fuzzing. To avoid input mutations leading to mostly invalid inputs, we combine standard byte-level mutations with a repair stage.

Both our projects found bugs that are out of reach of prior approaches.

C-to-RTL (register-transfer level) formal equivalence checkers (ECs) allow hardware implementations to be compared against software specifications. Thanks to their complete state-space coverage, ECs are trusted to authorise design sign-off. Therefore, ridding ECs of bugs is a top priority. In pursuit of this goal, we have developed Equifuzz, a technique and tool for randomized testing (fuzzing) of SystemC-to-RTL ECs. Equifuzz uses knowledge of SystemC semantics to generate rich designs that are known to be equivalent to trivial RTL designs. It has uncovered 7 unsoundness bugs in major commercial ECs (where the EC claimed equivalence incorrectly), and 5 incompleteness bugs (where the EC failed to prove equivalence between equivalent designs), all of which have been confirmed by the tool vendors. The fact that Equifuzz has been able to find serious bugs in extensively tested, major commercial ECs demonstrates that fuzzing is a valuable complement to the handcrafted tests that EC developers use as standard.

In order to aid quality assurance of large complex hardware architectures, system simulators have been developed. However, such system simulators do not always accurately mirror what would have happened on a real device. A significant challenge in testing these simulators comes from the complexity of having to model both the simulation and the infinite number of software that could be run on such a device.

Our previous work introduced SearchSYS, a testing framework for software simulators. SearchSYS leverages a large language model for initial seed C code generation which is then compiled, and the resultant binary is fed to a fuzzer. We then use differential testing by running the outputs of fuzzing on real hardware and a system simulator to identify mismatches.

In this talk, we present and discuss our solution to the problem of testing software simulators, using SearchSYS to test the gem5 VLSI digital circuit simulator, employed by ARM to test their systems. In particular, we focus on the simulation of the ARM silicon chip Instruction Set Architecture (ISA). SearchSYS can create test cases that activate bugs by combining LLMs, fuzzing, and differential testing. Using only LLM, SearchSYS identified 74 test cases that activated bugs. By incorporating fuzzing, this number increased by 93 additional bug-activating cases within 24 hours. Through differential testing, we identified 624 bugs with LLM-generated test cases and 126 with fuzzed test inputs. Out of the total number of bug-activating test cases, 4 unique bugs have been reported and acknowledged by developers. Additionally, we provided developers with a test case suite and fuzzing statistics, and open-sourced SearchSYS.

Program analyzers implement complex algorithms and, as any soft- ware, can contain bugs. Bugs in their implementation may lead to analyzers being imprecise and failing to verify safe programs, i.e., programs with no reachable error locations; or worse, analyzer bugs may lead to reporting unsound results by verifying unsafe programs, i.e., programs with reachable error locations.

In this paper, we propose a method to detect such bugs by gen- erating constraint-based test oracles for analyzers. We re-purpose and extend Fuzzle, a tool for benchmarking fuzzers, in a tool called Minotaur. Minotaur generates C programs from SMT constraints, and based on the satisfiability of the constraints, derives whether the generated programs are safe or unsafe. For instance, for an unsafe program, an analyzer under test contains a soundness issue if it proves it safe. Using Minotaur, we found 30 unique soundness and precision issues in 11 well-known analyzers that reason about reachability properties.

In this talk we will present and demo our “checkification” approach: a simple, automatic method for testing static analyzers. Broadly, it consists in checking that the properties inferred statically are satisfied dynamically. The main advantage of checkification lies in its simplicity, specially when framed within the Ciao assertion-based validation framework, which implements a blend of static and dynamic assertion checking.

We will demonstrate how in this setting analysis results can be tested with little effort by combining, via a simple program transformation, the basic components that comprise the framework itself: 1) the static analyzer, which outputs its results as the original program source with assertions interspersed; 2) the assertion run-time checking mechanism, which instruments a program to ensure that no assertion is violated at run time; 3) the random test case generator, which generates random test cases satisfying the properties present in assertion preconditions; and 4) the unit-testing framework, which executes those test cases. We will show the interaction of these components while checking the results of the CiaoPP abstract interpretation-based static analyzer, for several abstract domains for different properties, analysis (fixpoint) algorithms, etc.

Program analyzers are critical in safeguarding software reliability. However, due to their inherent complexity, they are likely to contain bugs themselves, and the question of how to detect them arises. Existing approaches, primarily based on specification-based, differential, or metamorphic testing, have been successful in finding analyzer bugs, but also come with certain limitations. In this paper, we present interrogation testing, a novel testing methodology for program analyzers, to address limitations in existing metamorphic-testing techniques. Specifically, interrogation testing introduces two key innovations by (1) incorporating more information from analyzer queries to construct more powerful oracles, and (2) introducing a knowledge base that maintains a history of diverse queries. We implemented interrogation testing in Sher- lock and tested 8 mature analyzers—including model checkers, abstract interpreters, and symbolic-execution engines—that can prove the safety of assertions in C/C++ programs. We found 24 unique issues in these analyzers, 16 of which are soundness related, i.e., an analyzer does not report an assertion that can be violated. Our experimental evaluation demonstrates Sherlock’s effectiveness by finding issues between 7x and 906x faster than our baseline, which is inspired by the state of the art.

In this talk, I will introduce our new program generator UBGen, which can generate C programs with various undefined behaviors, such as buffer overflows and null pointer dereferences. We have used UBGen to fuzz sanitizers (ASan, UBSan, and MSan) and have successfully detected more than 10 false negative bugs, where sanitizers failed to report the UB in programs.

Mopsa is a Modular Open Platform for Static Analysis, whose goal is to encourage research and education in static analysis, by providing a fully-featured and extensible open-source platform and usable analyses built with it. In particular, analyses in Mopsa can reach a high expressivity, thanks to a framework allowing an extensive use of relational domains, which are able to infer linear constraints between variables. In this talk, we will see a brief overview of Mopsa, our main design decisions and the results we have able to obtain so far.

Implementations of static analyzers are time-consuming to develop and to maintain, but necessary to enable building further research upon the implementation. This talk will present the tools and techniques we have come up with to simplify the maintenance of Mopsa. First, we describe an automated way to measure precision that does not require any manual inspection of the results, improves transparency of the analysis, and helps discovering regressions during continuous integration. Second, we have taken inspiration from standard tools observing the concrete execution of a program to design custom tools observing the abstract execution of the analyzed program itself, such as abstract debuggers and profilers. Finally, we report on some cases of automated testcase reduction.

Ensuring the correctness of SMT solvers is thus critical, as they serve as the cornerstone of a wide range of software engineering applications, from symbolic execution and program verification to program synthesis and repair. However, existing testing techniques, such as differential and metamorphic testing, have limitations: the former requires multiple solvers and is confined to shared functionality, while the latter is often restricted to simple, syntactic-preserving transformations. In this talk, I present DIVER, a technique that overcomes these limitations through semantic metamorphic testing. Unlike prior approaches, DIVER performs oracle-guided, unrestricted random mutations based on the semantic model of a formula, enabling it to uncover deep, solver-specific soundness and model-generation bugs that are out of reach for existing tools. Using DIVER, we have discovered 25 new bugs in Z3, CVC5, and dReal, including subtle logical errors that had persisted in production releases for years.

Quantum computing is a rapidly evolving field with the potential to revolutionize a wide range of industries. At the core of this revolution are quantum computing platforms, which – similar to traditional analyzers and compilers – analyze, optimize, and translate quantum programs. Unfortunately, like any complex software, these platforms are susceptible to bugs that can undermine the correctness and reliability of quantum applications. This talk presents two automated testing techniques designed to address this challenge. The first, MorphQ, is a metamorphic testing approach tailored to quantum computing platforms. It combines a generator of quantum input programs with a suite of program transformations that exploit quantum-specific metamorphic relationships to uncover inconsistencies. The second technique, QITE, introduces a cross-platform testing framework for quantum computing. It is based on a novel ITE process that generates equivalent quantum programs by iteratively (I) Importing assembly code into platform-specific representations, (T) Transforming the programs via platform-specific optimizations and gate conversions, and (E) Exporting them back to assembly. Both approaches have successfully identified a range of previously unknown bugs in widely used quantum computing platforms, including Qiskit, Pennylane, and Pytket, thereby contributing to the robustness and trustworthiness of this emerging field.

We present hevm, a symbolic execution engine for the EVM. hevm can prove safety properties for EVM bytecode or verify semantic equivalence between two bytecode objects. It exposes a user-friendly API in Solidity that allows end-users to define symbolic tests using almost the same syntax as they would for their usual unit tests. We evaluate our framework against state-of-the-art tools, using a comprehensive set of benchmarks. Our empirical findings demonstrate that hevm outperforms its counterparts, effectively solving a greater number of problems within competitive time frames.

Type checkers are the most widely used form of static analysis, helping us identify bugs in programs during development. However, bugs in type checkers themselves can harm the programmer experience and, more critically, pose security risks, especially when they compromise the soundness of the checker.

In this talk, we address one of the central challenges in program generation for testing type checkers: saturation. We introduce THALIA, a framework that leverages APIs from real-world software libraries to synthesize small client programs designed to stress-test type checker implementations. The strength of THALIA comes from the inherent complexity of modern APIs, which often depend on advanced typing features such as parametric polymorphism and overloading. By exploiting these APIs, THALIA produces programs that exercise sophisticated typing behaviors without the need to explicitly generate those features from scratch.

When applied to popular type checkers, THALIA uncovered dozens of previously unknown bugs, many of which had been missed by existing program generation techniques.

Thodoris Sotiropoulos (ETH Zürich, CH)

The first discussion panel of the seminar explored whether it is worthwhile to proactively test program analyzers and verifiers, particularly through techniques such as fuzzing. Arguments were presented on both sides. We clarify that these arguments do not suggest that program analyzers and verifiers do not matter. Instead, we question whether it is important to proactively test them using fuzzing to find edge case bugs.

Thodoris Sotiropoulos (ETH Zürich, CH)

This session discussed several topics proposed by the attendees during the seminar. The discussions were around the importance of faults in program analyzers/verifiers, bug de-duplication and prioritization, saturation of program generation, AI for testing, and performance testing of program analyzers/verifiers.