While research on formal verification continues, fully automatic dynamic analysis of RPM packages is now available for Fedora users.

In 2019, Red Hat joined the AUFOVER (Automation of Formal Verification) project, which focused on fully automatic detection of bugs in complex software products based on formal verification. The project was driven by Honeywell and supported by the Technology Agency of the Czech Republic. At that time, Masaryk University and Brno University of Technology were developing formal verification tools primarily intended for research. The industrial partners Honeywell and Red Hat were working to make the research tools practically useful and integrate them into their business workflow.

Red Hat collaborated primarily with Masaryk University because they were developing the tools we were interested in, namely Divine, which uses explicit-state model checking, and Symbiotic, which combines instrumentation, slicing, and symbolic execution. Our task was to integrate the formal verification tools into our environment and use them to formally verify the software that we distribute in our Linux distributions (Fedora and Red Hat Enterprise Linux). Thanks to the AUFOVER project, these tools are now available in Fedora through a simple user interface.

For an earlier report on AUFOVER, see “Automated Formal Verification,” RHRQ 2:2 (August 2020).

Our Linux distributions consist of RPM packages. The RPM package manager is used to install and remove software components of the system. We took advantage of this packaging system and built the automation of formal verification on top of it. In addition to RPM packages that can be installed on the target system, there are so-called source RPM packages, which contain source code and machine-readable metadata describing how to build the software from source.

The source RPM packages can be processed by tools like rpmbuild and mock in a fully automatic way to produce binary RPM packages. We have developed RPM-based automation of formal verification that takes advantage of the machine-readable metadata as well as the existing tools for automatic builds of RPM packages. We run the tools in a modified run-time environment, however.

The formal verification tools Symbiotic and Divine perform formal verification of C programs. The C language ecosystem does not come with any native framework for a fully automatic build from source code. The presence of the metadata in source RPM packages was crucial for the success of the solution we developed. On the other hand, the RPM packaging was initially developed for the build and installation of programs. The inventors of the RPM packaging format did not take fully automatic formal verification of programs into account. To succeed with our task, we had to overcome a few technical obstacles.

The tools Symbiotic and Divine operate on the intermediate code of the LLVM compiler (so-called bitcode) rather than binary code for a specific architecture. However, we need to build the architecture-specific code, too, in order not to break the native build process. The binary files created by the compiler are often executed during the build, and the results they produce have a significant impact on the further build process. To address this problem, we modified the build environment such that the intermediate code is captured during the build and embedded directly into the resulting binaries. The intermediate code is later extracted from the binaries when the formal verification tools need it.

The presence of the metadata in source RPM packages was crucial for the success of the solution we developed.

Another problem we needed to solve is how to automatically trigger the formal verification tools on the captured intermediate code. The RPM packaging format does not include any metadata describing which binaries should be given which parameters upon execution. The situation is even worse with RPM packages that install dynamically linked libraries only. The dynamically linked libraries cannot be executed on their own. They need to be linked to binary executables at run time.

Luckily, modern RPM packages contain test suites that run during the build. The entry point for these tests is a shell script that may, in theory, do anything. In addition to executing the programs produced by the build of an RPM package, the script may use external testing frameworks and other programs installed on the system. 

Our goal was to trigger formal verification tools only for the programs produced by the build of the given RPM package. To achieve this goal, we used an innovative solution, csexec, based on wrapping the system dynamic linker. We also experimented with an alternative solution, ldpwrap, based on instrumentation of the main() function, as the commonly used entry point of C programs.

In both cases, the formal verification tool automatically launched upon each execution of a binary produced by the build of an RPM package, and the verification tool was given the original command-line arguments passed by the testing framework. In some cases, RPM packages contain a single test that executes multiple binaries in parallel, possibly communicating with each other, for example, through a pipe. Moreover, the tests themselves are often executed in parallel to deliver results faster. In such cases, the automatically triggered formal verification tools also run in parallel. Their results are being captured while the tools are running and subsequently serialized in a single file that contains all relevant results of the formal verification tools.

Thanks to the csmock tool, which we originally developed for static analysis of RPM packages, we were able to hide all the technical details mentioned above and offer our solution through a simple user interface. We have developed experimental csmock plugins (see Figure 1) for Symbiotic and Divine. Fedora users can just install a csmock plugin, run csmock with the plugin enabled, and wait for the results. Of course, csmock does not remove any limitations of the verification tools, like memory and time complexity or annotation requirements. Still, csmock makes it much easier to evaluate formal verification tools on RPM packages and, consequently, on a Linux distribution.

The formal verification did not finish successfully in the vast majority of RPM packages we tried. Instead, we optimized the automation to deliver at least partial results in a predictable amount of time. This is achieved by specifying a timeout for a single run of a formal verification tool. By default, the timeout is set to 30 seconds. For more complex RPM packages with higher test coverage, we needed to decrease the timeout value to get the results in a reasonable time. 

Our most expensive experiment was the formal verification of coreutils-8.32-31.fc35 with Symbiotic, where the formal verification job took approximately eight hours on a machine with 16 CPU cores, even though the timeout was set to only eight seconds. This was primarily caused by the fact that, during the formal verification of a single RPM package, Symbiotic was triggered 24,470 times in total. To increase the search depth, we would need to increase the timeout value—at the cost of waiting longer for the results—or use more powerful hardware. As initially expected, we hit the obstacle of the excessive time complexity of formal verification.

All the interesting results of our experiments with formal verification of RPM packages are publicly available on GitHub, including an evaluation framework that can be used to reproduce our results on any Fedora system with sufficient performance. I would also like to highlight that Symbiotic was successful at the 11th Competition on Software Verification (SV-COMP 2022), winning three gold medals and one bronze. This success confirms that we selected the right tools to experiment with. 

While the formal verification tools are still under research, the tooling we developed for automation is already practically useful. Thanks to our dynamic linker wrapper (csexec), we could extend covscan, our internal service for static analysis of RPM packages, to support fully automatic dynamic analysis with the tools Valgrind and strace.

Based on our experiments with bigger software projects, the developers of Symbiotic decided to work further on improving the tool so that it handles more practical use cases. The automation we developed will help us to monitor progress on this effort.