Синтез и проверка драйверов устройств

Архитектура драйвера устройства. — *Драйвер устройства* .

Драйверы устройств — это программы, которые позволяют программному обеспечению более высокого уровня или компьютерным программам взаимодействовать с аппаратным устройством. Эти программные компоненты действуют как связующее звено между устройствами и операционными системами , взаимодействуя с каждой из этих систем и выполняя команды. Они обеспечивают уровень абстракции для вышеуказанного программного обеспечения, а также опосредуют связь между ядром операционной системы и устройствами ниже.

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

Мотивация автоматического синтеза и проверки драйверов

Драйверы устройств являются основным неисправным компонентом в большинстве систем. Проект открытой инфраструктуры для сетевых вычислений Беркли (BOINC) обнаружил, что сбои ОС в основном вызваны плохо написанным кодом драйвера устройства. ^[1] В Windows XP на долю драйверов приходится 85% зарегистрированных сбоев. В ядре Linux 2.4.1 код драйвера устройства занимает около 70% размера кода. ^[2] Ошибка драйвера может привести к сбою всей системы, поскольку она работает в режиме ядра . Эти результаты привели к появлению различных методологий и методов проверки драйверов устройств. Альтернативой была разработка методов, позволяющих надежно синтезировать драйверы устройств. Меньшее участие человека в процессе разработки и правильная спецификация устройства и операционных систем могут привести к созданию более надежных драйверов.

Другой мотивацией для синтеза драйверов является большое количество разновидностей операционных систем и комбинаций устройств. Каждый из них имеет свой собственный набор средств управления вводом/выводом и спецификации , что затрудняет поддержку аппаратных устройств в каждой из операционных систем. Таким образом, возможность использования устройства с операционной системой требует наличия соответствующей комбинации драйверов устройств. Поставщики оборудования обычно поставляют драйверы для Windows, Linux и Mac OS, но из-за высоких затрат на разработку или перенос, а также трудностей технической поддержки они не могут предоставить драйверы для всех платформ. Метод автоматического синтеза может помочь поставщикам предоставить драйверы для поддержки любых устройств в любой операционной системе.

Проверка драйверов устройств

Есть две проблемы, которые ограничивают тестирование драйверов устройств.

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

Волна проверки драйверов устройств была инициирована Microsoft в рамках проекта SLAM еще в 2000 году. Мотивацией проекта было то, что 500 000 сбоев, о которых сообщалось в день, были вызваны одним видеодрайвером, что вызвало обеспокоенность по поводу огромного уязвимость при использовании сложных драйверов устройств. Более подробную информацию можно найти здесь , в речи Билла Гейтса. С тех пор было предложено большое количество статических и динамических методов для обнаружения и изоляции ошибок.

Статический анализ

Статический анализ означает анализ программы, чтобы проверить, соответствует ли она заданным критическим для безопасности свойствам. Например, системное программное обеспечение должно соответствовать таким правилам, как «проверять права пользователя перед записью в структуры данных ядра», «не ссылаться на нулевой указатель без проверки», «запретить переполнение размера буфера» и т. д. Такие проверки могут выполняться без фактического выполнение проверяемого кода. Использование традиционного процесса тестирования (динамическое выполнение) требует написания множества тестовых примеров для проверки этих путей и перевода системы в состояния ошибок. Этот процесс может занять много времени и усилий и не является практическим решением. Другой теоретически возможный подход — проверка вручную, но это непрактично в современных системах, в которых задействованы миллионы строк кода, что делает логику слишком сложной для анализа человеком.

Методы компиляции

Правила, которые напрямую сопоставляются с исходным кодом, можно проверить с помощью компилятора. Нарушения правил можно обнаружить, проверив, не имеет ли исходная операция смысла. Например, такие правила, как «включение прерывания после его отключения», можно проверить, просмотрев порядок вызовов функций. Но если система типов исходного кода не может указать правила в своей семантике, то компиляторы не смогут отловить ошибки такого рода. Многие типобезопасные языки позволяют безопасности памяти компилятору обнаруживать нарушения , возникающие в результате небезопасного приведения типов.

