User Tools

Site Tools


gsoc:2015-gsoc-lsb-projects

2015 GSoC LSB projects

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, Vladimir Rubanov, Denis Silakov (dsilakov at gmail dot com).

Package Dependencies Support in LSB Database and Navigator

LSB Navigator is a web portal that provides users with different information about LSB itself and Linux ecosystem in general. In particular, it displays data about packages, libraries, binary symbols and other entities available in different Linux distributions. All this information is stored in the LSB Database and collected by automated tools.

An important aspect of distribution structure which is not currently reflected in the database in package dependencies. For users and developers it would be useful to know what every package provides/requires and which packages should be installed in particular distribution to satisfy given dependencies. The reason for the lack of this feature is that LSB itself always tried to eliminate the need for package dependencies. However, in real life it is hard to completely get rid of them and services that displays infrormation about package dependencies are quite popular among developers.

However, existing services (such as http://rpm.pbone.net/, http://pkgs.org/ or http://rpmfind.net/) are maintained by volunteers and provides information about only a limited set of distributions with preference for the community systems. The LSB Database contains data about wider range of enterprise distributions, so we believe that LSB Navigator with additional data will supplement existing services, not compete with them. And in any case the advantage of LSB Navigator is that it can provide additional information about package executable files, libraries, exported symbols, etc.

The aim of this project is to add possibility to collect data about package dependencies to the LSB data collection tools and implement support for these data in LSB Navigator (lists of package dependencies provides/requires, search among package dependencies and more intellectual features such as comparison of packages from different distributions). It is possible that the schema of the LSB Database will have to be improved, as well.

Desired knowledge: Perl, PHP, MySQL/Mariadb, basic knowledge of Linux packages (RPM and Deb formats).
Mentor: Denis Silakov

Extend and Update LSB Core Test Suite

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

Develop New LSB Desktop Test Suite

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

Formalization and Checking of Correct Usage of Kernel Core API

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 rules, 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 rules that has already helped to find and fix more than 200 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 finite state machine like formal model 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 error states (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.

A notation used for formal representation of the rules is C code and AspectJ-like notation to merge the model code with original source code of device driver in appropriate places.

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

gsoc/2015-gsoc-lsb-projects.txt · Last modified: 2016/07/19 01:24 (external edit)