Tool for Static Verification of Memory Access Correctness Preconditions in Linux Kernel

Student: Melnichenko Pyotr

Educational Programme: Applied Mathematics and Information Science (Bachelor)

Year of Graduation: 2018

This work implements a static analysis method for verifying memory access correctness within Linux kernel modules. Analyzing the entire Linux kernel is computationally expensive due to its sheer size. Instead, a module and the core Linux kernel functions it uses are analyzed separately using existing software verification tools. Developed system for analyzing Linux kernel functions extracts simple summaries of function behaviour with regards to memory safety. During analysis of a Linux module, these summaries are used for instrumentation of the module source code, inserting simplified versions of the kernel functions it uses. An existing static analyzer verifies the instrumented code, thus detecting memory safety issues both within the module itself and in the boundaries between the module and the core of the Linux kernel.

Student Theses at HSE must be completed in accordance with the University Rules and regulations specified by each educational programme.

Summaries of all theses must be published and made freely available on the HSE website.

The full text of a thesis can be published in open access on the HSE website only if the authoring student (copyright holder) agrees, or, if the thesis was written by a team of students, if all the co-authors (copyright holders) agree. After a thesis is published on the HSE website, it obtains the status of an online publication.

Student theses are objects of copyright and their use is subject to limitations in accordance with the Russian Federation’s law on intellectual property.

In the event that a thesis is quoted or otherwise used, reference to the author’s name and the source of quotation is required.

Search all student theses