Верификация модулей ядра ОС Linux

Ядро ОС Linux состоит из базовых компонентов, реализующих основную функциональность операционной системы (распределение процессорного времени, управление памятью, межпроцессным взаимодействием и т.д.), и подгружаемых модулей, в которые вынесена дополнительная функциональность (файловые системы, сетевые протоколы, драйверы устройств и т.д.). На подгружаемые модули приходится более 70% исходного кода ядра, а внимания их разработке уделяется нередко меньше, чем базовым компонентам. Поэтому неудивительно, что большинство ошибок, приводящих к зависаниям, падениям и некорректной работе всей ОС, содержится именно в исходном коде модулей.

В Центре верификации ведётся работа над двумя проектами, нацеленными на повышение качества подгружаемых модулей ядра ОС Linux. В первом проекте реализуется метод статического анализа исходного кода с целью выявления типовых ошибок в работе модулей ядра, и в первую очередь, драйверов устройств, а во втором разрабатывается система динамического анализа модулей ядра (проект "KEDR").

Технологии статического анализа исходного кода и динамического анализа поведения программ имеют свои достоинства и недостатки и успешно дополняют друг друга. Их основные отличия приведены в следующей таблице:

N Статический анализ Динамический анализ
1 Исходный код модуля анализируется без его исполнения. Данные необходимые для анализа собираются во время исполнения кода модуля. Сам анализ может быть проведен как во время работы целевого модуля (анализ времени выполнения), так и после него (анализ постфактум или "postmortem").
2 (Следует из предыдущего) Не требуется специальной аппаратуры или программного обеспечения для анализируемого модуля ядра. (Следует из предыдущего) Если анализируемый модуль требует специальной аппаратуры или программного обеспечения, его следует предоставить или эмулировать. Может быть проблематично сделать это, если, например, необходимо проанализировать драйвер для редкой сетевой карты. Тем не менее, обычно это не так важно для разработчиков драйверов (вероятно, у них в любом случае есть доступ к необходимому оборудованию) или для систем сертификации для больших вендоров, таких как Microsoft, SUSE/Novell, Red Hat, Google, Canonical (они обычно требуют представлять все необходимое программное обеспечение и аппаратуру).
3 Нетривиальный статический анализ обычно требует значительных ресурсов (время, вычислительная мощность) для проведения. Это сильно зависит от сложности проводимого анализа. Затраты и количество ресурсов, необходимое для динамического анализа могут меняться в зависимости от сложности анализа и количества собираемых данных. В общем, ни статический, ни динамический анализ не является лучшим во всех случаях относительно требуемых ресурсов, но часто динамический анализ требует меньше ресурсов.
4 Обычно требуется исходный код анализируемого модуля (хотя статический анализ может быть проведен на основе бинарного кода, сделать это несколько сложнее и такой подход редко применяется для модулей ядра). Исходный код анализируемых модулей обычно не требуется. Это позволяет анализировать модули ядра с закрытым исходным кодом (хотя таких и не много в Linux), модули, собранные для разных экзотических конфигураций, и т.д.
5 Инструменты статического анализа для разработчиков модулей ядра (модель использования).

- "Легковесные" инструменты статического анализа (такие как Sparse и Coccinelle на Linux или PREfast на MS Windows) могут быть использованы разработчиками с самых ранних стадий работы над модулями ядра. Инструменты могут использоваться на компьютерах разработчиков и часто могут быть включены большую часть времени.

- "Тяжеловесные" инструменты (такие как LDV на Linux или Static Driver Verifier на MS Windows), выполняющие более сложный статический анализ, вероятно, стоит использовать, когда большая часть функциональности модуля уже присутствует. Подобные инструменты иногда могут использоваться на машинах разработчиков, но более вероятно их использование на специализированных серверах. Время от времени разработчики загружают туда свой код и затем получают результаты.

 Инструменты динамического анализа для разработчиков модуле ядра (модель использования).

Инструменты динамического анализа могут быть использованы разработчиками модулей ядра на своих компьютерах, как только разрабатываемые модули можно будет запустить и выполнить с ними какие-то операции. Если модули работают с каким-либо специальным программным обеспечением или оборудованием, может быть сложно развернуть инструменты динамического анализа на внешних серверах, для которых такое оборудование недоступно.

Такие инструменты, как Driver Verifier на MS Windows или KEDR на Linux могут быть использованы на пользовательских компьютерах, чтобы помочь собрать данные о возможных ошибках в модулях ядра. Существует множество конфигураций пользовательских систем и не всегда возможно воспроизвести все эти конфигурации при разработке. Может быть полезно собрать требуемые данные на пользовательских компьютерах напрямую, используя инструменты динамического анализа и посылать собранные данные разработчикам для дальнейшего анализа.

