Predicate Abstaction using SAT

About DDverify

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.

Download

The file contains DDverify plus a collection of drivers from the linux kernel. SATABS can be downloaded from here. CBMC is available from here.

Requirements

SATABS needs a model checker to run. We recommend to install either Cadence SMV or BOPPO.

Installation

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.

Example

The directory case_studies contains a collection of device drivers coming from the linux kernel. The following example illustrates the usage of DDVerify. The 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.