Differences

This shows you the differences between two versions of the page.

--- gsoc:2018-gsoc-lsb-projects [2018/01/28 16:57]
khoroshilov
+++ gsoc:2018-gsoc-lsb-projects [2018/01/29 21:13]
khoroshilov [Add support for C++11 to LSB]
@@ Line 13: / Line 13: @@
 Mentors: Alexey Khoroshilov (alexey dot khoroshilov at gmail dot com), Jeff Licquia (licquia at linuxfoundation dot org), Vadim Mutilin, Denis Silakov (dsilakov at gmail dot com).
+=====Distributed scheduler development for Linux kernel modules static verification=====
+New Klever framework used for static verification of kernel modules in Linux  Driver Verification (LDV) program consists of three components: Web interface "Bridge", verification tasks generator "Core" and orchestration system "scheduler". The first one allows a user to configure and start a verification process. The second one generates an environment model and inserts asserts into the source code to check given modules against rule specifications, then it prepares verification tasks as a result. The third component schedule runs of  Core and Verification tools to generate verification tasks using Core and solve them using available static verification tools.
+Currently "Scheduler" allows employing a single workstation or a virtual machine to perform verification. In practice, verification requires many verification resources (days and even weeks of CPU time, dozens and sometimes hundreds of GB of RAM). So there is a need in the development of a distributed version of the Scheduler.
+It is supposed to use already existing orchestration systems for this task such as Kubernetes. Moreover, Scheduler was initially designed for distributed execution, so there is either no necessity in rewriting scheduling algorithms or developing the component from scratch.
+**Desired knowledge:** Python, Kubernetes\\
+**Mentors:** Ilja Zakharov, Eugene Novikov (eunovm at gmail dot com)
 =====Develop New LSB Desktop Test Suite=====
@@ Line 24: / Line 34: @@
 **Desired knowledge:** C, Testing\\ Mentors: Alexey Khoroshilov, Roman Zybin
-=====Add support for C++11 to LSB=====
+=====Development of environment model specifications for static verification of Linux Kernel=====
-It is required to capture data of C++11 ABI for [[http://ispras.linuxbase.org/index.php/LSB_Database_Home|LSB database]] using
+The Linux Driver Verification (LDV) program aims to apply heavy-weight static verification tools to find bugs in Linux kernel modules. In contrast to widely used static analysis tools, the approach considers a module as a whole and performs thorough verification empowered by formal techniques.
-[[http://ispras.linuxbase.org/index.php/LSB_DB_Tools|LSB_DB_Tools]].
-**Desired knowledge:** C++, C++ ABI, SQL databases, Perl\\
+The LDV framework generates an environment model as an additional C code for each provided kernel module on the base of its interface and runs a static verification tool which checks only that source code which is reachable with the generated environment model. Before the framework can create the environment model, an expert should prepare two kinds of specifications. The first one just describes declarations of an interface (types, references between them). The second specifies how environment model should triggers callbacks of a kernel module which implement the interface. Environment model specifications strongly influence verification results. Deficiencies in the model can lead to missed bugs as well as to false alarms.
-Mentors: Jeff Licquia, Denis Silakov, Alexey Khoroshilov
+The task assumes the following steps:
+  * Study verification coverage reports generated by the framework. Choose several kernel interfaces which are not covered by the existing specification set.
+  * Study existing environment model specifications and tests (simple kernel modules which implement the interface with stubs) examples. Develop own specifications for interfaces chosen during the previous step. Specifications of both referred kinds are quite short and easy to prepare. But before development, it is necessary to learn DSL languages and study kernel code to understand how the kernel invokes callbacks implemented by kernel modules, how it registers and deregisters them and how it initializes callback parameters.
+  * Obtain and analyze new verification results. Prove then now more code is covered. Analyze new verification results and prepare patches in case of found errors.
+More than one application can be approved.
+**Desired knowledge:** C, understanding of Linux kernel including interrupt handling and deferred works execution.\\
+**Mentors:** Ilja Zakharov, Alexey Khoroshilov
 =====Development of Rule Specifications for Correct Usage of Kernel Core API=====
@@ Line 54: / Line 72: @@
 More than one application can be approved. Formalization of ~5 rules is expected from each student.
-**Desired knowledge:** C, aspect-oriented programming, Linux kernel space API\\ Mentors: Alexey Khoroshilov, Vadim Mutilin, Eugeny Novikov
+**Desired knowledge:** C, aspect-oriented programming, Linux kernel space API\\
+**Mentors:** Alexey Khoroshilov, Vadim Mutilin, Eugeny Novikov
 =====Extend and Update LSB Core Test Suite=====
@@ Line 72: / Line 91: @@
 **Desired knowledge:** C, SEC, model based testing\\ Mentors: Alexey Khoroshilov, Roman Zybin
+=====Add support for C++11 to LSB=====
+It is required to capture data of C++11 ABI for [[http://ispras.linuxbase.org/index.php/LSB_Database_Home|LSB database]] using
+[[http://ispras.linuxbase.org/index.php/LSB_DB_Tools|LSB_DB_Tools]].
+Original idea was proposed in [[https://www.mail-archive.com/lsb-discuss@lists.linux-foundation.org/msg00104.html|lsb-discuss]] mailing list.
+**Desired knowledge:** C++, C++ ABI, SQL databases, Perl\\
+Mentors: Jeff Licquia, Denis Silakov, Alexey Khoroshilov

Wiki

User Tools

Site Tools

Differences

Page Tools