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.

h2. Development of rule model

All rule models are described in kernel-rules/model-db.xml. 

There is a <model> XML element for each rule model.

Identifier of the model is declared by ''id'' attribute.

Child elements of the <model> element include:

* rule – identifier of a rule (there can be several models for the same rule);

* status – status of readiness (''public'' means it is ready for public use, other values (e.g., ''default'' or ''private'') mean it is not recommended for some reasons);

* kind – kind of the model (''aspect'' means the model is defined with CIF aspects, ''plain'' means it is defined with C macro definitions) if unsure use ''aspect'' one;

* error – error label (for now, it must be LDV_ERROR);

* description – informal description of the model (optional, usually used if there are several models for the same rule);

* files - list of files defining the model, contains the following child elements:

** aspect – a relative path to file containing CIF "advices":http://en.wikipedia.org/wiki/Advice_%28programming%29 that are applied to all source files of a driver under analysis (this file contains an actual definition of the model);

** config – a relative path to a config file (should be models/config-tracers.h for new rules);

* hints – hints to verification engine such as extra options to be used for this particular model (if unsure leave empty).

An example of the model element:

<pre>

<model id="100_1a">

    <rule>0100</rule>

    <status>public</status>

    <kind>aspect</kind>

    <error>LDV_ERROR</error>

    <engine>blast</engine>

    <description></description>

    <files>

        <aspect>./models/model0100.aspect</aspect>

        <config>./models/config-tracers.h</config>

    </files>

    <hints></hints>

</model>

</pre>

h2. Model Comments

Model comments is used by error trace visualizer to highlight important elements of error traces. It makes analysis of error traces much easier, so it is highly recommended to write model comments from the very beginning. The comments should be short but it should clearly express corresponding situation. For example, comments to ldv_assert should explain what is a problem detected.

Model comments are usual C comments starting with '' LDV_COMMENT*''. For example:

<pre>

/* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name=''ldv_check_alloc_flags'') Check that a memory allocating function was called with a correct value of flags in spin locking. */

void ldv_check_alloc_flags(gfp_t flags)

{

  /* LDV_COMMENT_ASSERT If spinlock is locked then a memory allocating function should be called with GFP_ATOMIC flag set. */

  ldv_assert(ldv_spin == LDV_SPIN_UNLOCKED || flags & GFP_ATOMIC);

}

/* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name=''ldv_spin_lock'') Lock spinlock. */

void ldv_spin_lock(void)

{

  /* LDV_COMMENT_CHANGE_STATE Lock spinlock. */

  ldv_spin = LDV_SPIN_LOCKED;

}

</pre>

h3. Kinds of Model Comments

* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name=''function name to match with'') describes a model function. The name argument is mandatory.

It is used to match corresponding functions in error trace. In simple cases it equals to name of function in declaration.

* LDV_COMMENT_ASSERT describes what is a problem detected if the assertion failed.

* LDV_COMMENT_CHANGE_STATE decribes changes in model state.

* LDV_COMMENT_RETURN describes returned value of a model function.

* LDV_COMMENT_OTHER is used to describe any other interesting elements of a model.