Formal verification of RPM packages with CBMC, Divine, and Symbiotic is now easier than ever before! csmock plug-ins for these tools are now available in stable Fedora releases. The plug-ins are still experimental and they have some technical limitations:
- They work only for source RPM packages that contain the %check section that directly or indirectly invokes the binaries produced in the %build section.
- The tools are known to work reliably only for programs written in C.
- Only one formal verification tool can be enabled in one run of csmock.
- Only *-x86_64 build roots are supported for now.
- The fedora-rawhide-x86_64 build root is not supported at the moment.
The plug-ins can be installed on a Fedora system using the following command:
$ sudo dnf install csmock-plugin-{cbmc,divine,symbiotic}
Then you can formally verify RPM packages of your choice:
$ csmock -r fedora-35-x86_64 -t ${tool} ${pkg}.src.rpm
These plug-ins were developed as part of the AUFOVER (Automation of Formal Verification) research project:
https://research.redhat.com/blog/research_project/aufover-2/
Some useful tips can be found on the aufover/experiments wiki:
https://github.com/aufover/experiments
If you run into any issues please do not hesitate to reach out to us. We welcome any feedback you may have as it will help us make further improvements to the tools.
Kamil and the AUFOVER team