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:
- Enabling interrupts while in an interrupt handler (commits 1, acked 1)
- might_sleep functions in interrupt context (found the same results as less general variants of the given rule)
- Spinlocks acquisition in process and interrupt contexts (5 suspicious drivers)
- local_irq_enable/disable and local_irq_save/restore order (commits 1, 2)
- rcu_dereference() outside of rcu_read_lock/unlock (commits 1, 2, 3, 4)
- might_sleep functions with disabled interrupts (7 suspicious drivers)
- Inlined functions marked with EXPORT_SYMBOL (commits 1)
- might_sleep functions in spinlock context (verification results need to be carefully analyzed)
- might_sleep functions in rcu_read_lock/unlock (verification results need to be carefully analyzed)
- Requesting a threaded interrupt without a primary handler and without IRQF_ONESHOT (needs more accurate driver environment)
- Initialization functions marked with EXPORT_SYMBOL (found bugs seems not to be critical)
- 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:
- Creates list of program interfaces used by some Linux kernel module, in particular by a driver.
- Linux kernel source code is analyzed with help of cscope tool.
- On the basis of a generated cscope base a call graph containing program interfaces of interest (e.g. might_sleep macro) is created.
- 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.
- 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.
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:
- Possible TTY NULL dereference (commits 1, 2)
- The gadget driver (de)registration (commits 1, 2, 3, 4, 5)
- Refcounting with usb_get_dev()/usb_put_dev() (24 suspicious drivers)
- Don't call kfree_skb twice (no actual problems were found)
- Error handling in probe() (commits 1 and 5 suspicious drivers)
During Google Summer of Code 2012 Ph.D. student Evgeny Novikov managed by mentor Alexey Khoroshilov has successfully developed a project titled Advanced Source Code Instrumentation for the Linux Driver Verification Project for The Linux Foundation. A corresponding branch was merged to the master branch of the Linux Driver Verification project in 0491d9a.
The main feature implemented within the given project was ability to construct formal models of safety rules on the basis of program source code in the way independent of static verifier used for checks of rule models. Using this feature the LDV team enhanced existing rule models (Mutex lock/unlock and Spinlocks lock/unlock) and developed 7 new ones. Verification of Linux kernel drivers against these rule models with help of BLAST and CPAchecker tools demonstrated considerably lower rate of false positives in comparison with results obtained earlier and helped to discover several critical bugs.
In future we are planning to integrate the suggested approach with other approaches of rule models construction, e.g. based on automatic analysis of the Linux kernel core.
C++TESK Testing ToolKit v1.0.20 has been released. The following things have been done.
- Bugs in static data initialization have been fixed
- Source code detalization of the interface usage conflicts has been implemented
- Support of project building from the Eclipse IDE plugin has been added
- Support of distrubuted testing from the Eclipse IDE plugin has been added
- Problems with test launching from the Eclipse IDE plugin have been solved
The toolkit can be downloaded from the page http://forge.ispras.ru/projects/cpptesk-toolkit/files.
C++TESK Testing ToolKit v1.0.19 has been released. The following things have been done.
- macro CPPTESK_ITERATION_BEGIN_IF (IBEGIN_IF) has been implemented
- support of local variables in CPPTESK_ITERATION_ACTION (IACTION) blocks has been done
- engine's internal assertion 'stimulus id is out of range' has been disabled
- some bugs in the error diagnostics subsystem has been fixed
- Eclipse IDE plugin installation has been simplified
The toolkit can be downloaded from the page http://forge.ispras.ru/projects/cpptesk-toolkit/files.
C++TESK Testing ToolKit was demonstrated at the DATE 2012 University Booth exhibition held in Dresden in 13-15 March. The presentation raised interest of researchers and practitioners from different countries including Austria, Estonia, Germany, etc.
На сайте начал появляться спам. Для защиты от него мы принуждаем новых пользователей при регистрации разгадывать капчу. Радуйтесь, вы помогаете оцифровке книг!
C++TESK Testing ToolKit v1.0.18 has been released. The following things have been done.
- Virtual method invariant() has been added to the message class
- Macros for declaring arrays of interfaces have been implemented (CPPTESK_DECLARE_{INPUT|OUTPUT}_ARRAY, CPPTESK_DECLARE_{INPUT|OUTPUT}_ARRAY_2D, etc.)
- New macros for declaring/defining interface adapters have been added (CPPTESK_DEFAULT_{INPUT|OUTPUT}_ADAPTER, CPPTESK_SET_DEFAULT_{INPUT|OUTPUT}_ADAPTER and CPPTESK_{DECLARE|DEFINE}_DEFAULT_{INPUT|OUTPUT}_ADAPTER)
- Macros CPPTESK_SET_{IFACE|INOUT}_ADAPTER have been removed
- New macros for randomized generation have been implemented (CPPTESK_RANDOM(_{WIDTH|FIELD|BITS|RANGE})_EXCLUDING)
- Automatic tracking of interface usage coverage has been included
- Macro CPPTESK_ADD_NONRANDOMIZABLE_FIELD has been added
- Macros CPPTESK_WITH_PROBABILITY, CPPTESK_ELSE_WITH_PROBABILITY and CPPTESK_ELSE have been implemented
- Callbacks onCycleBegin() and onCycleEnd() have been added
- Further improvement of the Eclipse IDE plugin has been made
- Several bugs in the error diagnostic subsystem have been fixed
- CPPTESK_SHORT_NAMES is activated automatically if CPPTESK_SHORT_SHORT_NAMES is defined
The toolkit can be downloaded from the page http://forge.ispras.ru/projects/cpptesk-toolkit/files.
Redmine обновился до 1.3.0.stable.8748
Установлен плагин Redmine Mylyn connector, который позволяет подключить задачи из Redmine к Mylyn.
Mylyn - это встроенная в Eclipse платформа для управления задачами и жизненным циклом приложения. Эта платформа предоставляет возможность подключения сторонних инструментов.
C++TESK Testing ToolKit v1.0.17 has been released. The following things have been done.
- Error diagnostics has been improved
- Macros CPPTESK_DECLARE_BIT_ARRAY, CPPTESK_DECLARE_FIELD_ARRAY, etc. have been implemented
- Several bugs have been fixed
The toolkit can be downloaded from the page http://forge.ispras.ru/projects/cpptesk-toolkit/files.
Merry Christmas and Happy New Year!