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

После более 2-х лет активной разработки был выпущен инструментарий LDV Tools 0.4. Эта версия включает в себя множество улучшений и исправлений ошибок. В целом она состоит из около 900 изменений, которые были сделаны только в репозитории LDV Tools, не включая подмодули. Наиболее существенные изменения следующие:

• Улучшения существующих спецификаций правил:
  • Module get/put
  • Atomic allocation in interrupt context
  • Mutex lock/unlock
  • Memory allocation under spinlocks
  • NOIO allocation under USB lock
• Поддержка для 25 новых спецификаций правил:
  • Possible TTY NULL dereference
  • Block requests
  • Usage of msleep()
  • USB gadget driver (de)registration
  • Initialization of spinlocks
  • Integer underflow in calling copy_from_user(), copy_to_user(), etc.
  • Usage of spin_lock_irq*()
  • Usage of local_irq_*()
  • RW locks lock/unlock
  • probe() return values
  • Arguments of find_next_zero_bit()
  • Initialization of sysfs attributes
  • USB reference counting
  • Double kfree_skb()
  • Error handling in probe()
  • usb_deregister() and usb_serial_deregister()
  • netif_napi_add()/netif_napi_del()
  • napi_enable()/napi_disable()
  • register_netdev()/unregister_netdev(), alloc_netdev()/free_netdev()
  • Usage of mod_timer()
  • Usage of semaphores
  • Work with clocks
  • RCU read sections nesting
  • RCU update operations inside read sections
  • Initialization of completions
• Исправление шаблонов для нескольких структур драйверов с целью генерации корректных моделей окружения.
• Поддержка C Instrumentation Framework - удобного в использовании интерфейса для Aspectator.
• Поддержка повторного использования блоков аспектных файлов и соответствующая реорганизация всех существующих спецификаций правил.
• Добавлена возможность выполнять запросы по исходному коду с помощью Aspectator, которая используется при построении спецификаций правил на основе инструментируемого кода (см. соответствующую новость) и при генерации моделей окружения.
• Поддержка более удобного для пользователей интерфейса подключения инструментов верификации.
• Переход на версию 2.7.1 инструмента верификации BLAST (инструмент верификации, который используется в LDV Tools по умолчанию).
• Улучшение интеграции с инструментом верификации CPAchecker, который был включен, как подмодуль LDV Tools.
• Интеграция с инструментом верификации UFO.
• Поддержка общего формата трасс ошибок и улучшение визуализации трасс ошибок различных инструментов верификации.
• Поддержка базы знаний для автоматизации разметки результатов верификации.
• Поддержка автоматической валидации LDV Tools и инструментов верификации на известных ошибках в ядре Linux.
• Генерация покрытия для отладки LDV Tools и различных анализов инструмента верификации CPAchecker.

Валидация LDV Tools 0.4 с разными инструментами верификации на 38 известных ошибках в ядре Linux показала, что:

• BLAST способен выявить 11 из них.
• CPAchecker способен выявить 10 из них.

Соответствующий исходный код можно увидеть в репозитории по тэгу v0.4. Инструкции по скачиванию и установке LDV Tools описаны здесь.