БЕЗОПАСНОСТЬ И ЗАЩИТА -
УДК 004.45
МОДЕЛИРОВАНИЕ ОКРУЖЕНИЯ С ИСПОЛЬЗОВАНИЕМ ШАБЛОНОВ ДЛЯ СТАТИЧЕСКОЙ ВЕРИФИКАЦИИ МОДУЛЕЙ ЯДРА LINUX *
© 2015 г. И. С. Захаров, В. С. Мутилин, А. В. Хороши л ов
Институт системного программирования РАН
109004 Москва, ул. А. Солженицына, 25 E-mail: ilja.zakharov@ispras.ru, mutilin@ispras.ru, khoroshilov@ispras. ru Поступила в редакцию 13.12.2014
Модули ядра Linux функционируют в окружении, управляемом событиями. При статической верификации таких модулей необходимо учитывать все возможные сценарии взаимодействия между модулями и их окружением. Данная работа предлагает новый метод моделирования окружения, позволяющий автоматически генерировать модели окружения для заданного модуля ядра на основе анализа исходного кода модуля и набора спецификаций, описывающих шаблоны сценариев взаимодействий между модулями и их окружением. В спецификациях могут быть заданы как шаблоны сценариев для всего ядра Linux, так и детальные, которые характерны для определенной подсистемы. Это позволяет значительно сократить размер спецификации и позволяет верифицировать больше модулей с меньшими усилиями. Предложенный метод реализован в компоненте инструментария LDV Tools, который применяется для статической верификации модулей практически всех подсистем ядра Linux.
1. ВВЕДЕНИЕ
Ядро Linux лежит в основе разных операционных систем. Упомянутые операционные системы требуют от ядра поддержки разной функциональности в зависимости от области применения и используемой аппаратуры. Обычно ядро предоставляет лишь набор наиболее востребованных функций, таких, как управление памятью и процессами. Для того чтобы расширить функциональность ядра, можно воспользоваться динамически загружаемыми модулями, реализующими недостающие функции.
Ядро уже поставляется с большим набором модулей, включающих драйверы для различных
* Исследование проводилось при финансовой поддержке Министерства образования и науки Российской федерации (уникальный идентификатор проекта — RFMEFI60414X0051).
устройств и файловых систем, реализации сетевых протоколов и др. Наборы доступных для динамической загрузки модулей различаются в зависимости от архитектуры системы и конфигурации ядра. Например, последняя версия ядра Linux на момент написания статьи включала четыре тысячи модулей для архитектуры х86_64 в конфигурации allmodconf ig.
Модули ядра работают в том же адресном пространстве и с тем же уровнем привилегий, что и остальное ядро. Но, по некоторым причинам, уровень качества модулей в сравнении с собственно ядром существенно ниже [1]. Около половины всех нефункциональных ошибок в модулях ядра Linux составляют случаи, связанные с некорректным использованием модулями интерфейсов ядра [2]. Данная работа рассматривает ошибки этого типа и предлагает применять статическую верификацию для борьбы с ними. Эта техника позволяет анализировать все воз-
можные пути выполнения программы на предмет содержания ошибок, в том числе сложно воспроизводимые.
Современные инструменты статической верификации [3, 4, 5, 6, 7] уже позволяют проверять средние по размеру программы. Поэтому они применимы для поиска ошибок в модулях ядра Linux, так как последние как раз имеют размер порядка нескольких тысяч строк кода. Но, с одной стороны, основная функциональность модулей ядра Linux заключается в предоставлении средств обработки различных событий, например, возникающих как следствие прерываний от аппаратуры или системных вызовов от пользовательских программ, из-за чего пути выполнения исходного кода модуля в большой степени зависят от его окружения. С другой стороны, существующими инструментами статической верификации модули не могут быть проанализированы вместе с остальным ядром из-за слишком большого объема и сложности исходного кода подобной системы. Для того чтобы проверять модули ядра отдельно, требуется подменить недостающий код на модельное окружение, позволяющее при верификации порождать пути выполнения, которые могут произойти при работе модуля в реальном окружении. В работе [8] было показано, что для применения инструментов статической верификации требуется достаточно точная модель окружения. В противном случае инструменты генерируют большое число ложных сообщений об ошибках, допуская при верификации невозможные в реальности пути выполнения программы. Кроме того, модели окружения не должны упускать сценариев допустимых взаимодействий между модулями и их окружением, которые могут иметь место при реальном выполнении. Иначе это может привести к пропуску ошибок.
При моделировании окружения важно учитывать темпы развития ядра Linux, так как новые версии ядра появляются несколько раз в год. В ядре постоянно появляется поддержка новых типов устройств, появляются новые подсистемы и удаляются устаревшие или неиспользуемые функции, кроме того, дорабатываются уже существующие части. Та часть ядра Linux, которая реализует поддержку взаимодействия ядра с модулями, и сами модули непосредственно ока-
зываются на переднем крае изменений, так как именно дополнительная функциональность, реализованная в модулях ядра, чаще всего оказывается предметом улучшений. Еще одним обстоятельством, затрудняющим разработку точных моделей окружения для модулей ядра, является многообразие различных интерфейсов и видов обработчиков, которые модули предоставляют ядру. Наш анализ исходного кода ядра Linux версии 3.17-гс1 и его модулей показал, что счет обработчиков идет на десятки тысяч, а их видов насчитываются сотни. Поэтому при описании модели окружения чрезвычайно важно сократить ручной труд и описания моделируемых интерфейсов ядра, привязанных к его определенной версии.
Основной вклад данной работы заключается в предлагаемом методе и его реализации в инструменте для моделирования окружения. Метод предоставляет средства для задания одновременно точной и допускающей переиспользование спецификации модели окружения. Спецификации предлагается задавать на упрощенном языке для задания шаблонов допустимых взаимодействий между модулями и их окружением, что позволяет существенно сократить работу по специфицированию окружения. Части спецификаций, зависящие от развивающегося интерфейса ядра Linux, отделены от шаблонов взаимодействий, чтобы сократить усилия на разработку и поддержку. Также финальное представление модели окружения генерируется на языке Си, чтобы позволять применять различные инструменты верификации.
Данная работа организована следующим образом. В разделе 2 мы рассматриваем типовые сценарии взаимодействия между модулями ядра Linux и их окружением. В разделе 3 изложен предлагаемый метод для моделирования окружения. Его реализация описана в разделе 4. Раздел 5 посвящен результатам экспериментов. Существующие подходы к моделированию окружения рассматриваются в разделе 6. В последнем разделе 7 подводятся итоги.
2. ОКРУЖЕНИЕ МОДУЛЕЙ ЯДРА LINUX
Окружение модулей ядра Linux схематично изображено на рис. 1. Для простоты здесь и далее мы предполагаем, что каждый модуль вза-
Рис. 1. Взаимодействие модулей ядра Linux с их окружением.
имодейетвует с пользовательскими программами и аппаратурой только через так называемую сердцевину ядра. Модули предоставляют сердцевине ядра функции -обработчики различных событий, возникающих, например, как следствие прерываний от аппаратуры или системных вызовов от пользовательских программ. Обработчики можно объединить в группы по типам, каждый тип включает обработчики для выполнения операций над соответствующим ресурсом, например, устройством определенного вида или структурой данных. Назначение каждого обработчика группы характеризуется его ролью. Типы групп и соответствующие роли обработчиков определяются в сердцевине, а модули реализуют группы обработчиков как экземпляры поддерживаемых типов. Примером тина группы обработчиков может служить набор операций с файловыми дескрипторами внутри ядра, такими как открытие, чтение, запись, закрытие файла. Другим примером типа группы обработчиков является набор функций но управлению электропитанием какого-либо устройства, роли здесь определяют подготовку при погружении устройства в сон и действия но пробуждении. Для взаимодействия с USB или PCI шинами также существуют определенные типы групп обработчиков. Так, модуль драйвера для управления портативным USB-модемом обязательно содержит группу обработчиков, предназначенную для управления USB интерфейсом, и непосредственно группы об-
работчиков для передачи данных через сеть.
В процессе работы ядра операционной системы каждый модуль регистрирует свои группы обработчиков в сердцевине ядра согласно типу каждой группы, обычно это происходит при помощи вызова функций из сердцевины. Работа модуля начинается сразу после того, как его загрузили в намять и вызвали его функцию инициализации, в которой и выполняется регистрация первых групп обработчиков. Регистрация подразумевает передачу в сердцевину ядра указателей на функции-обработчики группы модуля. Сердцевина ядра затем вызывает обработчики но указателям для обработки определенных событий. Многие события обрабатываются параллельно, поэтому и обработчики модуля могут также выполнятся параллельно друг с другом. Как только потребность в средствах обработки событий модулем пропадает, сердцевина вызывает функцию выхода модуля, в которой выполняется де-регистрация групп обработчиков, после чего модуль может быть выгружен из памяти.
Разные группы обработчиков модуля вызываются согласно определенному протоколу между модулем и его окружением, так как во время вызова обработчиков может происходить регистрация и дерегиетрация новых групп модуля, выделение и освобождение памяти, захват примитивов синхронизации и др. Так, например, группу обработчиков нельзя дерегистрировать, пока ее обработчики не освободят ранее выделенные ре-
1 static int usbpn_open(struct net_device *dev) { ... };
2 static int usbpn_close(struct net_device *dev) { ... };
3 static const struct net_device_ops usbpn_ops = {
4 ,ndo_open = usbpn_open,
5 ,ndo_stop = usbpn_close
6 >;
7 int usbpn_probe(struct usb_interface *intf, ...) {
8 struct net_device
Для дальнейшего прочтения статьи необходимо приобрести полный текст. Статьи высылаются в формате PDF на указанную при оплате почту. Время доставки составляет менее 10 минут. Стоимость одной статьи — 150 рублей.