Project

General

Profile

News

Version 0.8 of LDV Tools released

Added by Vadim Mutilin over 3 years ago

LDV Tools 0.8 comes with the following improvements:

Results of validation of LDV Tools 0.8 and LDV Tools 0.7 with different verification tools on 41 known bugs in the Linux kernel are presented in the table below.

LDV Tools 0.8 LDV Tools 0.7
BLAST CPAchecker BLAST CPAchecker
Found bugs 19 18 19 15
Missed bugs Due to bugs in verification tools 3 2 3 2
Out of memory (63 gigabytes) 2 0 1 2
Timeouts (50 minutes) 0 5 0 6
Due to other reasons 17 16 18 16

The new version of CPAchecker was able to find three more reference bugs in Linux kernel thanks to improvements described here.

The source code repository can be browsed by v0.8 tag. To get and to install LDV Tools see instructions. If you want to use prebuilt LDV Tools, please follow our LDV Tools in Docker instructions.

Version 0.7 of LDV Tools released

Added by Evgeny Novikov almost 4 years ago

LDV Tools 0.7 comes with quite a lot improvements and bug fixes:

Results of validation of LDV Tools 0.7 and LDV Tools 0.6 with different verification tools on 41 known bugs in the Linux kernel are presented in the table below.

LDV Tools 0.7 LDV Tools 0.6
BLAST CPAchecker BLAST CPAchecker
Found bugs 19 15 17 13
Missed bugs Due to bugs in verification tools 3 2 3 2
Out of memory (63 gigabytes) 1 2 1 2
Timeouts (50 minutes) 0 6 0 6
Due to other reasons 18 16 20 18

Both BLAST and CPAchecker were able to find two more reference bugs thanks to improvements in rule specifications sysfs_attr_init() call before device_create_file() call and usb_deregister()/usb_serial_deregister().

The source code repository can be browsed by v0.7 tag. To get and to install LDV Tools see instructions.

2nd Google Summer of Code 2014 project was merged to master

Added by Evgeny Novikov almost 4 years ago

Vitaly Mordan successfully finished Google Summer of Code 2014 project Public Pool of Bugs in Linux Kernel Modules under Evgeny Novikov supervision.

In summer of code Vitaly made the following:
  • Wrote a comprehensive specification of Public Pool of Bugs in which all requirements of LDV Tools developers for that project were considered.
  • Extended linuxtesting.org in order to present LDV Tools verification results beyond the ISP RAS. New web pages were developed to represent full information about found bugs/false alarms (for the Linux kernel developers) and to edit information (for the LDV Tools developers).
  • Extended LDV Knowledge Base and LDV Analytics Center in order to make it possible to publish verification results (such as kernel version, module, corresponding error trace, verdict, etc) to linuxtesting.org and to synchronize them later.
  • Developed an authorization module for LDV Analytics Center to exclude an accidental publishing of unnecessary data, so only authorized users could publish verification results.

All changes to LDV Tools components were merged to master in 363f810.

Completing this project made possible to share any new found potential bugs in Linux kernel modules with its full description with the Linux kernel developers. In future this project will increase the number of found bugs in Linux kernel modules with the help of LDV Tools.

Google Summer of Code 2014 project was merged to master

Added by Evgeny Novikov almost 4 years ago

Ilja Zakharov successfully finished Google Summer of Code 2014 project Parallel Verification of Linux Kernel Modules under Evgeny Novikov supervision.

During the project Ilja made an overview of available technologies of cloud and distributed computing which are suitable for software verification tools deployment - the actual task since such tools are characterized by high time and memory consumption. Working in touch with other LDV developers he also contributed to the new perspective version of LDV Tools which is still under development. As a result he improved performance of verification task generation and proceeded with a solution of an infrastructure for establishing distributed Docker-based verification. As a part of the project Ilja also implemented verification on a remote host using BLAST in a Docker container and CPAchecker cloud web-interface task submitting. The latter was merged to master in 960e64e.