Другой областью, где могут применяться инструменты динамического анализа, является разработка свободных аналогов существующих проприетарных модулей (так Mmiotrace используется для разработки драйверов графики Nouveau для видеокарт NVidia).
6 Инструменты статического анализа для систем сертификации модулей ядра (модель использования).
Инструменты статического анализа могут использоваться в системах сертификации, но до сих пор не были обязательными (так Static Driver Verifier используется на MS Windows). Вероятно, это связано с возможностью ложных срабатываний (false positives).

Модель использования может быть следующая. Система анализа устанавливается на сервере. Используя службы, предоставляемые этим сервером, можно загрузить исходный код модуля для анализа и затем получить результаты.

 Инструменты динамического анализа для систем сертификации модулей ядра (модель использования).
Инструменты динамического анализа могут быть использованы в системах сертификации. Подобные инструменты обычно дают меньше ложных срабатываний, чем системы статического анализа, так что если они зафиксируют ошибки в анализируемых модулях, можно считать это основанием для отказа сертификации. Так Driver Verifier используется на MS Windows (Windows Logo Program) и механизмы Novell "API Swapping" на Linux (Novell YES Certified Program).

Модель использования может быть следующей. Система сертификации загружает инструменты динамического анализа и анализируемый модуль и затем запускает ряд тестов для этого модуля. Инструменты следят за работой модуля (a также могут на неё влиять) и выявляют ошибки в этом модуле.
7 Многие (или даже все) пути исполнения в коде могут быть проверены одновременно. Только один путь исполнения может быть проверен в данный момент времени.
8 (Следует из предыдущего) При достаточном времени и вычислительной мощности большинство или даже все ошибки могут быть выявлены. Важный вопрос состоит в том, насколько много времени и ресурсов необходимо для каждого конкретного случая. (Следует из предыдущего) Только ошибки, которые встречаются в фактически исполняемом пути, могут быть выявлены.
9 Более удобен, когда недостаточно проанализировать относительно много коротоких путей в коде (длина может быть ограничена "комбинаторным взрывом" или подобными проблемами). Более удобен, когда необходимо проанализировать пути исполнения в коде от начала до конца.
10 Иногда выгодно использовать инструменты статического анализа, чтобы зафиксировать отсутствующую обработку ошибок. Типичный пример - это ситуация, когда не проверено, завершилась ли функция успешно: вернула ли функция выделения памяти NULL или нет, и т.д. Инструменты динамического анализа обычно не имеют существенных преимуществ в детектировании отсутствующей обработки ошибок по сравнению со статическим анализом.
Что касается поиска проблем при обработке ошибок (use-after-free, и т.д.), здесь нельзя сказать, что какой-то из подходов строго лучше, чем другой. Всё сильно зависит от того, насколько длинный путь в коде должен быть проанализирован, чтобы обнаружить проблему.
11 Инструменты статического анализа отлично приспособлены для обнаружения использования некоторых операций в ситуациях, когда это запрещено. Пример: использование функции, которая может ожидать (или может вызвать reschedule ещё каким-то способом) в атомарном контексте, то есть, в обработчиках прерываний, в критических секциях, защищенных spinlock'ами, и тому подобным. Инструменты динамического анализа предоставляют крайне мало преимуществ при при обнаружении использования операций при некорректных условиях. Дело в том, что такие инструменты могут обнаруживать ошибки подобного рода только непосредственно перед или даже после совершения операции.
12 Инструменты и статического, и динамического анализа сейчас используются для обнаружения таких ошибок, как состояние гонки ("race conditions"), некорректные операции доступа к памяти, утечки ресурсов.
13 Инструменты статического анализа не требуют, чтобы код анализируемый модуль выполнялся. Таким образом, может быть безопаснее использовать статический анализ, если известно, что анализируемый модуль может, к примеру, серьезно повредить систему, если что-то пойдет не так. Динамический анализ в некоторых случаях менее безопасен, чем статический анализ, потому что ошибки в работающем модуле могут иметь непредсказуемые последствия.
14 Во многих случаях при использовании статического анализа модулей ядра ложные срабатывания более вероятны, чем при использовании динамического анализа (и иногда количество ложных срабатываний может быть слишлом большим). Причины для этого следующие:

- Чтобы провести статический анализ модуля ядра, необходима модель среды, в которой исполняется анализируемый модуль. Модель обычно не является абсолютно точной, в конце концов, это же модель.

- Если анализируется конкретный модуль, то необходимы модели модулей, с которыми он взаимодействует, а также модели ядра - и они обычно также не точны.

 Как правило, инструменты динамического анализа дают меньше ложных срабатываний, чем инструменты статического анализа (нередко ложных срабатываний нет совсем).

Тем не менее, инструменты динамического анализа могут давать ложные срабатыванияю Например, средства для поиска ошибок, связанных с многопоточностью (race conditions, ...) нередко дают ложные срабатывания, когда анализируемая система использует нестандартные механизмы синхронизации.