• Table of contents
• Formalizing Safety Rules
  • Main Tasks
  • Typical Workflow
  • Elicitation of kernel core API relevant to the rule
  • Development of rule model

Formalizing Safety Rules¶

Main Tasks¶

1. Elicitation of all elements of kernel core API relevant to the rule
2. 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)
3. Extending code of the rule with model comments
4. Test development
5. Linux kernel verification and result analysis
6. Markup of results of reference runs
7. Rule description
8. Report
9. Publication
10. Reporting bugs detected in Linux kernel

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

Typical Workflow¶

1. Reserve a rule identifier by creating a feature request here:
   http://forge.ispras.ru/projects/ldv-rules/issues.
2. Collect a list of functions from kernel API relevant to the rule (at first iterations the list can be incomplete).
3. Write a small pseudo driver that uses a couple of key function from the list above.
4. 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.
5. 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):
   

     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
   

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

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.

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

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