Version 0.6 of LDV Tools released

Added by Evgeny Novikov about 4 years ago

LDV Tools 0.6 includes the following most important changes:

Results of validation of LDV Tools 0.6 and LDV Tools 0.5 with different verification tools on 41 known bugs in the Linux kernel* are presented in the table below.

LDV Tools 0.6 LDV Tools 0.5
BLAST CPAchecker BLAST CPAchecker
Found bugs 17 13 15 14
Missed bugs Bugs in verification tools 3 2 3 3
Out of memory (63 gigabytes) 1 2 1 0
Timeouts (50 minutes) 0 6 0 4
Unsupported rule specifications 0 0 7 7
Others 20 18 15 13

Both BLAST and CPAchecker were able to find one more bug thanks to improvements in rule specification SKB allocation in pm_runtime context. Additionally BLAST has found a new bug with one of the new rule specifications. CPAchecker has lost ability to detect 3 bugs due to degradation in analysis time, while it has found a bug that led to an exception before.

The source code repository can be browsed by v0.6 tag. To get and to install LDV Tools see instructions.

* This validation benchmark has many differences from the one used earlier for validating LDV Tools 0.5.

Version 0.5 of LDV Tools released

Added by Evgeny Novikov over 4 years ago

The major feature of this release is a control groups based resource manager aimed to limit and to count resource consumption of verifiers. Linux control groups allow to perform very accurate measurements without any noticeable overhead. Other important changes are as follows:
  • Support for automatic verification of modules of the Linux kernel in user-defined configurations, including different computer architectures.
  • Addition of the new rule specification Locking and unlocking SDIO bus.
  • Improvements in existing rule specifications: Module get/put and Block requests.
  • Fixing all known segmentation faults in Aspectator.
  • Switch to 2.7.2 version of BLAST verifier.
  • Support of CBMC verifier as one of LDV Tools' back ends.
  • Introducing a standalone error trace visualization tool.
Validation of LDV Tools 0.5 with different verifiers on 37 known bugs in the Linux kernel showed that:
  • BLAST is able to detect 13 of them.
  • CPAchecker is able to detect 11 of them.

In comparison with LDV Tools 0.4 6 known bugs were removed from the validation benchmark since they do not fit existing rule specifications, while 5 new known bugs were added to the benchmark (3 due to support of user-defined configurations, 1 due to addition of the new rule specification and 1 due to determining of an appropriate environment model). LDV Tools can detect two of those new bugs with help of BLAST verifier.

The source code repository can be browsed by v0.5 tag. To get and to install LDV Tools see instructions.

Google Summer of Code 2013 project was completed

Added by Evgeny Novikov almost 5 years ago

Master's student Ilja Zakharov under Vadim Mutilin supervision successfully finished Google Summer of Code 2013 project Generation of Environment Model for Verification of Multi-module Device Drivers for The Linux Foundation.

Ilja worked in the following directions:
  1. Experiments with extraction of interconnected Linux kernel modules.
  2. New implementation for a Linux-related stack of components of the LDV Tools.

Ilja developed a new approach for extracting a graph of all interconnected Linux kernel modules and a new method for a graph clusterization specific for verification purposes. Obtained groups of modules rarely exceed 5 modules in size. Further research for generating environment model and study of corner cases lie ahead.

Kernel Manager, Build Command Extractor and Command Stream Divider components of the LDV Tools were completely redesigned. The most notable features that they support now include an adjustment on the basis of an extendable common configuration, a results caching, various strategies of module extraction and an extracting of the Linux kernel modules for the ARM architecture. Also a new architecture of these components allow to avoid all old bugs like this. Integration of the components with LDV Tools is ongoing.

Version 0.4 of LDV Tools released

Added by Evgeny Novikov about 5 years ago

