Project

General

Profile

News

MicroTESK: MicroTESK to be presented at DATE 2013

Added by Alexander Kamkin almost 5 years ago

The MicroTESK tool will be presented at the University Booth exhibition of the DATE 2013 conference - one of the biggest European events for electronic system design and test. The conference & exhibition will take place on March 18-21 in Grenoble, France.

DATE, the Design, Automation and Test Conference and Exhibition, is the unique European event bringing together researchers together researchers, users and vendors as well as specialists in design, test and manufacturing of electronic circuits and systems. The University Booth is a part of the DATE program. It is sponsored by the DATE Sponsor Society, by the European Design and Automation Association, the EDA Consortium, the IEEE Computer Society – TTTC and CEDA, ECSI, ACM SIGDA, and the Russian Academy of Sciences. Read more...

Pictures of DATE 2013

C++TESK Testing ToolKit: C++TESK Testing ToolKit v1.0.21 released

Added by Alexander Kamkin about 5 years ago

C++TESK Testing ToolKit v1.0.21 has been released. The following things have been done.

  • Process table and scheduler have been refactored
  • Buffering of implementation reactions has been implemented
  • Support of pipelined implementation reactions has been added
  • Experimental facilities for FSM description have been included
  • Failure diagnostics has been improved

The toolkit can be downloaded from the page http://forge.ispras.ru/projects/cpptesk-toolkit/files.

Bugless New Year!

Local Support Project: Ограничение доступа к директориям

Added by Alexey Demakov about 5 years ago

Реализована возможность органичения доступа к директориям, доступным через браузер (например, апдейт-сайтам закрытых проектов).
Для этого в самой директории или в любой из родительских директорий следует добавить в файл .htaccess идентификатор проекта:

RedmineProject _projectid_

Файлы из этой директории будут доступны только членам проекта projectid с правом просмотра репозитория.

BLAST: BLAST 2.7.1 has been released

Added by Mikhail Mandrykin over 5 years ago

You may download sources and binaries on the Files page of the BLAST project. See also the original project page.

Release notes

This version fixes a couple of bugs exposed at the Competition on Software Verification at TACAS'12. We advise you to use 2.7.1 instead of 2.7.

Analysis

  • Fix bug that all undefined local variables, such as int __VERIFIER_nondet_int() { int val; return val; }, were treated as equal in all calls of a function.

Infrastructure improvements

  • Binary builds are now compatible with RHEL 5.

Local Support Project: Redmine 2.1.2

Added by Alexey Demakov over 5 years ago

Уважаемые коллеги!
Проект forge.ispras.ru переехал на новый сервер.
Redmine обновился до версии 2.1.2. Все плагины для начала отключены.
Просьба сообщать об обнаруженных проблемах.

KEDR: KEDR 0.4 released

Added by Alexey Khoroshilov over 5 years ago

KEDR is an extensible system for dynamic analysis of Linux kernel modules (device drivers, file system modules, etc.). KEDR tools operate on the modules chosen by the user and can detect memory leaks, perform fault simulation and more.

This release provides several enhancements and various fixes compared to version 0.3. The most significant changes in this version:
  • KEDR now supports kernel versions 3.3-3.6.
  • LeakCheck has been redesigned: the analysis engine has been separated from data collection which makes the tool easier to maintain and to extend. The API it provides allows to use the memory leak detector in more cases than before.
  • Handling of the information about signatures of the processed functions has been revisited to remove duplicate code and make the components involved easier to configure and to maintain.
  • 12 more functions that allocate or deallocate memory are now processed, so are the functions kfree_rcu() expands to.
  • Many fixes have been made in LeakCheck, fault simulation and other subsystems.
  • Support for kernel version 2.6.31 has been dropped. The minimum supported kernel version is now 2.6.32.

Linux Driver Verification: 3rd Google Summer of Code 2012 project was completed

Added by Evgeny Novikov over 5 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.

Linux Driver Verification: 2nd Google Summer of Code 2012 project was merged to master

Added by Evgeny Novikov over 5 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)

Linux Driver Verification: Google Summer of Code 2012 project was merged to master

Added by Evgeny Novikov over 5 years ago

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.

(231-240/291)

Also available in: Atom