Другой подход — использовать компиляцию метауровня (MC) . ^[3] Метакомпиляторы, созданные для этой цели, могут дополнять компиляторы облегченными, специфичными для системы средствами проверки и оптимизаторами. Эти расширения должны быть написаны разработчиками системы на языке высокого уровня и динамически связаны с компиляторами для проведения строгого статического анализа.

Проверка модели программного обеспечения

Проверка модели программного обеспечения — это алгоритмический анализ программ для проверки свойств их выполнения. ^[4] Это автоматизирует рассуждения о поведении программы относительно заданных правильных спецификаций. Проверка модели и символическое выполнение используются для проверки критически важных для безопасности свойств драйверов устройств. Входными данными для средства проверки модели являются программа и свойства временной безопасности. Результатом является доказательство корректности программы или демонстрация нарушения спецификации с помощью контрпримера в виде конкретного пути выполнения.

Инструмент SDV (статическая проверка драйверов) ^[5] от Microsoft использует статический анализ драйверов устройств Windows. Механизм внутреннего анализа SLAM использовал проверку модели и символьное выполнение для статической проверки во время компиляции. Правила, которые должны соблюдаться драйверами для каждого API, указаны на C-подобном языке SLIC (язык спецификаций для проверки интерфейса). Механизм анализа находит все пути, которые могут привести к нарушениям правил использования API, и представляются в виде путей ошибок на уровне исходного кода через исходный код драйвера. Внутри он абстрагирует код C в логическую программу и набор предикатов, которые представляют собой правила, которые должны соблюдаться в этой программе. Затем он использует символическую проверку модели ^[6] для проверки предикатов в логической программе.

Средство проверки моделей BLAST (инструмент проверки программного обеспечения Berkeley Lazy Abstraction) ^[7] используется для обнаружения ошибок безопасности памяти и неправильных блокировок в коде ядра Linux. Он использует алгоритм абстракции, называемый ленивой абстракцией. ^[8] построить модель из кода драйвера C. Он успешно проверил свойства временной безопасности программ на языке C, содержащих до 50 тысяч строк кода. Он также используется для определения того, влияет ли изменение в исходном коде на подтверждение собственности в предыдущей версии и демонстрируется ли он в драйвере устройства Windows.

Авинукс ^[9] — это еще один инструмент, который облегчает автоматический анализ дисков устройств Linux и построен на основе средства проверки ограниченных моделей CBMC. ^[10] Существуют методы локализации неисправности, позволяющие найти место ошибки, поскольку эти инструменты проверки модели возвращают длинную трассировку примера счетчика, и трудно найти точное место неисправности. ^[11]

Анализ времени выполнения

Динамический анализ программы выполняется путем запуска программы с достаточным количеством тестовых входных данных для получения интересного поведения. Безопасное вождение ^[12] — это система с низкими издержками для обнаружения и устранения нарушений типовой безопасности в драйверах устройств. Внеся всего лишь 4% изменений в исходный код сетевых драйверов Linux, они смогли реализовать SafeDrive и обеспечить лучшую защиту и восстановление ядра Linux. Аналогичный проект, использующий аппаратное обеспечение для изоляции драйверов устройств от основного ядра, — Nook. ^[13] Они помещают драйверы устройств в отдельный домен аппаратной защиты, называемый «nooks», и имеют отдельные настройки разрешений для каждой страницы, гарантируя, что драйвер не изменяет страницы, которые не находятся в его домене, но может читать все данные ядра, поскольку они используют одно и то же адресное пространство. .

Еще одна подобная работа в этой области – автоматическое восстановление операционных систем из-за сбоев драйверов. МИНИКС 3 ^[14] — это операционная система, которая может изолировать серьезные неисправности, обнаруживать дефекты и заменять вышедшие из строя компоненты на лету.

