Project

General

Profile

Wiki » History » Version 3

Alexey Khoroshilov, 06/26/2018 03:51 AM

1 1 Alexey Khoroshilov
To see description in Russian, please look at source:README_ru.md.
2
3
The repository contains ACSL specifications for the Linux kernel functions. The aim of the project is formal verification of Linux kernel library functions.
4
5
h2. Papers
6
7
- D. Efremov, M. Mandrykin, "Formal Verification of Linux Kernel Library Functions":http://www.ispras.ru/proceedings/isp_29_2017_6/isp_29_2017_6_49/  (in Russian) "[PDF]":http://www.ispras.ru/proceedings/docs/2017/29/6/isp_29_2017_6_49.pdf
8
- D. Efremov, M. Mandrykin, A. Khoroshilov, Deductive Verification of Unmodified Linux Kernel Library Functions (will be published soon)
9
10
h2. Proofs Status
11
12
| ID | Function      | Status | Logic function | libfuzzer | Comment |
13
| 1  | check_bytes8 | proved | proved         | yes       |         |
14
| 2  | match_string |        | not required   |           |         |
15
| 3  | memchr        | proved |                | yes       |         |
16
| 4  | memcmp        | proved |                | yes       |         |
17
| 5  | memscan       | proved | not required   | yes       |         |
18
| 6  | skip_spaces  | proved | proved         | yes       | requires too strict (remove strlen) |
19
| 7  | strcasecmp    | proved |                | yes       |         |
20
| 8  | strcat        | proved | not required   |           | usr strcmp in ensures |
21
| 9  | strchr        | proved | proved         | yes       |         |
22
| 10 | strchrnul     | proved | proved         | yes       |         |
23
| 11 | strcmp        | proved |                | yes       |         |
24
| 12 | strcpy        | proved | not required   |           | use strcmp logic function |
25
| 13 | strcspn       | proved | proved         | yes       |         |
26
| 14 | strim         |        | not required   | !const    |         |
27
| 15 | strlen        | proved | proved         | yes       |         |
28
| 16 | strncasecmp   |        |                | yes       |         |
29
| 17 | strncat       |        | not required   |           |         |
30
| 18 | strnchr       | proved |                | yes       |         |
31
| 19 | strncmp       |        |                | yes       |         |
32
| 20 | strncpy       |        | not required   |           |         |
33
| 21 | strnlen       | proved | proved         | yes       |         |
34
| 22 | strnstr       |        |                | yes       |         |
35
| 23 | strpbrk       | proved | proved         | yes       |         |
36
| 24 | strrchr       | proved |                | yes       |         |
37
| 25 | strreplace    |        | not required   | !const    |         |
38
| 26 | strsep        | proved | not required   | !const    |         |
39
| 27 | strspn        | proved | proved         | yes       |         |
40
| 28 | strstr        |        |                | yes       |         |
41
| 29 | sysfs_streq  |        |                | yes       |         |
42
| 30 | strlcat       |        | not required   |           |         |
43
| 31 | strlcpy       | proved | not required   |           | use strncmp lf in ensures |
44
| 32 | memmove       | proved(*)| not required   |           | use memcmp logic function at ensures |
45
| 33 | memcpy        | proved | not required   |           | use memcmp logic function at ensures |
46
| 34 | memset        | proved | not required   | !const    |         |
47
| 35 | kstrtobool    | proved | not required   | yes       |         |
48
| 36 | _parse_integer_fixup_radix | proved | not required | yes | |
49
| 37 | _parse_integer |     |                | yes       |         |
50
51
 (*) memmove - except pointer difference vc fail. Model limitation.
52
53
h2. Toolchain
54
55
The specifications are developed in the "[ACSL]":http://frama-c.com/download/acsl-implementation-Sulfur-20171101.pdf language. Frama-C with "[AstraVer]":https://forge.ispras.ru/projects/astraver plugin is used as the deductive verification instrument.
56
57
- A description of how to install the tools can be found [here](https://forge.ispras.ru/projects/astraver/wiki). You can run them on Linux, Windows, Mac OS X.
58
59
h2. Repository files
60
61
Each library function of the Linux kernel is located in a separate \*.c file. The corresponding \*.h file contains declarations, types, and structures specific to the function.
62
63
- The **kernel_definitons.h** file contains common for all functions types, macros, and other declarations.
64
- In **ctype.h** there are several functions, which were initially developed as macro. For the convenience of formal verification, these macro (islower, isupper, isdigit, ...) have been rewritten as an inline functions.
65
66
h3. How to add a function in the repository
67
68
There is a tool called dismember in the "[repository]":https://forge.ispras.ru/projects/astraver-utils/. It is used to "transfer" the function code into a separate file.
69
Example (code for the strim function):
70
<pre>
71
bash
72
$ dismember -m ~/linux-stable/lib/string.c -k ~/linux-stable --double -f strim --output-dir .
73
</pre>
74
75
Two files will be created: strim.c and strim.h
76
77
- **<notextile>-m</notextile>** - path to the file with function definition
78
- **<notextile>-k</notextile>** - path to the kernel directory
79
- **<notextile>-double</notextile>** - generate two files *.h and *.c
80
- **<notextile>-f</notextile>** - function name
81
- **<notextile>-output-dir</notextile>** - output directory
82
83
h2. Specifications
84
85
The specification contract (precondition and postcondition) is located in the corresponding *.h file for each proved function (for example, strlen.h). A header file may also contain lemmas/axioms/logical functions if they are developed for a function.
86
87
A *.c file contain a body of a function with loops invariants, evaluation functions, and assertions.
88
89
For some functions, specifications are redundant. In fact, they describe function's behavior in two different ways. For example, the contract for the strlen function consists of a "regular" functional requirements and the requirement for correspondence of the returned result to the logical function strlen.
90
91
What is the reason for a such "redundancy"?
92
93
The logical function strlen is convenient to use in the other function's specification. For example, strcmp function (and strcmp logical function in the strcpy contract). All the basic properties of a logical functions are expressed in lemmas (lemmas are not proved at this stage). Such specifications can't be translated in the run-time assertions with E-ACSL plugin. Therefore, for those functions with a correspondent logical function, there are additionally exists a "usual" specification.
94
95
Criteria to develop a logical function:
96
97
1. It is possible to write a logical function only for a pure C function;
98
2. It is rational to write logical functions if they are useful for developing specifications of other functions. For example, in the memcpy contract, you can express the equality of src and dest by calling the memcmp logical function.
99
100 2 Alexey Khoroshilov
Full verification protocols (solver launches) are included (*.jessie folders) in the repository for the [[wiki#Proofs-Status|proved functions]].
101 3 Alexey Khoroshilov
102
At the given stage, the correctness of the lemmas in the specifications is not proved in any way. Thus, they can contain contradictions. The lemmas will be proved at the second project stage by means of Coq or lemma functions.
103
104
h2. How to run the tools
105
106
<pre>
107
$ frama-c -jessie <func>.c
108
$ frama-c -jessie check_bytes8.c
109
</pre>
110
111
Or
112
<pre>
113
$ make verify-<func>
114
$ make verify-check_bytes8
115
</pre>
116
117
h2. LibFuzzer integration
118
119
"[LibFuzzer]":http://llvm.org/docs/LibFuzzer.html - is the library for function fuzzing. The status of functions fuzzing integration can be viewed in [[wiki#Proofs-Status|proved functions]] table. It is required to have clang compiler installed and libFuzzer.a in the project directory to run fuzzing.
120
How to run fuzzing:
121
<pre>
122
$ make fuzz-<func>
123
$ make fuzz-check_bytes8
124
</pre>