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

[[Developing Aspect Rule Models]]

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>

h2. Test Development

h3. Common Notes

Do not pay too much attention to tests. Tests just should show that you are developing the rule model in the proper way. Your actual purpose is described in the next Section. 

To create tests for a new rule model you can simply copy existing tests for other 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 QA night test task (regr-tests/test-sets/medium). New tests should be passed, so test them carefully before merging.

h3. Test Driver

Each test driver consists of Makefile and a set of C and H source files. Each driver should be compatible with a kernel it is developed for. 

Состоит из набора исходных кодов .c, .h файлов и Makefile. Драйвер должен компилироваться с тем ядром, для которого он предназначен. В Makefile указывается директива obj-m, определяющая собираемые модули (файлы .ko).

    Называйте модули согласно вердикту: начинайте название с U где результат должен быть unsafe, и с S — где safe. Если срабатывание ложное — добавляйте букву F (например, "FU" или "FS").

    Создав несколько .c файлов с кодом, можно запустить скрипт drivers/gen_makefile.pl, чтобы автоматически сгенерировать Makefile драйвера с модулем .ko на каждый сишник .c.

    Повторю, основной критерий качества тестов на функцию: если функция вовсе не инструментируется, то хотя бы один из её тестов должен провалиться. В модели 08_1 на каждую функцию написано три теста: 0, 1 и 2 вызова (только 1 вызов — правильный, safe).

    Несколько папок с тестами нужны для возможности их отдельного запуска. Дело в том, что API ядра меняется, и, если в один архив попадут много тестов на разные функции, то с большой вероятностью этот драйвер будет пригоден для тестирования только с одним ядром. Поэтому для существенно разных функций имеет смысл делать разные папки с драйверами (особенно, если эти функции появились в какой-то определённой версии ядра!). 

h3. Test Task

Для первого запуска регрессионных тестов вам необходимо сформировать файл задания, где описано хотя бы минимум то, что вы хотите запускать (см. далее Первая часть). После первого запуска надо будет разобраться с полученными результатами (автоматически будет сформирована Вторая часть) и, если все правильно, то можно поменять исходный файл с заданием на сгенерированный.

Файл задания состоит из записей вида

 driver=08_1--test-nonseek.tar.bz2;origin=external;kernel=linux-2.6.37;model=08_1;module=drivers/08_1/test-nonseek/S-nonseek-alone-test.ko;main=ldv_main0_sequence_infinite_withcheck_stateful;verdict=safe

Первая часть переменных описывает параметры запуска

 driver=08_1--test-nonseek.tar.bz2;origin=external;kernel=linux-2.6.37;model=08_1

    driver имя архива драйвера, формируется по именам папок от drivers/ с заменой "/" на "--". Например 08_1--test-nonseek.tar.bz2 лежит в drivers/08_1/test-nonseek/.

    origin

        external - внешний драйвер (для модельных тестов, как правило, будет указан данный вид драйверов)

        kernel - внутренний драйвер 

    kernel - версия ядра

    model - идентификатор модели 

Вторая часть описывает ожидаемый результат (ее можно не описывать в самом начале)

 module=drivers/08_1/test-nonseek/S-nonseek-alone-test.ko;main=ldv_main0_sequence_infinite_withcheck_stateful;verdict=safe

    module - модуль драйвера

    main - имя сгенерированной точки входа

    verdict - полученный по результатам верификации вердикт 

В том случае, если вердикт unknown, в дополнительных полях показывается, какой инструмент упал и перечисляются выявленные проблемы:

verdict=unknown;RCV_status=fail;problems=Blocks_SAT,Exception

h3. Choosing the Linux Kernel

Ядро для тестирования рекомендуется выбирать на основе уже имеющихся в репозитории (дабы не раздувать размеры репозитория).

Имеющиеся версии можно посмотреть здесь:

    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-tests/rule-models

        linux-2.6.37.tar.bz2

        linux-3.5.tar.bz2 

В будущем планируется сделать систему автоматической загрузки нужных версий ядра из локального или одного из глобальных хранилищ. Тогда можно будет себя не ограничивать в выборе версий ядер.

Запуск тестов и анализ результатов

Для начала тесты нужно установить:

 prefix=/path/to/your/installation/directory make install-testing

где /path/to/your/installation/directory - путь к установленному ldv-tools. После этого архивы с установленными тестами появятся в директории /ldv-tests/rule-models/. Там же будет лежать и ваш файл задания.

h3. Regression Testing

First of all you need to create an empry working directory. Then you need to move to it and run the following command (path to LDV tools executables should be added to $PATH environment 

Для запуска следует создать рабочую папку, перейти в неё и выполнить следующую команду:

 rm -rf * && LDV_DEBUG=100 LDVDBTEST=ldvdb LDVUSERTEST=ldvreports regr-test.pl --test-set /home/shchepetkov/ldv/ldv-tests/rule-models/regr-task-118_1a 

где:

    rm -rf * - удаляет все файлы и папки из рабочей директории, возможно оставшиеся после предыдущего запуска. Рабочая папка перед запуском должна быть пустая! 

    LDVDBTEST=ldvdb LDVUSERTEST=ldvreports - переменные окружения, указывающие на пользователя и базу данных. Подставьте сюда свои значения. Учтите, в результате из этой базы удалятся результаты всех предыдущих запусков! 

    regr-test.pl - скрипт, отвечающий за запуск тестов. Его содержимое можно посмотреть тут: /bin/regr-test.pl 

    --test-set /home/shchepetkov/ldv/ldv-tests/rule-models/regr-task-118_1a - тут задаётся абсолютный путь до файла с заданием. --test-set <name> - одна из опция запуска скрипта, как раз указывающая на файл с заданием. Чтобы посмотреть остальные доступные опции, следует выполнить команду: 

 regr-test.pl --help

Итак, по окончанию запуска результаты буду залиты на сервер статистики. Так же в папке появятся файлы и директории, которые создаёт скрипт регрессионного тестирования:

 ls -1

 current.sorted

 launcher-results-dir

 launcher-working-dir

 original.sorted

 regr-task-new

 regr-test.diff

 work

Тут нам будут интересны 3 файла - original.sorted, current.sorted и regr-test.diff. Первый - ваш отсортированный тест задания. Второй - это тест задания, сгенерированный скриптом regr-test.pl автоматически на основе результатов запуска. Если ожидаемые результаты не сходятся с фактическими, то разница будет записана в третий файл - regr-test.diff. В этом случае его необходимо посмотреть, понять в чем проблема и исправить её. Если же файл пустой, то тесты успешно проёдены.

Для большего удобства анализирования результатов можно установить стороннюю программу meld. Она занимается сравниванием содержимого текстовых файлов. Команда:

 meld current.sorted original.sorted 

покажет вам различие между этими файлами. Получается гораздо нагляднее и быстрее, чем если просто смотреть regr-test.diff. 

h2. Verification of Linux Kernel Drivers

TBD.

h2. Creating Final Account

TBD.