Синтез драйверов устройств

Альтернативой проверке и изоляции ошибок является внедрение методов в процесс разработки драйверов устройств, чтобы сделать его более надежным. Учитывая спецификацию устройства и функции операционной системы, одним из методов является синтез драйвера устройства для этого устройства. Это помогает уменьшить количество ошибок, вносимых человеком, а также затраты и время, затрачиваемые на разработку системного программного обеспечения. Все методы синтеза основаны на той или иной форме спецификаций производителей аппаратных устройств и функций операционной системы.

Языки спецификации интерфейса

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

Дьявол ^[15] обеспечивает высокий уровень определения связи с устройством. Аппаратные компоненты выражаются в виде портов ввода-вывода и регистров, отображаемых в памяти. Эти спецификации затем преобразуются в набор макросов C, которые можно вызывать из кода драйвера и, таким образом, устранять ошибки, вызванные программистом при написании функций низкого уровня. НДЛ ^[16] является усовершенствованием Devil, описывающим драйвер с точки зрения его рабочего интерфейса. Он использует синтаксис определения интерфейса Devil и включает в себя набор определений регистров, протоколы доступа к этим регистрам и набор функций устройства. Функции устройства затем преобразуются в серию операций на этом интерфейсе. Для создания драйвера устройства необходимо сначала написать функции драйвера на этих языках спецификации интерфейса, а затем использовать компилятор, который сгенерирует код драйвера низкого уровня.

HAIL (язык интерфейса аппаратного доступа) ^[17] — это еще один язык спецификации драйверов устройств, специфичный для конкретной области. Разработчику драйвера необходимо написать следующее.

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

Компилятор HAIL принимает эти входные данные и переводит спецификацию в код C.

Аппаратное обеспечение Программное обеспечение Совместное проектирование

При совместном проектировании аппаратного и программного обеспечения разработчик определяет структуру и поведение системы, используя конечные автоматы, которые взаимодействуют между собой. Затем на этих конечных автоматах выполняется серия испытаний, моделирования и формальной проверки, прежде чем решить, какие компоненты войдут в аппаратное обеспечение, а какие в программное обеспечение. Аппаратное обеспечение обычно выполняется в виде программируемых вентильных матриц (FPGA) или специализированных интегральных схем (ASIC), тогда как программная часть переводится на язык программирования низкого уровня. Этот подход в основном применяется во встроенных системах, которые определяются как набор программируемых частей, которые постоянно взаимодействуют с окружающей средой через датчики. Существующие методы ^[18] предназначены для создания простых микроконтроллеров и их драйверов.

Автономный синтез драйверов

При автономном синтезе устройство и системное программное обеспечение выполняются отдельно. Устройство моделируется с использованием любого языка описания оборудования (HDL), и разработчик программного обеспечения не имеет доступа к спецификациям HDL. Разработчики оборудования изложили интерфейс устройства в паспорте устройства. Из таблицы данных разработчик драйвера извлекает структуру регистров и памяти устройства, а также поведенческую модель в виде конечных автоматов. Это выражается в доменных языках, описанных в разделе «Язык интерфейса». Последний шаг включает генерацию кода на основе этих спецификаций.

Инструмент Термит ^[19] для создания драйвера требуются три спецификации.

Спецификация устройства. Спецификация регистра устройства, памяти и служб прерываний, полученная из таблицы данных устройства.
Спецификация класса устройства: ее можно получить из соответствующего стандарта протокола ввода-вывода устройства. Например, для Ethernet стандарт Ethernet LAN описывает общее поведение этих контроллеров. Обычно это кодируется как набор событий, таких как передача пакета, завершение автосогласования, изменение статуса канала и т. д.
Спецификация ОС: описывает интерфейс ОС с драйвером. Точнее, запросы, которые ОС может направить драйверу, порядок этих запросов и то, что ОС ожидает от драйвера в ответ на эти запросы. Он определяет конечный автомат, где каждый переход соответствует вызову драйвера ОС, обратному вызову, выполняемому драйвером, или событию, указанному протоколом.

