SATABS Manual

SATABS – Predicate Abstraction with SAT

Tutorials

Example: Reference Counting in Linux Device Drivers

Microsoft's SLAM toolkit has been successfully used to find bugs in Windows device drivers. SLAM automatically verifies device driver whether a device driver adheres to a set of specifications. SLAM provides a test harness for device drivers that calls the device driver dispatch routines in a non-deterministic order. Therefore, the Model Checker examines all combinations of calls. Motivated by the success this approach, we provide a toy example based on Linux device drivers. For a more complete approach to the verification of Linux device drivers, consider DDVerify.

Dynamically loadable modules enable the Linux Kernel to load device drivers on demand and to release them when they are not needed anymore. When a device driver is registered, the kernel provides a major number that is used to uniquely identify the device driver. The corresponding device can be accessed through special files in the filesystem; by convention, they are located in the /dev directory. If a process accesses a device file the kernel calls the corresponding open, read and write functions of the device driver. Since a driver must not be released by the kernel as long as it is used by at least one process, the device driver must maintain a usage counter (in more recent Linux kernels, this is done automatically, however, drivers that must maintain backward compatibility have to adjust this counter).

We provide a skeleton of such a driver. Download the files spec.c, driver.c, driver.h, kdev_t.h, and modules.h.

The driver contains following functions:

1. register_chrdev: (in spec.c) Registers a character device. In our implementation, the function sets the variable usecount to zero and returns a major number for this device (a constant, if the user provides 0 as argument for the major number, and the value specified by the user otherwise).

   int usecount;
   
   int register_chrdev (unsigned int major, const char* name)
   {
     usecount = 0;
     if (major == 0)
       return MAJOR_NUMBER;
     return major;
   }

2. unregister_chrdev: (in spec.c) Unregisters a character device. This function asserts that the device is not used by any process anymore (we use the macro MOD_IN_USE to check this).

   int unregister_chrdev (unsigned int major, const char* name)
   {
     if (MOD_IN_USE)
       {
       ERROR: assert (0);
       }
     else
       return 0;
   }

3. dummy_open: (in driver.c) This function increases the usecount. If the device is locked by some other process dummy_open returns -1. Otherwise it locks the device for the caller.

4. dummy_read: (in driver.c) This function "simulates" a read access to the device. In fact it does nothing, since we are currently not interested in the potential buffer overflow that may result from a call to this function. Note the usage of the function nondet_int: This is an internal SATABS-function that non­determi­nistically returns an arbitrary integer value. The function __CPROVER_assume tells SATABS to ignore all traces that do not adhere to the given assumption. Therefore, whenever the lock is held, dummy_read will return a value between 0 and max. If the lock is not held, then dummy_read returns -1.

5. dummy_release: (in driver.c) If the lock is held, then dummy_release decreases the usecount, releases the lock, and returns 0. Otherwise, the function returns -1.

We now want to check if any valid sequence of calls of the dispatch functions (in driver.c) can lead to the violation of the assertion (in spec.c). Obviously, a call to dummy_open that is immediately followed by a call to unregister_chrdev violates the assertion.

The function main in spec.c gives an example of how these functions are called. First, a character device "dummy" is registered. The major number is stored in the inode structure of the device. The values for the file structure are assigned non-deterministically. We rule out invalid sequences of calls by ensuring that no device is unregistered while it is still locked. We use the following model checking harness for calling the dispatching functions:

      random = nondet_uchar ();
      __CPROVER_assume (0 <= random && random <= 3);

      switch (random)
      {
      case 1: 
        rval = dummy_open (&inode, &my_file);
        if (rval == 0)
          lock_held = TRUE;
        break;
      case 2:
        __CPROVER_assume (lock_held);
        count = dummy_read (&my_file, buffer, BUF_SIZE); 
        break;
      case 3:
        dummy_release (&inode, &my_file);
        lock_held = FALSE;
        break;
      default:
        break;
      }

The variable random is assigned non-deterministically. Subsequently, the value of random is restricted to be 0 &le random ≤ 3 by a call to __CPROVER_assume. Whenever the value of random is not in this interval, the corresponding execution trace is simply discarded by SATABS. Depending on the value of random, the harness calls either dummy_open, dummy_read or dummy_close. Therefore, if there is a sequence of calls to these three functions that leads to a violation of the assertion in unregister_chrdev, then SATABS will eventually consider it.

If we ask SATABS to show us the properties it verifies with

satabs driver.c spec.c --show-properties

for our example, we obtain

1. Claim unregister_chrdev.1:
       file spec.c line 18 function unregister_chrdev
       MOD_IN_USE in unregister_chrdev
       FALSE

2. Claim dummy_open.1:
       file driver.c line 15 function dummy_open
       i_rdev mismatch
       (unsigned int)inode->i_rdev >> 8 == (unsigned int)dummy_major

It seems obvious that the property dummy_open.1 can never be violated. SATABS confirms this assumption: We call

satabs driver.c spec.c --property dummy_open.1

and SATABS reports VERIFICATION SUCCESSFUL after a few iterations.

If we try to verify property unregister_chrdev.1, SATABS reports that the property in line 18 in file spec.c is violated (i.e., the assertion does not hold, therefore the VERIFICATION FAILED). Furthermore, SATABS provides a detailed description of the problem in the form of a counterexample (i.e., an execution trace that violates the property). On this trace, dummy_open is called twice, leading to a usecount of 2. The second call of course fails with rval=-1, but the counter is increased nevertheless:

int dummy_open (struct inode *inode, struct file *filp)
{
  __CPROVER_assert(MAJOR (inode->i_rdev) == dummy_major,
      "i_rdev mismatch");
  MOD_INC_USE_COUNT;

  if (locked)
    return -1;
  locked = TRUE;

  return 0; /* success */
}

Then, dummy_release is called to release the lock on the device. Finally, the loop is left and the call to unregister_chrdev results in a violation of the assertion (since usecount is still 1, even though locked=0).