• Table of contents
• Formalizing Safety Rules 2
  • Understanding and Informal Description of the Rule
  • Development of the Rule Model
    • Rule Model Description
    • Developing Aspect Rule Models
    • Model Comments
  • Developing Model Tests
    • Test Drivers
    • Choosing the Linux Kernel
    • Test Task
    • Regression Testing
  • Verification of Linux Kernel Drivers
  • Creating Final Account

Formalizing Safety Rules 2¶

Before starting formalizing safety rules you need to create an account at http://forge.ispras.ru if you don't have it. 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.

Formalizing safety rules consists of following activities that can be fully or partially repeated several times. Also you may mix some activities, e.g. develop model tests before rule models themselves.

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. 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 any more.

To understand the rule you need to:

• Read available documentation of the relevant kernel core API, e.g. here or in books like LDD3.
• Explore source code, especially appropriate header files, of the Linux kernel. For navigation through Linux kernel source code you may use http://lxr.linux.no (very many versions of the Linux kernel, but it is slow and sometimes buggy, also it may truncate useful search results) or http://lxr.free-electrons.com (just main versions of the Linux kernel, fast and complete search results).
• 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 (temporarily you should place it to description of the corresponding feature request), that includes:

• Short name, that should be a part of the name of the feature request you have created for this rule. It can be modified any times rather then the rule identifier.
• Summary, that should outline the essence of the rule.
• Detailed description, that should clearly and fully describe a relevant kernel core API and all incorrect usages of it.
• Links to existing violations of the rule. Also it would be great 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, that is required to formalize or/and to check some part of the rule.

You can find an example of a good description of a rule here. But nobody prevent you from creating a much better description.

Development of the Rule Model¶

After each iteration of understanding the rule you will need to either create or update the rule model.

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 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: the rule identifier concatenated with '_1a'. Generally speaking, there can be several models for the same rule.

Child elements of the <model> element include:

• rule – identifier of the 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 using a CIF aspect, '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 files defining the model. Paths to these files should be relative to $LDV_TOOLS_SRC/kernel-rules. For aspect rule models this list contains the following child elements:
  • aspect – a file containing a CIF aspect (see below, how to write aspect files).
  • 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.

Here is an example of the existing model element:

<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>

Developing Aspect Rule Models¶

TBD
Developing Aspect Rule Models

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:

/* 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;
}

Developing Model Tests¶

Model tests are intended to insure that you are developing the rule model in the proper way. So, you should not pay too much attention to tests. Your actual purpose is to verify real drivers of the Linux kernel that will be described a bit later.

To create tests for a new rule model you can simply copy existing tests for other rule model. Rather good example is tests for 43_1a rule model.

Tests for rule models should be placed to $LDV_TOOLS_SRC/ldv-tests/rule-models/:

• Test drivers are placed to subdirectories of $LDV_TOOLS_SRC/ldv-tests/rule-models/drivers. These subdirectories are to be named in accordance with the rule model identifiers, e.g. $LDV_TOOLS_SRC/ldv-tests/rule-models/drivers/08_1a. Inside these subdirectories test should be placed to subdirectories which names start with 'test-'.
• Test tasks are placed to files starting with 'regr-task' in $LDV_TOOLS_SRC/ldv-tests/rule-models/. Be careful, after merging your branch to the master branch of LDV tools all test tasks starting with 'regr-task' will be automatically added to a QA night test task. New tests should be passed, so test them carefully before merging.
• Optionally auxiliary scripts for preparing test drivers and test tasks for regression testing.

Test Drivers¶

Test drivers should cover basic variants of usage of the relevant kernel core API. Likely for each function and macro there will be at least two tests: one should be intentionally incorrect (and thus Unsafe will be reported for it, see below) and one should be correct. Other tests may cover different sequences of invocation of macros and functions as well as reproduce some trick situations.

It is recommended to put test drivers in different directories that has names of interfaces they are intended for (don't forget about 'test-' prefix for each such directory). In each directory there should be Makefile and a set of C and, optionally, H source files.

C files should introduce loadable kernel modules. As an example you can copy existing C files, e.g. from $LDV_TOOLS_SRC/rule-models/drivers/43_1a/test-alloc_skb.

Makefile should should contain instructions how to build one or several loadable kernel modules. You can see an example of Makefile in $LDV_TOOLS_SRC/rule-models/drivers/43_1a/test-alloc_skb. Modules should be named starting with 'U' if there are violations of the rule in them ('FS' if LDV tools will report that they are Safe) or with 'S' if they are correct against this rule ('FU' if LDV tools will report that they are Unsafe). Makefiles can be generated automatically with help of $LDV_TOOLS_SRC/ldv-tests/rule-models/drivers/gen_makefile.pl but any case you should inspect generated Makefiles manually.

Of course you can create one big test driver by putting all C files into one directory and creating one Makefile for them. But you should keep in mind, that the Linux kernel API is not stable. So, you will unlikely be able to use your test driver with different versions of the Linux kernel. Especially this has sense if you already know that some interface appeared or withdrew in some particular version of the kernel.

Choosing the Linux Kernel¶

Test drivers should be compatible with a particular version of the kernel it is developed for. This doesn't mean that you may load corresponding kernel modules and observe that they work. It just means that test drivers can be built with this kernel. So that they should include proper header files and use API provided by that kernel.

It is recommended to choose one of versions of the Linux kernel already available for test development:

• $LDV_TOOLS_SRC/ldv-tests/regr-tests/test-sets/big/
  • linux-2.6.31.6.tar.bz2
  • linux-2.6.32.15.tar.bz2
  • linux-2.6.34.tar.bz2
• $LDV_TOOLS_SRC/ldv-tests/rule-models
  • linux-2.6.37.tar.bz2
  • linux-3.5.tar.bz2 (this is the most fresh in the LDV tools repository and thus the most preferable for test development).

In future we are going to support git repositories for testing. But this will be just in future...

Test Task¶

After developing test drivers for some kernel(s), you can pack them and start verification manually LDV tools. You can see $LDV_TOOLS_SRC/TUTORIAL, Section II, a. Section III of that tutorial describes how to view verification results. But it is tedious work (assume that you need to do this each day with hundreds of test drivers). So, regression test system was developed. Front-end of that system is regr-test.pl.

In regression testing there is usually an input that describes previous results (remember 'U' and 'S' prefixes of modules). Every time when regression testing is performed, the same or a bit another set of tasks are tested (verified) and then results are compared with that input. If there are some differences, this means that there some regressions.

Input for regr-test.pl is a test task. An example is $LDV_TOOLS_SRC/ldv-tests/rule-models/regr-task-43_1a. If you will open this file, you will see many long lines like "driver=43_1a--test-alloc_skb_fclone.tar.bz2;origin=external;kernel=linux-2.6.37;model=43_1a;module=drivers/43_1a/test-alloc_skb_fclone/S-spin_lock-alloc_skb_fclone_atomic-spin_unlock-test.ko;main=ldv_main0_sequence_infinite_withcheck_stateful;verdict=safe". Don't worry the most of these will be generated automatically after the first launch of regr-test.pl.

For the first invocation of regr-test.pl you just need to set up beginnings of some of these lines like "driver=43_1a--test-alloc_skb_fclone.tar.bz2;origin=external;kernel=linux-2.6.37;model=43_1a". So you need to specify (without duplicates and without any sorting):

• driver - a name of a driver archive. This name is obtained from paths to test drivers, e.g. for drivers/43_1a/test-alloc_skb a driver is 43_1a--test-alloc_skb.tar.bz2. You need to specify each of your drivers.
• origin -
  • 'external' - external driver for the kernel (for test drivers you should specify this option).
  • 'kernel' - internal driver of the kernel.
• kernel - a kernel version (most likely is linux-3.5).
• model - the model identifier

You can try to generate an initial version of the test task with help of the auxiliary script like $LDV_TOOLS_SRC/ldv-tools/ldv-tests/rule-models/drivers/43_1a/gen_task.sh. That script is intended for 43_1a model tests. So you need to set another model identifier and version of the Linux kernel.

The generated test task can be used for regression testing. The rest or the test task is as follows (you will need this when you will interpret results of the testing):

• module - a loadable kernel module. There may be several modules for each driver depending on your Makefiles.
• main - an entry point generated by driver environment generator. There may be several mains for each module.
• verdict - a verification verdict: 'safe' (the module satisfies the rule), 'unsafe' (the module doesn't satisfy the rule) or 'unknown' (something went wrong).
• In case when the verdict is 'unknown', a failed component and its problems are shown in the form similar to "RCV_status=fail;problems=Blocks_SAT,Exception".

Regression Testing¶

You need to install regression tests in accordance with $LDV_TOOLS_SRC/INSTALL, Section INSTALLING LDV, item 4. After that test drivers and the test task can be found in $PREFIX/ldv-tests/rule-models/.

Also once you need to set a special database in accordance with $LDV_TOOLS_SRC/TUTORIAL, Section I. Note that this database will be clean up automatically each time when you will run regr-test.pl. That Section also says that path to LDV tools executables should be added to $PATH environment variable.

To run regression testing, you need to create an empty working directory or clear the existing one. Then you need to chdir to it and run the following command

 rm -rf * && LDV_DEBUG=100 LDVDBTEST=ldvdb LDVUSERTEST=ldvreports regr-test.pl --test-set /absolute/path/to/your/test/task

where:

• rm -rf * - deletes all files and directories from the current working directory (something may remain from previous launches).
• LDVDBTEST=ldvdb LDVUSERTEST=ldvreports - environment variables specifying a connection to the database you have created before. So 'ldvdb' and 'ldvreports' should be replaced with your settings. A password if so can be specified via LDVDBPASSWDTEST. Note that all data from the database will be removed.
• regr-test.pl - front-end for regression test system.
• --test-set /absolute/path/to/your/test/task - an absolute path to your test task that was placed to $PREFIX/ldv-tests/rule-models/. It is one of available options of regr-test.pl. Other options can be seen by running "regr-test.pl --help".

If something is wrong in your test task, then the regression test system will point you errors. Otherwise it will finish successfully in any case.

After regression testing will finish, there will be following files and directories inside the current working directory:

• current.sorted - a sorted version of regr-task-new.
• launcher-results-dir/ - a directory with verification results (you needn't see them).
• launcher-working-dir/ - a working directory of the LDV tools (most likely you needn't see inside).
• original.sorted - a sorted version of your test task specified via --test-set.
• regr-task-new - a new version of test task generated by the regression test system automatically on the basis of verification results.
• regr-test.diff - a difference between original.sorted and current.sorted. You may use any other diff/merge tool to compare these files. For instance, meld is a good visual tool ("meld current.sorted original.sorted").

The most interesting for you is regr-test.diff. If this file is empty, it means that there is no regressions (also this can mean that your test task is empty). But during model test development it will be likely nonempty. You need to carefully analyze this difference. The reasons of them may be:

• It is a first invocation of the regression test system, and your test task was incomplete. Most likely you can simply replace your test task with current.sorted (remember that this was already noted). But you need to analyze obtained results, especially verdicts. If you suspect 'unsafe' but obtain 'safe' or/and vise versa, it is very suspicious and should be analyzed in more details.
• You have changed the rule model in such the way that model tests don't correspond to it any more. This may be either properly (and you need to fix tests) or improperly (and you need to fix the rule model).
• Something changed in LDV tools (this can happen if you update LDV tools, for example).

Verification of Linux Kernel Drivers¶

TBD

Creating Final Account¶

TBD