Учитывая эти спецификации, Termite сгенерирует реализацию драйвера, которая преобразует любую допустимую последовательность запросов ОС в последовательность команд устройства. Благодаря формальной спецификации интерфейсов Termite может генерировать код драйвера, который обладает свойствами безопасности и живучести .

Еще одна очень интересная попытка взлома была предпринята RevNIC. ^[20] который генерирует конечный автомат драйвера путем обратного проектирования существующего драйвера для создания совместимых и безопасных драйверов для новых платформ. Чтобы выполнить реверс-инжиниринг драйвера, он перехватывает аппаратные операции ввода-вывода, выполняя драйвер с использованием символьных и конкретных исполнений. Выходные данные прослушивания передаются на синтезатор, который восстанавливает граф потока управления исходного драйвера на основе этих многочисленных трасс вместе с шаблонным шаблоном для соответствующего класса устройств. Используя эти методы, исследователи портировали некоторые драйверы сетевых интерфейсов Windows на другие Linux и встраиваемые операционные системы.

Критика

Хотя многие инструменты статического анализа широко используются, многие инструменты синтеза и проверки драйверов не получили широкого распространения на практике. Одна из причин заключается в том, что драйверы, как правило, поддерживают несколько устройств, и в процессе синтеза драйверов обычно создается один драйвер для каждого поддерживаемого устройства, что потенциально может привести к созданию большого количества драйверов. Другая причина заключается в том, что драйверы также выполняют некоторую обработку, а модель конечного автомата драйверов не может отображать обработку. ^[21]

Заключение

Различные методы проверки и синтеза, рассмотренные в этой статье, имеют свои преимущества и недостатки. Например, изоляция ошибок во время выполнения приводит к снижению производительности, тогда как статический анализ не охватывает все классы ошибок. Полная автоматизация синтеза драйверов устройств все еще находится на ранней стадии и имеет многообещающее направление будущих исследований. Прогресс будет облегчен, если многие языки, доступные сегодня для спецификации интерфейсов, смогут в конечном итоге объединиться в единый формат, который будет повсеместно поддерживаться поставщиками устройств и командами операционных систем. Результатом таких усилий по стандартизации может стать реализация полностью автоматизированного синтеза надежных драйверов устройств в будущем.

Ссылки

