23.08.2021: Поиск ошибок использования памяти в ядре Linux

Опубликовано Vadim Mutilin в Пнд, 23/08/2021 - 16:49

Лутовинова Надежда завершила проект GSoC “Поиск ошибок, связанных с памятью, в ядре Linux и улучшение спецификации модели окружения для статической верификации”. Этот проект был связан с поиском ошибок, связанных с памятью, в коде драйверов Linux. В процессе работы Надежда использовала Klever - фреймворк для верификации программного обеспечения, созданный для автоматической проверки программ, написанных на языке программирования C. С помощью него она анализировала код ядра Linux версии 5.12-rc3.

По ее мнению, Klever - довольно удобный инструмент. При обнаружении возможной ошибки отображаются необходимые условия для переменных и порядок вызовов функций, приводящих к ошибке. Однако не всегда понятен принцип поиска и выделения ошибок. Бывает, что Клевер определяет что-то как баг, пропуская ранее точно такую же возможную ошибку.

Надежда проанализировала 18 вердиктов, предварительно помеченных как ошибки и по которым оставались вопросы о верности их определения. Из них:

  • 7 ложных предупреждений:
    • 3 - связанны с генератором моделей окружения EMG (Environment Model Generator).
    • 4 - связанны с неполнотой моделей некоторых функций.
  • 8 ошибок:
    • 5 сообщено, подготовлены патчи (см. ниже).
    • 3 одинаковых ошибках в разных модулях сообщено в одном сообщении.
  • 3 остались неопределенными.

Большинство трасс были связаны с регистрацией обработчика прерывания до инициализации каких-то необходимых данных. В некоторых файлах для предотвращения ошибок были использованы проверки условий, но Klever неправильно их обработал из-за проблем, описанных выше.

Патчи: