Linux Driver Verification

{{toc}}

h1. Formalizing Safety Rules

h2. Main Tasks

# Elicitation of all elements of kernel core API relevant to the rule

# Development of rule model that consists of

#* model state (one or more C variables);

#* transitions between states linked to appropriate events in device driver (usually calls of kernel core API)

#* a set of error states (that represents misuse of kernel core API)

# Extending code of the rule with model comments

# Test development

# Linux kernel verification and result analysis

# Markup of results of reference runs

# Rule description

# Report

# Publication

# Reporting bugs detected in Linux kernel

Usually process of work on the tasks is iterative and the sequence of the tasks can be different.

h2. Typical Workflow

# Reserve a rule identifier by creating a feature request here:

http://forge.ispras.ru/projects/ldv-rules/issues.

# Collect a list of functions from kernel API relevant to the rule (at first iterations the list can be incomplete).

# Write a small pseudo driver that uses a couple of key function from the list above.

# Create a template of your model in a separate folder (by copying kernel-rules). ldv-manager is able to use this copy of RuleDB using environment variable LDV_KERNEL_RULES=/path/to/folder. Use of the copy will help you to avoid problems with commiting to git submodule later. Create model comments (actual description can be just a fake at the beginning, but they still will help to visualize error trace.

# Write a positive (SAFE) and negative (UNSAFE) test for each assertion your have in the rule. It is recommended to develop tests and the model in parallel and check them using ldv-manager and its embedded vizualization (LDV_VIEW=y):

<pre>

  prefix=/xxx make -C ldv-tests/rule-models install

  cp /xxx/ldv-tools/ldv-tests/rule-models/__install/ldv-tests/rule-models/MODEL_testname.tar.bz2  /ldv-manager/

  cd ldv-manager

  LDV_VIEW=y LDV_KERNEL_RULES=/home/user/work/ldv/ldv-tools/144 \

      ldv-manager envs=linux-3.10.tar.bz2 drivers=test_name.tar.bz2 rule_models=144_1a 2>&1

</pre>

# Run verification on all drivers from the kernel. Analyze the results. If there are issues with your rule model, fix them and rerun the verification.

It is recommended after each modification of the rule to rerun all tests for the rule, then run verification of small (but interesting for the modifications) subfolder from Linux drivers, and only after that to run verification of all the drivers.

h2. Elicitation of kernel core API relevant to the rule

Usually several relevant interfaces (i.e. function and macroses) are obvious from a description of the rule and from examples of the corresponding bug fixes.

Reading documentation to already identified interfaces and of the corresponding subsystem helps to extend the list. To find documentation look to header files

where the interfaces are declared and to grep Documentation folder of linux kernel. http://lxr.free-electrons.com/ is a useful resource for navigation across kernel code.

The rest of the interfaces are detected during of analysis of results of verification runs.