Linux Driver Verification

{{toc}}

h1. Formalizing Safety Rules 2

Before starting formalizing safety rules you need to create an account at this site. The name of this account should be sent to managers of the LDV project, e.g. via e-mail. Then somebody will add you to developers of the LDV project and you will be able to create and to update feature requests and bug reports "here":http://forge.ispras.ru/projects/ldv-rules/issues. 

Formalizing safety rules consists of following activities that can be fully or partially repeated several times.

h2. Understanding and Informal Description of the Rule

Just one time per each rule you need to reserve a rule identifier by creating a feature request "here":http://forge.ispras.ru/projects/ldv-rules/issues. The rule identifier is a number. This number should be greater by one then the maximum of already reserved numbers. Note that you won''t be able to change the rule identifier. 

To understand the rule you need to:

* Read available documentation of the relevant kernel core API, e.g. "here":https://git.kernel.org/cgit/linux/kernel/git/torvalds/linux.git/tree/Documentation or in books like "LDD3":http://lwn.net/Kernel/LDD3.

* Explore source code, especially relevant header files, of the Linux kernel. For navigation through Linux kernel source code you may use http://lxr.linux.no or http://lxr.free-electrons.com.

* Analyze existing violations of the given rule. You may use the Internet or https://git.kernel.org/cgit/linux/kernel/git/torvalds/linux.git for this purpose.

* Analyze verification results that you will obtained at one of the following steps.

* Discuss it with developers of the LDV project, if nothing else helps.

Each time after understanding more details about the rule, you should update informal description of the rule, that includes:

* Short name, that should be a part of the name of the feature request you have created before.

* Summary, that should outline the essense of the rule.

* Detailed description, that should clearly describe all incorrect usages of the relevant kernel core API.

* Links to existing violations of the rule. Also it would be greate to provide some short description of each violation, since they may be rather hard for understanding.

* Some auxiliary information like absence of required functionality in LDV tools to formalize or/and to check some part of the rule.

You can find an example of a good description of a rule "here":http://linuxtesting.org/ldv/online?action=show_rule&rule_id=0032. But nobody prevent you from creating a much better description.

h2. Development of the Rule Model

h3. Rule Model Description

All rule models are described in $LDV_TOOLS_SRC/kernel-rules/model-db.xml. So that the most easy way to add one more rule model is to copy description of the existing one (e.g. "100_1a") and to update some information in this description. 

There is a <model> XML element for each rule model. The identifier of the model is declared by ''id'' attribute. Most likely the identifier of the new rule model will be in form: identifier of the rule concatenated with ''_1a''.

Child elements of the <model> element include:

* rule – identifier of the 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. You should use ''private'' during development

* kind – kind of the model. ''aspect'' means the model is defined with CIF aspects, ''plain'' means it is defined as a library. You should use ''aspect'' kind.

* error – error label. For now, it must be LDV_ERROR.

* engine - a verifier to be used for analysis. You should use ''blast''.

* description – informal description of the model. Optional, usually used if there are several models for the same rule. So you may not fill it.

* files - list of relative to $LDV_TOOLS_SRC/kernel-rules files defining the model. It contains the following child elements (for ''aspect'' models):

** aspect – a 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, see below).

** config – a config file. It should be models/config-tracers.h for new rule models.

* hints – hints to a verifier such as extra options to be used for this particular model. Most likely you need to leave this element 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>

h3. Developing Aspect Rule Models

TODO.

h3. Model Comments

Model comments are used by error trace visualizer to highlight important elements of error traces produced by a verifier. 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.

You can use one of the following kinds of model comments:

* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name=''function name to match with'') - describes a model function. The name argument is mandatory. Its value should be equal to a model function name defined at the following line.

* 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 a returned value of a model function.

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

Model comments are written as usual C comments, 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>