Go back to the main GSoC Linux Foundation page

Mailing list: lsb-discuss at lists dot linux-foundation dot org

IRC: #lsb on irc.freenode.net

Workgroup Resources

Code License: GPL/BSD, specs: GNU FDL

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

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)

LSB Desktop tests [1,2] is a part of LSB certification tests. Existing tests do not cover all interfaces included into LSB and LSB specification continues to grow (http://linuxbase.org/navigator/browse/status.php). The goal of the project is to develop tests for newly included libraries and for interfaces that have no tests yet (http://linuxbase.org/navigator/coverage/cov2.php).

Gtk3/Gdk3 and friends are at the moment very high on our list of untested items. The test development ideally should be coordinated with upstream projects so the tests can be useful for them as well.

[1] http://bzr.linuxfoundation.org/loggerhead/lsb/devel/desktop-test/files
[2] http://bzr.linuxfoundation.org/loggerhead/lsb/devel/t2c-desktop-tests/files

Desired knowledge: C, Testing
Mentors: Alexey Khoroshilov, Roman Zybin

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.

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.

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

Linux Driver Verification (LDV) program is devoted to developing an integrated framework for device drivers verification and adopting leading edge research results to enhance quality of verification tools. Currently LDV tools are used to check Linux device drivers against several safety rule specifications, each of them formally defines what is correct usage of a particular part of kernel core API. Another way of looking at the safety rules is that a rule represents one or more typical misuse of kernel core API.

By the moment, the framework contains around 30 rule specifications that has already helped to find and fix more than 300 issues in device drivers of vanilla Linux kernel.

This project (or several ones) is aimed at extending number of rules supported by the framework.

We have a collection of several dozens rules written in informal way, but other rules can be used as well. Formalization process usually includes the following steps:

• identification of all elements of kernel core API relevant to the rule;
• writing a rule specification 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 assertions (that represents misuse of kernel core API);
• writing unit tests covering all the interfaces;
• checking all drivers against the rule, analyzing results, reporting bugs and fixing the rule specification.

Rule specifications are written in a mix of C code and AspectJ-like notation that allows to merge the model code with original source code of device driver.

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

LSB Core tests [1,2] is the main part of LSB certification tests. Originally they were developed for POSIX (IEEE Std 1003.1-1990) and LSB 3.1. LSB specification was expanded since that time (http://linuxbase.org/navigator/browse/status.php). The goal of the project is to fix open issues in the tests, i.e. to fix issues appearing on modern Linux distributions and to accomodate all relevant changes in text of specifications, as well as to expand coverage of the test suite to newly added LSB Core interfaces.

VSX-PCTS was implemented using TET/VSXgen test harness. The OLVER test suite was developed using model-based testing technology UniTESK. The technology follows well-known Design by Contract approach to represent formal specifications. Program contracts consist of preconditions and postconditions of interface operations and data type invariants. The main advantage of program contracts is that they enable automatic construction of test oracles that check the conformance of the target system behavior to the specifications.

Traceability of formal specifications to text of original LSB/POSIX specifications is supported using the following ideas:

• each elementary requirement in original specification obtains a unique identifier;
• each of the requirements is explicitly linked to a fragment of text in the original specification;
• all checks in preconditions and postconditions are marked by identifiers of corresponding requirements.

[1] http://bzr.linuxfoundation.org/loggerhead/lsb/devel/olver-core-tests/files
[2] http://bzr.linuxfoundation.org/loggerhead/lsb/devel/runtime-test/files

Desired knowledge: C, SEC, model based testing
Mentors: Alexey Khoroshilov, Roman Zybin

It is required to capture data of C11 ABI for [[http://ispras.linuxbase.org/index.php/LSB_Database_Home LSB database]] using LSB_DB_Tools. Original idea was proposed in lsb-discuss mailing list. Desired knowledge: C, C++ ABI, SQL databases, Perl
Mentors: Jeff Licquia, Denis Silakov, Alexey Khoroshilov