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
_______________________________________________
devel mailing list -- devel@xxxxxxxxxxxxxxxxxxxxxxx
To unsubscribe send an email to devel-leave@xxxxxxxxxxxxxxxxxxxxxxx
Fedora Code of Conduct: https://docs.fedoraproject.org/en-US/project/code-of-conduct/
List Guidelines: https://fedoraproject.org/wiki/Mailing_list_guidelines
List Archives: https://lists.fedoraproject.org/archives/list/devel@xxxxxxxxxxxxxxxxxxxxxxx
Do not reply to spam on the list, report it: https://pagure.io/fedora-infrastructure
