Project

General

Profile

Formalizing Safety Rules » History » Version 2

Alexey Khoroshilov, 07/18/2013 02:57 AM

1 2 Alexey Khoroshilov
{{toc}}
2
3 1 Alexey Khoroshilov
h1. Formalizing Safety Rules
4
5
h2. Main Tasks
6
7
# Elicitation of all elements of kernel core API relevant to the rule
8
# Development of rule model that consists of
9
#* model state (one or more C variables);
10
#* transitions between states linked to appropriate events in device driver (usually calls of kernel core API)
11
#* a set of error states (that represents misuse of kernel core API)
12
# Extending code of the rule with model comments
13
# Test development
14
# Linux kernel verification and result analysis
15
# Markup of results of reference runs
16
# Rule description
17
# Report
18
# Publication
19
# Reporting bugs detected in Linux kernel
20
21
Usually process of work on the tasks is iterative and the sequence of the tasks can be different.
22
23
h2. Typical Workflow
24
25
# Reserve a rule identifier by creating a feature request here:
26
http://forge.ispras.ru/projects/ldv-rules/issues.
27
# Collect a list of functions from kernel API relevant to the rule (at first iterations the list can be incomplete).
28
# Write a small pseudo driver that uses a couple of key function from the list above.
29
# 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.
30
# 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):
31
<pre>
32
  prefix=/xxx make -C ldv-tests/rule-models install
33
  cp /xxx/ldv-tools/ldv-tests/rule-models/__install/ldv-tests/rule-models/MODEL_testname.tar.bz2  /ldv-manager/
34
  cd ldv-manager
35
  LDV_VIEW=y LDV_KERNEL_RULES=/home/user/work/ldv/ldv-tools/144 \
36
      ldv-manager envs=linux-3.10.tar.bz2 drivers=test_name.tar.bz2 rule_models=144_1a 2>&1
37
</pre>
38
# 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.
39
40
41
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.
42 2 Alexey Khoroshilov
43
h2. Elicitation of kernel core API relevant to the rule
44
45
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.
46
47
Reading documentation to already identified interfaces and of the corresponding subsystem helps to extend the list. To find documentation look to header files
48
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.
49
50
The rest of the interfaces are detected during of analysis of results of verification runs.