Home

CBMC as a csmock plugin

IMPORTANT

Replace /bin/csexec-cbmc with this and /bin/cbmc-convert-output with this.

# get csmock - tool for scanning SRPMs by Static Analysis tools in a fully automated way
$ git clone https://github.com/aufover/csmock; cd csmock
# experimental branches: [symbiotic+divine, WIP-cbmc-plugin]
$ git checkout WIP-cbmc-plugin
# RPM-based Installation (be careful with versions)
$ ./make-srpm.sh # *src.rpm was made
# build RPMs from csmock*.src.rpm e.g. csmock-2.8.0.20210811.151353.gca4c85d.cbmc_plugin_WIP-1.fc33.src.rpm
$ rpmbuild --rebuild /home/vmihalko/praca/csmock_cbmc_plugin/csmock/csmock-
# install RPMs what we need to install from ~/rpmbuild/RPMS/noarch/{all plugins and csmock-common} 
# csmock-common installation
$ sudo dnf localinstall ~/rpmbuild/RPMS/noarch/csmock-common-2.8.0.20210811.151353.gca4c85d.cbmc_plugin_WIP-1.fc33.noarch.rpm 
# plugin installation
$ sudo dnf localinstall ~/rpmbuild/RPMS/noarch/csmock-plugin-cbmc-2.8.0.20210811.151353.gca4c85d.cbmc_plugin_WIP-1.fc33.noarch.rpm
# download src.rpm package, which you want to verify
$ koji download-build -a src logrotate-3.17.0-3.fc33
# run package verification (underhood: https://github.com/kdudka/cswrap/wiki/csexec, https://www.youtube.com/watch?v=FjV84hbD1GY&t=659s&ab_channel=KamilDudka)
$ csmock -t cbmc -r fedora-33-x86_64  ./logrotate-3.17.0-3.fc33.src.rpm --cbmc-timeout 10
# get the results
$ tar -xvf ./logrotate-3.17.0-3.fc33.tar.xz '*/cbmc-capture/'
# check the results
$ cd logrotate-3.17.0-3.fc33/debug/raw-results/builddir/cbmc-capture/