Predicate Abstaction using SAT
DDVerify is tool for checking Linux device drivers for specific bugs. It automatically detects the operations provided by the module, and generates a test harness to reveal specific misuses of the kernel API. The harnesses generated by DDverify are plain C models that can be passed to verification tools such as SATABS or CBMC.
Unpack the file ddverify.tgz.
DDverify needs to setup the environment variable DDV_PATH
to the location of the unpacked directory. Finally, add the directory $DDV_PATH/bin to the PATH.
The directory case_studies contains a collection of device drivers coming from the
linux kernel. The following example illustrates the usage of
subdirectory char/watchdog/machzwd contains a driver that reads an uninitialized
port, violating thus the requirements of the kernel API.
Go to the directory machzwd, and run the following command:
ddverify machzwd.c --check-io --model seq1
The file machzwd.c contains the code of the driver.
DDVerify extracts the initialization
function and the exit function of the module, and generates a test harness using the model for operating-system seq1,
which can be found in the directory $DDV_PATH/models/seq1. The name 'seq1' stands for sequential. A single thread
is used to nondeterministically call the different operations of the driver. The option check-io informs ddverify
to generate assertions for verifying the correct usage of IO ports.
By default, the model checker is set to smv. The option --modelchecker boppo switches the model-checking engine to boppo.
DDverify shall report that the claims 1 and 2 fail. To get more information about the bug, type the command ./ddv_satabs --claim zf_readw.2. This script is automatically generated by ddverify to verify a specific claim using SATABS.