After more then 2 years of active development we are happy to announce that we released version 0.4 of LDV Tools. This version includes a lot of improvements and many bug fixes. In total it consists of about 900 commits that were made just in the LDV Tools repository not including submodules. The most significant changes are: Validation of LDV Tools 0.4 with different verifiers on 38 known bugs in the Linux kernel showed that:
  • BLAST is able to detect 15 of them.
  • CPAchecker is able to detect 13 of them.

The source code repository may be browsed by v0.4 tag. To get and to install LDV Tools see instructions.

3rd Google Summer of Code 2012 project was completed

Added by Evgeny Novikov about 6 years ago

In Google Summer of Code 2012 Ph.D. student Denis Efremov managed by mentor Alexey Khoroshilov has successfully developed a project titled Formalization of Correct Usage of Kernel Core API for The Linux Foundation.

Denis implemented 12 formal models for safety rules that help him to find a lot of bugs in Linux kernel drivers:
  1. Enabling interrupts while in an interrupt handler (commits 1, acked 1)
  2. might_sleep functions in interrupt context (found the same results as less general variants of the given rule)
  3. Spinlocks acquisition in process and interrupt contexts (5 suspicious drivers)
  4. local_irq_enable/disable and local_irq_save/restore order (commits 1, 2)
  5. rcu_dereference() outside of rcu_read_lock/unlock (commits 1, 2, 3, 4)
  6. might_sleep functions with disabled interrupts (7 suspicious drivers)
  7. Inlined functions marked with EXPORT_SYMBOL (commits 1)
  8. might_sleep functions in spinlock context (verification results need to be carefully analyzed)
  9. might_sleep functions in rcu_read_lock/unlock (verification results need to be carefully analyzed)
  10. Requesting a threaded interrupt without a primary handler and without IRQF_ONESHOT (needs more accurate driver environment)
  11. Initialization functions marked with EXPORT_SYMBOL (found bugs seems not to be critical)
  12. BUG like macros in interrupt context (rule highly depends on user purposes, thus it was rejected)
To develop 5 of these rule models Denis has suggested a new approach of an automatic construction of a Linux kernel core model. This approach is based on a suggestion if some program interface may invoke directly or indirectly some specific program interface (like might_sleep macro) then it can be marked respectively (e.g. as might_sleep interface). The approach was implemented in the following way:
  1. Creates list of program interfaces used by some Linux kernel module, in particular by a driver.
  2. Linux kernel source code is analyzed with help of cscope tool.
  3. On the basis of a generated cscope base a call graph containing program interfaces of interest (e.g. might_sleep macro) is created.
  4. Intersects lists of program interfaces obtained at 1st and 3rd steps. Thus obtains a list of program interfaces that can, say, sleep, and that are used by the module.
  5. Constructs a rule model on the basis of the list obtained at 4th step. For instance, checks a specific context for program interfaces from the given list.

Several rule models were merged to the master branch of the Linux Driver Verification project. To merge other rule models we need to integrate tools developed by Denis with LDV tools.

2nd Google Summer of Code 2012 project was merged to master

Added by Evgeny Novikov about 6 years ago

In Google Summer of Code 2012 Ph.D. student Mikhail Mandrykin managed by mentor Alexey Khoroshilov has successfully developed a project titled Formalization of Correct Usage of Kernel Core API for The Linux Foundation. A corresponding branch was merged to the master branch of the Linux Driver Verification project in 5ee5b4e.

Mikhail implemented 5 formal models for safety rules that help him to find a lot of bugs in Linux kernel drivers:
  1. Possible TTY NULL dereference (commits 1, 2)
  2. The gadget driver (de)registration (commits 1, 2, 3, 4, 5)
  3. Refcounting with usb_get_dev()/usb_put_dev() (24 suspicious drivers)
  4. Don't call kfree_skb twice (no actual problems were found)
  5. Error handling in probe() (commits 1 and 5 suspicious drivers)
(1-10/14)

Also available in: Atom