^ Арчана Ганапати, Виджи Ганапати и Дэвид Паттерсон. « Анализ сбоя ядра Windows XP ». В материалах конференции по администрированию больших инсталляционных систем 2006 г., 2006 г.
^ А. Чоу, Дж. Ян, Б. Челф, С. Халлем и Д. Энглер. Эмпирическое исследование ошибок операционных систем. В СОСП, 2001 г.
^ Энглер, Доусон и Челф, Бенджамин и Чоу, Энди и Халлем, Сет. « Проверка системных правил с использованием специфичных для системы расширений компилятора, написанных программистом ». В материалах 4-й конференции симпозиума по проектированию и внедрению операционных систем, 2000 г.
^ Джала, Ранджит и Маджумдар, Рупак. «Проверка модели программного обеспечения». В обзоре вычислений ACM. 2009 год
^ Томас Болл, Элла Бунимова, Байрон Кук, Владимир Левин, Якоб Лихтенберг, Кон МакГарви, Бохус Ондрусек, Шрирам Раджамани. и Абдулла Устунер. « Тщательный статический анализ драйверов устройств », в SIGOPS Oper. Сист. Преподобный, Том. 40, 2006.
^ Макмиллан, Кеннет Л. «Проверка символической модели». Академическое издательство Клувер, 1993.
^ Томас А. Хензингер, Ранджит Джала, Рупак Маджумдар и Грегуар Сутре. « Верификация программного обеспечения с помощью BLAST ». В СПИН, 2003.
^ Томас А. Хенцингер, Ранджит Джала, Рупак Маджумдар и Грегуар Сутре. «Ленивая абстракция», на конференции ACM SIGPLAN-SIGACT по принципам языков программирования, 2002 г.
^ Х. Пост, В. Кюхлин. «Интеграция статического анализа для проверки драйверов устройств Linux». В 6-м международном. Конф. по интегрированным формальным методам, 2007.
^ Эдмунд Кларк, Дэниел Крёнинг и Флавио Лерда. «Инструмент для проверки программ ANSI-C». В ТАКАС, 2004 г.
^ Томас Болл, Маюр Наик и Шрирам К. Раджамани. «От симптома к причине: локализация ошибок в следах контрпримеров». Уведомления ACM SIGPLAN, 2003 г.
^ Фэн Чжоу, Джереми Кондит, Закари Андерсон, Илья Баграк, Роб Энналс, Мэтью Харрен, Джордж Некула и Эрик Брюэр. « SafeDrive: безопасные и восстанавливаемые расширения с использованием языковых методов ». В 7-м OSDI, 2006 г.
^ Майкл М. Свифт, Стивен Мартин, Генри М. Леви и Сьюзен Дж. Эггерс. « Nooks: архитектура для надежных драйверов устройств ». В 10-м ACM SIGOPS, 2002 г.
^ Йоррит Н. Гердер, Герберт Бос, Бен Грас, Филип Хомбург и Эндрю С. Таненбаум. « MINIX 3: высоконадежная самовосстанавливающаяся операционная система ». В СИГОПС Опер. Сист. Ред. 40, 2006 г.
^ Фабрис Мерийон, Лоран Ревейер, Шарль Консель, Рено Марле и Жиль Мюллер. « Дьявол: IDL для аппаратного программирования ». В материалах 4-й конференции симпозиума по проектированию и внедрению операционных систем, Vol. 4, 2000.
^ Кристофер Л. Конвей и Стивен А. Эдвардс. « NDL: предметно-ориентированный язык для драйверов устройств ». Уведомления ACM SIGPLAN 39, 2004 г.
^ Дж. Сунь, В. Юань, М. Каллахалла и Н. Ислам. « HAIL: язык для простого и правильного доступа к устройствам ». В Proc. конференции ACM по встраиваемому программному обеспечению, 2005 г.
^ Феличе Баларин и др. « Совместное аппаратно-программное проектирование встраиваемых систем. Подход ПОЛИС ». Издательство Kluwer Academic, 1997.
^ Леонид Рыжик, Питер Чубб, Игорь Куз, Этьен Ле Сюёр и Гернот Хейзер. «Автоматический синтез драйверов устройств с помощью Termite». В материалах 22-го симпозиума ACM по принципам операционных систем, 2009 г.
^ Виталий Чипунов и Джордж Кандеа. « Реверс-инжиниринг двоичных драйверов устройств с помощью RevNIC ». 5-я конференция ACM SIGOPS/EuroSys, 2010 г.
^ Асим Кадав и Майкл М. Свифт «Понимание современных драйверов устройств» в материалах 17-й конференции ACM по архитектурной поддержке языков программирования и операционных систем.

Внешние ссылки

[1] Арчана Ганапати, Виджи Ганапати и Дэвид Паттерсон. « Анализ сбоя ядра Windows XP ». В материалах конференции по администрированию больших инсталляционных систем 2006 г., 2006 г.

[2] А. Чоу, Дж. Ян, Б. Челф, С. Халлем и Д. Энглер. Эмпирическое исследование ошибок операционных систем. В СОСП, 2001 г.

[3] Энглер, Доусон и Челф, Бенджамин и Чоу, Энди и Халлем, Сет. « Проверка системных правил с использованием специфичных для системы расширений компилятора, написанных программистом ». В материалах 4-й конференции симпозиума по проектированию и внедрению операционных систем, 2000 г.

[4] Джала, Ранджит и Маджумдар, Рупак. «Проверка модели программного обеспечения». В обзоре вычислений ACM. 2009 год

