31.08.2020: Разработка спецификаций модели окружения для статической верификации ядра ОС Linux

Лутовинова Надежда закончила проект GSoC 2020 “Разработка спецификаций модели окружения для статической верификации ядра Линукс” под эгидой The Linux Foundation.

В проекте она использовала Klever - инструмент проверки программного обеспечения, созданный для автоматической проверки программ, написанных на языке программирования C. Klever включает в себя необходимые спецификации для обнаружения проблем безопасности памяти в ядре Linux. Клевер анализирует код и выдает предупреждения о возможных ошибках. Не все из них настоящие. Надежда проанализировала вердикты Клевера и разметила их как реальные и ложные. Ложные предупреждения могут возникать из-за неточностей в различных компонентах Klever. В частности, в методе SMG (Symbolic Memory Graph), который используется для обнаружения проблем безопасности памяти, и в EMG (Environment Model Generator), который генерирует модели среды для анализируемых функций.

Клевер - довольно удобный инструмент. Он отображает не только последовательность вызовов функций, которая привела к ошибке, но и необходимые для этого условия на переменные. Когда нет необходимой информации, он продолжает работать, исследуя различные значение. Также можно сравнить запуски с разными моделями и детально увидеть различия в результатах. В то же время есть некоторые отрицательные моменты, которые заметила Надежда. Например, есть проблемы с отображением трасс ошибок (неполное отображение строк кода, отсутствие четкого соответствия между переданными аргументами и внутренними именами функций в трассах, некоторые файлы не могут быть открыты по ссылке из трасс и т.д.). Также система тегов не совсем очевидна. Необходимость делать модели для множества функций для повышения точности также усложняет работу с этим инструментом.

Изначально предполагалось разработать и усовершенствовать модели операций со строками. Но ошибок, связанных с неправильными строковыми моделями, в ходе анализа обнаружено не было. Так что модели для функций строк не нуждались в улучшении. Чаще всего ошибки были связаны с неполнотой модели окружения ядра, особенно с операциями из debugfs.h, и неполнотой модели для операций со списками.

Анализ предупреждений

Надежда проанализировала 62 предупреждения для модулей ядра Linux версии 5.7-rc7. Она нашла две ошибки и сообщила об этом разработчикам. Для первой ошибки она подготовила патч, который был принят, см. LKML. Отчет о второй ошибке можно найти здесь.

60 ложных предупреждений было проанализировано и размечено следующим образом:

• 1 связана с проблемой в Klever (пр. ошибка в отображении трассы)
• 13 связано с проблемой в SMG (пр. SMG одновременно предполагала противоположные утверждения)
• 5 связано с EMG моделями (пр. утечка памяти из-за неверного освобождения памяти)
• 41 связано с неполными моделями функций (пр. без модели для __builtin_mul_overflow() модель для devm_kcalloc() работает некорректно и происходит разыменование нулевого указателя)
  • 12 связаны с отсутствием моделей для некоторых функций из debugfs.h (пр. без модели для debugfs_create_dir() последующее выполнение debugfs_remove(), которая работает с указателем, возвращенном debugfs_create_dir(), происходит некорректно) [Тэги: EMG, EnvSpec, debugfs]
  • 6 связаны с неполнотой модели для операций со списками (пр. __list_add не добавляет новый элемент в список и возникает утечка памяти) [Тэги: KernelModel, list_add]
  • 4 из них связаны с отсутствием модели для nvmem_cell_read() [Тэги: EMG, EnvSpec]
  • 2 из них связаны с отсутствием модели для acpi_evaluate_object() [Тэги: KernelModel]
  • 2 из них связаны с отсутствием модели для is_acpi_device_node() [Тэги: KernelModel]
  • 2 из них связаны с отсутствием модели для for drm_dev_init() [Тэги: EMG, EnvSpec]
  • 1 из них связана с отсутствием модели для kvfree() [Тэги: KernelModel]
  • 1 из них связана с отсутствием модели для acpi_evaluate_object_typed() [Тэги: KernelModel]
  • 1 из них связана с отсутствием модели для memdup_user() [Тэги: KernelModel]
  • 1 из них связана с отсутствием модели для __builtin_mul_overflow() [Тэги: KernelModel]
  • 1 из них связана с отсутствием модели для i2c_smbus_read_block_data() [Тэги: KernelModel, i2c_smbus_read_block_data]
  • 1 из них связана с отсутствием модели для devm_hwrng_register() [Тэги: EMG, EnvSpec]
  • 1 из них связана с отсутствием модели для vchan_init() [Тэги: EMG, EnvSpec]
  • 1 из них связана с отсутствием модели для iscsi_boot_create_acpitbl() [Тэги: EMG, EnvSpec]
  • 1 из них связана с отсутствием модели для mipi_dsi_device_register_full() [Тэги: EMG, EnvSpec]
  • 1 из них связана с отсутствием модели для drm_random_order() [Тэги: EMG, EnvSpec]
  • 1 из них связана с отсутствием модели для gb_hd_create() [Тэги: EMG, EnvSpec]
  • 1 из них связана с неполнотой модели для acpi_get_object_info() [Тэги: CIF]
  • 1 из них связана с неполнотой модели для krealloc() [Тэги: CIF]

Спецификация списков

Надежда разработала улучшения для модели списков для Klever и протестировала их на ядре Linux версии 5.7-rc7. Улучшения можно найти на github.

Результаты внедрения новых моделей списков: