16.01.2015: Выпущен инструментарий LDV Tools 0.7

В LDV Tools 0.7 вошло достаточно большое количество улучшений и исправлений ошибок:

• Поддержка совместимости с ядром Linux версий 3.17-3.19.
• Улучшения в 12 существующих спецификациях правил:
  • sysfs_attr_init() call before device_create_file() call.
  • usb_deregister()/usb_serial_deregister().
  • Usb alloc/free urb.
  • Possible TTY NULL dereference.
  • Atomic allocation in interrupt context.
  • Memory allocation inside spinlocks.
  • NOIO allocation under usb_lock.
  • Initialization of completion.
  • Locking and unlocking SDIO bus.
  • Underflow in call copy_from_user() etc..
  • All allocated socket buffers should be freed.
  • Error handling in probe().
• Поддержка верификации на удаленном компьютере с помощью BLAST в контейнере Docker.
• Поддержка верификации в облаке CPAchecker.
• Поддержка публичного пула ошибок.
• Большое количество исправлений ошибок и реализация новой функциональности в Rule Instumentor и CIF - компонентах инструментария LDV Tools, которые используются для инструментирования верифицируемого исходного кода.
• Многочисленные улучшения и исправления ошибок в компонентах для загрузки и визуализации результатов верификации.

Результаты валидации инструментария LDV Tools версий 0.7 и 0.6 с различными инструментами верификации на наборе, состоящем из 41 известной ошибки в ядре Linux, представлены ниже в таблице.

Оба инструмента верификации смогли найти на две ошибки больше благодаря улучшениям в спецификациях правил sysfs_attr_init() call before device_create_file() call и usb_deregister()/usb_serial_deregister().

Исходный код LDV Tools 0.7 доступен в репозитории по тегу v0.7. Инструкции по скачиванию и установке представлены здесь.