[5] Томас Болл, Элла Бунимова, Байрон Кук, Владимир Левин, Якоб Лихтенберг, Кон МакГарви, Бохус Ондрусек, Шрирам Раджамани. и Абдулла Устунер. « Тщательный статический анализ драйверов устройств », в SIGOPS Oper. Сист. Преподобный, Том. 40, 2006.

[6] Макмиллан, Кеннет Л. «Проверка символической модели». Академическое издательство Клувер, 1993.

[7] Томас А. Хензингер, Ранджит Джала, Рупак Маджумдар и Грегуар Сутре. « Верификация программного обеспечения с помощью BLAST ». В СПИН, 2003.

[8] Томас А. Хенцингер, Ранджит Джала, Рупак Маджумдар и Грегуар Сутре. «Ленивая абстракция», на конференции ACM SIGPLAN-SIGACT по принципам языков программирования, 2002 г.

[9] Х. Пост, В. Кюхлин. «Интеграция статического анализа для проверки драйверов устройств Linux». В 6-м международном. Конф. по интегрированным формальным методам, 2007.

[10] Эдмунд Кларк, Дэниел Крёнинг и Флавио Лерда. «Инструмент для проверки программ ANSI-C». В ТАКАС, 2004 г.

[11] Томас Болл, Маюр Наик и Шрирам К. Раджамани. «От симптома к причине: локализация ошибок в следах контрпримеров». Уведомления ACM SIGPLAN, 2003 г.

[12] Фэн Чжоу, Джереми Кондит, Закари Андерсон, Илья Баграк, Роб Энналс, Мэтью Харрен, Джордж Некула и Эрик Брюэр. « SafeDrive: безопасные и восстанавливаемые расширения с использованием языковых методов ». В 7-м OSDI, 2006 г.

[13] Майкл М. Свифт, Стивен Мартин, Генри М. Леви и Сьюзен Дж. Эггерс. « Nooks: архитектура для надежных драйверов устройств ». В 10-м ACM SIGOPS, 2002 г.

[14] Йоррит Н. Гердер, Герберт Бос, Бен Грас, Филип Хомбург и Эндрю С. Таненбаум. « MINIX 3: высоконадежная самовосстанавливающаяся операционная система ». В СИГОПС Опер. Сист. Ред. 40, 2006 г.

[15] Фабрис Мерийон, Лоран Ревейер, Шарль Консель, Рено Марле и Жиль Мюллер. « Дьявол: IDL для аппаратного программирования ». В материалах 4-й конференции симпозиума по проектированию и внедрению операционных систем, Vol. 4, 2000.

[16] Кристофер Л. Конвей и Стивен А. Эдвардс. « NDL: предметно-ориентированный язык для драйверов устройств ». Уведомления ACM SIGPLAN 39, 2004 г.

[17] Дж. Сунь, В. Юань, М. Каллахалла и Н. Ислам. « HAIL: язык для простого и правильного доступа к устройствам ». В Proc. конференции ACM по встраиваемому программному обеспечению, 2005 г.

[18] Феличе Баларин и др. « Совместное аппаратно-программное проектирование встраиваемых систем. Подход ПОЛИС ». Издательство Kluwer Academic, 1997.

[19] Леонид Рыжик, Питер Чубб, Игорь Куз, Этьен Ле Сюёр и Гернот Хейзер. «Автоматический синтез драйверов устройств с помощью Termite». В материалах 22-го симпозиума ACM по принципам операционных систем, 2009 г.

[20] Виталий Чипунов и Джордж Кандеа. « Реверс-инжиниринг двоичных драйверов устройств с помощью RevNIC ». 5-я конференция ACM SIGOPS/EuroSys, 2010 г.

[21] Асим Кадав и Майкл М. Свифт «Понимание современных драйверов устройств» в материалах 17-й конференции ACM по архитектурной поддержке языков программирования и операционных систем.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[18]

[19]

[20]

[21]