Развитие метода контрактных спецификаций для верификации модулей ядра операционной системы LINUX тема диссертации и автореферата по ВАК РФ 05.13.11, кандидат наук Новиков, Евгений Михайлович

• Новиков, Евгений Михайлович
• кандидат наук
• 2013

Оглавление диссертации кандидат наук Новиков, Евгений Михайлович

СОДЕРЖАНИЕ

Введение

Глава 1. Обзор существующих методов контрактных спецификаций

1.1 Неформальные методы контрактных спецификаций

1.2 Формальные методы контрактных спецификаций

1.2.1 Контрактные спецификации для компиляторов и интерпретаторов

1.2.2 Контрактные спецификации при динамическом анализе

1.2.3 Контрактные спецификации при статическом анализе

1.2.4 Контрактные спецификации при верификации

1.2.4.1 Модель окружения для модулей ядра ОС Linux

1.2.4.2 Спецификации правил корректного использования программных интерфейсов

1.3 Выводы

Глава 2. Метод контрактных спецификаций

2.1 Анализ правил корректного использования программного интерфейса сердцевины ядра ОС Linux

2.2 Подход аспектно-ориентированного программирования для языка Си

2.2.1 Основные понятия АОП

2.2.2 Традиционные способы описания аспектов

2.2.3 Влияние особенностей языка программирования Си и процесса сборки Си-программ на реализацию АОП

2.2.4 Особенности практического применения реализации АОП для языка Си

2.2.5 Существующие реализации АОП для языка Си

2.2.5.1 AspeCt-oriented С

2.2.5.2 InterAspect

2.2.5.3 Specification Language for Interface Checking

2.2.5.4 Другие реализации АОП для языка Си

2.2.6 Выводы

2.3 Метод описания в виде контрактных спецификаций правил корректного использования программного интерфейса сердцевины ядра ОС Linux

2.3.1 Шаг 1. Разработка модели подсистем ядра

2.3.2 Шаг 2. Описание множества точек использования элементов программного интерфейса

2.3.3 Шаг 3. Привязка модельных функций к точкам использования элементов программного интерфейса

2.3.4 Шаг 4. Задание предусловий использования элементов программного интерфейса

2.3.6 Дополнения к заданию контрактных спецификаций

2.4 Метод автоматизированного инструментирования исходного кода модулей ядра ОС Linux на основе контрактных спецификаций

2.5 К вопросу о доверии к контрактным спецификациям

2.5.1 Идеальные и избыточные контрактные спецификации

2.5.2 Примеры избыточных контрактных спецификаций

2.5.3 Чрезмерная избыточность контрактных спецификаций

2.5.4 Избыточность контрактных спецификаций на практике

2.5.5 Корреляции контрактных спецификаций

2.6 Подход к автоматизированному анализу структуры программы на основе

высокоуровневых запросов по исходному коду

2.6.1 Существующие решения

2.6.1.1 Запросы по исходному коду на основе регулярных выражений

2.6.1.2 Запросы по исходному коду на основе формального представления программы

2.6.2 Использование реализации АОП для выполнения запросов по исходному коду программ

2.6.2.1 Получение фактических параметров макрофункций

2.6.2.2 Получение списка вызываемых функций, у которых тип одного из параметров является указателем

2.6.2.3 Получение списка функций, в которых изменяется глобальная переменная

2.7 Метод автоматизированной поддержки корректности и согласованности контрактных спецификаций в условиях изменения программного интерфейса

2.8 Подход к автоматизированному уточнению контрактных спецификаций в условиях неполноты модели окружения

2.9 Выводы

Глава 3. Реализация метода контрактных спецификаций

3.1 Aspect-Oriented С — аспектно-ориенгированное расширение языка программирования Си с поддержкой всех расширений компилятора GCC

3.2 С Instrumentation Framework — аспектный компоновщик

3.2.1 Этап 1. Аспектное препроцессирование

3.2.2 Этап 2. Подготовка исходного кода

3.2.3 Этап 3. Инструментирование макросов

3.2.4 Этап 4. Инструментирование

3.2.5 Этап 5. Компиляция

3.3 База контрактных спецификаций

3.4 Место разработанного инструментария в системе верификации LDV

3.5 Выполнение высокоуровневых запросов по исходному коду

3.6 Контроль корректности и согласованности контрактных спецификаций в условиях изменения программного интерфейса

3.6.1 Обеспечение синтаксической корректности контрактных спецификаций

3.6.2 Проверка синтаксической совместимости контрактных спецификаций с программным интерфейсом сердцевины ядра ОС Linux

3.6.3 Обеспечение семантической корректности контрактных спецификаций

3.7 Уточнение контрактных спецификаций в условиях неполноты модели окружения

Глава 4. Практические результаты

Заключение

Список использованных источников

Приложение А Каталог наиболее критичных правил корректного использования

программного интерфейса сердцевины ядра ОС Linux

Приложение Б Аспектно-ориентированное расширение языка программирования Си с поддержкой всех расширений компилятора GCC

Введение диссертации (часть автореферата) на тему «Развитие метода контрактных спецификаций для верификации модулей ядра операционной системы LINUX»

Введение

На сегодняшний день ядро операционной системы (ОС) Linux представляет собой одну из самых востребованных программных систем. Ядро ОС Linux используется повсеместно на большом количестве различных аппаратных платформ, начиная от встроенных систем и персональных компьютеров и заканчивая интернет-серверами и суперкомпьютерами [1-4]. За последние несколько лет популярность ядра ОС Linux значительно возросла за счет использования ядра в ОС для мобильных устройств (Android, Tizen, Firefox OS и др.).

Ядро ОС Linux является одной из самых больших и динамично развивающихся программных систем. Разработку ядра начал Линус Торвальдс в 1991 году [5]. Размер первой версии ядра ОС Linux 0.01 был около 10 тыс. строк кода. 17 декабря 2003 года было выпущено ядро версии 2.6.0, размер которого составил около 6 млн строк кода. Последняя на момент начала написания данной работы, стабильная версия ядра ОС Linux 3.8 была выпущена 18 февраля 2013 года. Ее размер составил более 16 млн строк кода. Менее, чем за десять лет, размер исходного кода ядра ОС Linux вырос более, чем в 2,5 раза. Процесс разработки ядра ОС Linux обладает уникальными особенностями. Начиная с версии ядра 2.6.24, выпущенной 24 января 2008 года, в подготовке всех новых версий ядра принимают участие более 1 000 разработчиков из 200 организаций, рассредоточенных по всему миру [6]. Каждая новая версия ядра ОС Linux включает около 9-12 тыс. изменений, что соответствует в среднем 5,4 изменениям в час.

По своей архитектуре ядро ОС Linux является монолитным. Сердцевина ядра состоит из подсистем управления процессами, памятью, и межпроцессорным взаимодействием, подсистем поддержки различных аппаратных платформ и т.д. [7, 8]. Сердцевина ядра допускает динамическую

загрузку модулей, что позволяет расширить набор ее функций [8, 9]. Схематично устройство ядра приведено на рисунке 1. В настоящее время в состав ядра ОС Linux входит более 3,7 тыс. модулей, из которых большая часть является драйверами устройств (около 75%). Помимо драйверов устройств к числу модулей ядра ОС Linux относятся реализации различных файловых систем, сетевых протоколов, аудиокодеков и т.д.

В рамках данной работы было проведено дополнительное исследование, которое показало, что для первого релиз-кандидата ядра версии 3.9 в конфигурации allmodconfig на аппаратной платформе х86_64 сердцевина состоит из 1 651 файла (написанных на языках программирования Си и ассемблер), которые содержат 1 054 022 строк кода. На модули приходится 8 918 Си-файлов, которые содержат 7 862 862 строк кода. Таким образом, всего из 10 569 файлов около 16% приходится на сердцевину и 84% — на модули, а из 8 916 884 строк кода — 12% на сердцевину и 88% на модули. Остальной код ядра

х

3

с

О О

о а И

в;

Сердцевина

Рисунок 1. Схема устройства ядра ОС Linux.

либо относится к другим архитектурам и/или конфигурациям, либо представляет собой заголовочные файлы. Всего в первый релиз-кандидат ядра версии 3.9 вошло 22 061 заголовочный файл, размер которых составил 2 958 407 строк кода.

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

Ядро ОС Linux является свободным программным обеспечением. Одним из достоинств этого является то, что доступ к его коду имеют большое количество разработчиков и огромное количество пользователей основанных на нем ОС. Это создает так называемый эффект многих глаз — большое количество ошибок обнаруживается и исправляется за достаточно короткое время [10]. Таким образом могут быть обнаружены не все ошибки, так как во всем мире достаточным уровнем знания во всех особенностях устройства ядра обладают небольшое количество людей, а ядро имеет достаточно большой размер и развивается высокими темпами [11].

Исследования показали, что более 85% ошибок в исходном коде ядра ОС

Linux сосредоточены в модулях1 [12-14]. Это обусловлено тем, что, во-первых,

модули составляют большую часть всего ядра. Во-вторых, сердцевина ядра

активно используется разными модулями, а потому ошибки в ней выявляются

достаточно быстро. Кроме того, разработчики модулей ядра ОС Linux, как

правило, не являются экспертами в устройстве ядра. Например, большинство

драйверов устройств разрабатывается производителями соответствующего

аппаратного обеспечения. Подобное исследование для ядра ОС Microsoft

Windows ХР также показало, что наибольшее количество ошибок в ядре данной

1 Если говорить точнее, то в данных исследованиях была получена оценка числа ошибок только для драйверов устройств, которые составляют около 75% от числа всех модулей. Поэтому общее число ошибок в модулях может быть значительно больше 85%.

ОС находятся в драйверах устройств [15].

Модули ядра ОС Linux работают с тем же уровнем привилегий, что и сердцевина ядра, поэтому ошибки в них могут привести к ненадежной работе и снижению производительности всего ядра, а также и ОС в целом. Например, было продемонстрировано, как недоверенные пользовательские приложения могут использовать уязвимости в драйверах с целью исполнять произвольный код с привилегиями ядра и получать доступ к структурам ядра [16, 17]. В силу этого задача обеспечения различных аспектов качества модулей ядра ОС Linux является критически важной задачей.

Взаимодействие сердцевины ядра ОС Linux и модулей осуществляется следующим образом (рисунок 2):

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

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

2 Если не оговорено иное, то здесь и далее под программным интерфейсом сердцевины ядра понимается программный интерфейс только подсистем ядра без обработчиков событий.

Ext/

File Sys

MPEG

x с

реализация описание

A____L

API модулей (функции-обработчики)

О

?! а лз I

К s и ш

I

ш О

возврат

значении

ZÖE

_ вызовы

Обработчики событий

возврат значений

API сердцевины (подсистем ядра)

описание реализация

Подсистемы ядра

реализация описание

_А_____1_

API сердцевины (обработчиков событий) м-

«

системные возврат J/0 прерывания, вызовы,... зрачени^ ... порты, ... ...

Аппаратное еспечение

GNOME Пользовательские приложения

HübreOffice

Рисунок 2. Обработка событий в ядре ОС Linux (программный интерфейс для краткости называется API).

Как правило, программный интерфейс сердцевины ядра ОС Linux включает в себя следующие элементы3. Прототипы функций — наиболее часто используемые элементы программного интерфейса. Реализация этих функций находится в подсистемах ядра, static inline функции — функции с реализацией. Обычно такие функции небольшие по объему, и зачастую в телах этих функций вызываются функции, которые определены в подсистемах ядра. Макросы — в основном используются макрофункции. Если не оговорено иное, то в рамках данной работы считается, что макроподстановки аналогичны вызовам static inline функций (у параметров макрофункций и их возвращаемых значений нет типов). Другие возможности по использованию макросов в работе не рассматриваются. Декларации составных типов данных4 — в основном используются структуры, которые задают соглашение об организации данных, в том числе представлении функций-обработчиков, между сердцевиной и модулями.

Анализ изменений в модулях стабильных версий ядра за год разработки с 26.10.10 по 26.10.11 показал, что нарушения правил корректного использования программного интерфейса сердцевины ядра ОС Linux в модулях являются источником 15% от числа всех ошибок, или 50% от числа ошибок, которые не связаны с нарушениями спецификаций аппаратного обеспечения, сетевых протоколов, аудиокодеков и т.п.5 [18].

Дополнительное исследование, проведенное в рамках данной работы, показало, что программный интерфейс сердцевины ядра ОС Linux является достаточно многообразным:

- для обнаружения 170 видов нарушений правил корректного

3 Другие элементы используются намного реже по сравнению с данными и не рассматриваются в данной работе.

4 Под составными типами данных языка Си в данной работе понимаются структуры, объединения и перечисления.

5 Стоит отметить, что данные спецификации зачастую невозможно получить в полном виде.

использования программного интерфейса сердцевины ядра ОС Linux в модулях ядра требуется около 100 различных видов правил, причем для обнаружения 60% ошибок достаточно 30% правил;

- всего для модулей ядра требуется проверять порядка 2000 видов правил, из которых 600 позволяют обнаружить примерно 60% всех нарушений.

Программный интерфейс сердцевины ядра ОС Linux не является стабильным, что в частности подтверждается заявлением Грега Кроа-Хартмана, одного из ведущих разработчиков ядра ОС Linux [19]. Это утверждение относится только к тем элементам программного интерфейса, которые используются модулями ядра. На рисунке 2 — это API сердцевины (подсистем ядра). Элементы программного интерфейса, которые используются пользовательскими приложениями являются стабильными на протяжении долгих лет. На рисунке 2 — это API сердцевины (обработчиков событий).

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

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

Помимо изменения программного интерфейса сердцевины ядра ОС Linux с течением времени, программный интерфейс может предоставляться по-разному для различных конфигураций ядра. Существует огромное множество конфигураций ядра, но как будет показано в приложении А, отличия между ними, как правило, не очень существенны. Наиболее частым случаем изменений между парами разных конфигураций является то, что вместо прототипов функций предоставляются static inline функции либо макрофункции. Более существенные различия наблюдаются для такого важного частного случая конфигураций, как конфигурации для различных аппаратных платформ. Например, функция ioremap_cache определяется только для х86, Xtensa, IA-64 и SuperH, причем имеет три различные сигнатуры (п. АЛЛО).

Для поиска нарушений правил корректного использования программного интерфейса сердцевины ядра ОС Linux в модулях в данной работе предлагается применять передовые методы и инструменты верификации. Инструменты верификации, такие как BLAST [20], CPAchecker [21], UFO [22], LLBMC [23], Predator [24] и т.д., в настоящее время активно развиваются в университетах и научно-исследовательских институтах по всему миру. С каждым годом список инструментов пополняется [25-27]. Инструменты верификации реализуют различные подходы, что позволяет применять их для проверки различных аспектов качества программ. Среди этих инструментов нет однозначного

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

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

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

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

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

6 Как правило, достижимости оператора, помеченного специальной меткой, от некоторой точки входа в программу.

Таблица 1. Некоторые результаты международных мероприятий ETAPS/Competition on Software Verification 2013 года.

Инструмент

Организация-разработчик

BLAST 2.7.1 CPAchecker- CPAchecker- ESBMC Explicit 1.1.10 SeqCom 1.1.10 1.20

LLBMC

Predator

UFO

ИСП РАН, Университет Москва, Россия Пассау, Германия

Университет Федеральный Технологический Брненский Унивеситет

Анализ потока управления

Анализ указателей

Анализ циклов

Анализ битовых операций

Анализ структур данных в куче

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

Всего баллов (максимально 3791)

Всего времени работы (секунд)

Пассау, Германия

Университет институт

Амазонас, Карлсруэ,

Манаус, Германия Бразилия

технический Торонто, университет, Канада Чехия

81000

-27

166 36

-75 40 0

799 9 700

146

74 54

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

Цель работы — развитие метода контрактных спецификаций, который учитывает особенности процесса разработки ядра ОС Linux и обеспечивает возможность проверки правил корректного использования программного интерфейса сердцевины ядра в модулях посредством различных инструментов верификации.

Для достижения цели работы были поставлены следующие задачи:

а) Провести анализ существующих методов контрактных спецификаций.

б) Провести анализ и составить каталог наиболее критичных правил корректного использования программного интерфейса сердцевины ядра ОС Linux.

в) Разработать метод контрактных спецификаций, обеспечивающий следующие возможности:

1) описание в виде спецификаций всех правил из составленного каталога;

2) применение различных инструментов верификации для автоматизированной проверки модулей ядра ОС Linux на предмет выполнения требований спецификаций;

3) автоматизацию контроля корректности и согласованности спецификаций в условиях изменения программного интерфейса.

г) Разработать инструментарий, реализующий предлагаемый метод.

д) Оценить реализацию метода на практике, дать оценку области применимости метода.

Научной новизной обладают следующие результаты работы:

- новый метод описания в виде контрактных спецификаций правил корректного использования программного интерфейса сердцевины ядра ОС Linux, основанный на предложенном новом аспектно-ориентированном расширении языка Си\

- новый метод автоматизированного инструментирования исходного кода модулей ядра ОС Linux на основе контрактных спецификаций, позволяющий применять для его проверки различные инструменты верификации;

- новый метод автоматизированного контроля корректности и согласованности контрактных спецификаций в условиях изменения программного интерфейса сердцевины ядра ОС Linux.

На основе предлагаемого в работе метода контрактных спецификаций были разработаны и использованы на практике спецификации для 34 правил корректного использования программного интерфейса сердцевины ядра ОС Linux.

Инструментарий, реализующий предлагаемый метод контрактных спецификаций, был включен в состав системы верификации модулей ядра ОС Linux, разработанной в рамках проекта Linux Driver Verification (LDV) [28-33]. По результатам верификации модулей нескольких версий ядра ОС Linux уже было выявлено более 125 ошибок [33]. Исправления обнаруженных ошибок были направлены разработчикам ядра ОС Linux, которые включили их в состав последних версий ядра. Коллектив проекта Linux Driver Verification постоянно осуществляет мониторинг новых версий ядра ОС Linux, что позволяет как дорабатывать контрактные спецификации, так и находить новые ошибки по мере развития ядра.

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

Данный набор используется в рамках ежегодных мероприятий ETAPS/Competition on Software Vérification [26, 27, 29, 30, 34]. В будущем планируется обновлять данный набор на основе результатов верификации модулей новых версий ядра ОС Linux.

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

Основные положения работы докладывались на 8 конференциях и семинарах:

- Научно-практическая конференция «Актуальные проблемы программной инженерии» (г. Москва, 2009 г.);

- 52-я научная конференция МФТИ «Современные проблемы фундаментальных и прикладных наук» (г. Долгопрудный, 2009 г.);

- 5-й весенний/летний коллоквиум молодых исследователей в области программной инженерии (SYRCoSE, г. Екатеринбург, 2011 г.);

- 6-я летняя школа Microsoft Research (г. Кембридж, Великобритания, 2011г.);

- 8-я конференция разработчиков свободных программ (г. Обнинск, 2011г.);

- 2-й международный семинар Linux Driver Vérification в рамках 5-го международного симпозиума по внедрению формальных методов, верификации и валидации (LDV Workshop, ISoLA, г. Ираклион, о. Крит, Греция, 2012 г.);

- семинар ИСП РАН (г. Москва, 2012 г.);

- Европейская конференция по программной инженерии, совмещенная с

Симпозиумом по основам программной инженерии АСМ БЮБОРТ (ЕБЕС/РЗЕ, г. Санкт-Петербург, 2013 г.).

По теме диссертации автором опубликовано 15 работ [18, 25, 28, 29, 30, 34, 75, 97-101,113, 114, 119] (из них 7 в изданиях из перечня ВАК [18, 25, 28, 29, 100, 113, 114]) и получено 2 свидетельства о государственной регистрации программы дня ЭВМ [117,118].

Диссертация состоит из введения, 4 глав, заключения, списка литературы (132 наименования) и 2 приложений. Основной текст диссертации (без приложений и списка литературы) занимает 123 страницы.

Глава 1. Обзор существующих методов контрактных спецификаций

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

1.1 Неформальные методы контрактных спецификаций

Одним из основных подходов к заданию контрактных спецификаций был и остается подход к описанию требований к реализации и использованию программных интерфейсов в текстовом виде с использованием графиков, схем и таблиц [8, 35-37]. Существенным недостатком данного подхода является то, что подобное представление является неформальным. С одной стороны это приводит к тому, что описанные таким образом контрактные спецификации могут быть неадекватны, неполны, противоречивы или избыточны, одной из причин чего является развитие описываемых программных интерфейсов с течением времени [38]. С другой стороны, в общем случае подобное представление требований не может быть однозначно проинтерпретировано и использовано, например, для проведения автоматизированного тестирования или верификации.

Достаточно часто описание требований к реализации и использованию программных интерфейсов задается только неформальным образом. Поэтому данное представление используется при проведении экспертизы исходного кода программ [10, 39, 40] и при составлении каталогов требований [41-44], а также является основой для формального задания контрактных спецификаций.

1.2 Формальные методы контрактных спецификаций

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

В обзоре [45] отмечается, что для задания контрактных спецификаций программных систем в разных ситуациях могут подходить совершенно различные подходы. Для задания ограничений на допустимые значения, которые могут быть обработаны элементами программных интерфейсов, используются предусловия. В коде могут использоваться формальные ограничения (англ. assertions), которые накладывают ограничения на значения переменных по мере того, как система проходит через различные состояния выполнения. С помощью постусловий можно проверить функциональность компонента, описывая то, как его выходные значения зависят от входных. Конечные автоматы позволяют формализовать состояния системы и переходы между этими состояниями. С помощью диаграмм можно показать, как компонент взаимодействует с другими компонентами программной системы или его окружением. Варианты использования показывают, как пользователи с разными ролями могут взаимодействовать с программной системой.

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

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

В настоящее время существует очень большое количество различных подходов к заданию контрактных спецификаций. Достаточно подробно данные подходы рассмотрены и классифицированы в обзорах [45, 46]. В рамках данной работы мы не будем рассматривать все существующее многообразие средств для задания контрактных спецификаций, а остановимся только на некоторых из них. Таким образом будет показана история развития методов контрактных спецификаций и будут продемонстрированы преимущества и недостатки различных подходов при решении определенных задач.

1.2.1 Контрактные спецификации для компиляторов и интерпретаторов

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

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

Список литературы диссертационного исследования кандидат наук Новиков, Евгений Михайлович, 2013 год

Список использованных источников

1 Обзор рынка ОС встроенных систем [Электронный ресурс] / Режим доступа:

http://www.embeddedxom/ContentEETimes/Documents/Embedded.com/MarketStud у/2012_EmbeddedMarketStudy_UBM.pdf, свободный.

2 Обзор рынка ОС мобильных устройств [Электронный ресурс] / Режим доступа: http://www.netmarketshare.com/operatmg-system-market-share.aspx? qprid=8&qpcustomd=l, свободный.

3 Обзор рынка ОС интернет-серверов [Электронный ресурс] / Режим доступа: http://news.netcrafl.com/archives/2012/12/04/december-2012-web-server-survey.html, свободный.

4 Обзор рынка ОС суперкомпьютеров [Электронный ресурс] / Режим доступа: http://www.top500.org/statistics/overtime, свободный.

5 Создание ядра ОС Linux [Электронный ресурс] / Режим доступа: https://www.linux.com/learn/new-user-guides/376-linux-is-everywhere-an-overview-of-the-linux-operating-system?start=2, свободный.

6 J. Corbet, G. Kroah-Hartman, A. McPherson. Linux kernel development. How Fast it is Going, Who is Doing It, What They are Doing, and Who is Sponsoring It [Электронный ресурс] / Режим доступа: http://go.linuxfoundation.org/who-writes-linux-2012, свободный.

7 М. Т. Jones. Anatomy of the Linux kernel [Электронный ресурс] / Режим доступа: http://www.ibm.com/developerworks/linux/library/l-linux-kernel, свободный.

8 R. Love. Linux kernel development // Novell Press, 401 pp., 2005.

9 M. T. Jones. Anatomy of Linux loadable kernel modules [Электронный ресурс] / Режим доступа: http://www.ibm.com/developerworks/linux/library/l-lkm/index.html, свободный.

10 E.S. Raymond. The Cathedral and the Bazaar: Musings on Linux and Open Source by an Accidental Revolutionary // O'Reilly, Sebastopol, CA, USA, 2001.

11 R.L. Glass. Facts and Fallacies of Software Engineering // Addison Wesley, Professional, Sebastopol, CA, USA, 2003.

12 A. Chou, J. Yang, B. Chelf, S. Hallem, and DR Engler. An Empirical Study of Operating System Errors // Proc. 18th ACM Symp. Operating System Principles, 2001.

13 M. Swift, B. Bershad, H. Levy. Improving the reliability of commodity operating systems // In: SOSP '03: Proceedings of the nineteenth ACM symposium on Operating systems principles, 2003.

14 N. Palix, G. Thomas, S. Saha, C. Calves, J. Lawall, and Gilles Muller. Faults in linux: ten years later // Proceedings of the sixteenth international conference on Architectural support for programming languages and operating systems (ASPLOS'll), USA, 2011.

15 A. Ganapathi, V. Ganapathi, D. Patterson. Windows XP kernel crash analysis // Proceedings of the 2006 Large Installation System Administration Conference, 2006.

16 S. Butt, V. Ganapathy, M.M. Swift, C.-C. Chang. Protecting Commodity Operating System Kernels from Vulnerable Device Drivers // Computer Security Applications Conference (ACSAC '09), 2009.

17 D. Tian, X. Xiong, C. Hu, P. Liu. Policy-centric protection of OS kernel from vulnerable loadable kernel modules // Proceedings of the 7th international conference on Information security practice and experience, 2011.

18 Мутилин B.C., Новиков E.M., Хорошилов A.B. Анализ типовых ошибок в драйверах операционной системы Linux // Труды Института системного программирования РАН. 2012. Т. 22. С. 349-374.

19 G. Kroah-Hartman. The Linux Kernel Driver Interface [Электронный ресурс] / Режим доступа:

http://www.kernel.org/doc/Documentation/stable_api_nonsense.txt, свободный.

20 P. Shved, M. Mandrykin, V. Mutilin. Predicate Analysis with Blast 2.7 // Proceedings of TACAS, vol. 7214, pp. 525-527,2012.

21 S. Lowe, P. Wendler. CPAchecker with Adjustable Predicate Analysis // Proceedings of TACAS, vol. 7214, pp. 528-530,2012.

22 A. Albarghouthi, A. Gurfmkel, Y. Li, S. Chaki, M. Chechik. UFO: Verification with Interpolants and Abstract Interpretation // Proceedings of TACAS, vol. 7795, pp. 637-640,2013.

23 C. Sinz, F. Merz, S. Falke. LLBMC: A Bounded Model Checker for LLVM's Intermediate Representation // Proceedings of TACAS, vol. 7214, pp. 542544,2012.

24 K. Dudka, P. Mtiller, P. Peringer, T. Vojnar. Predator: A Verification Tool for Programs with Dynamic Linked Data Structures // Proceedings of TACAS, vol. 7214, pp. 545-548, 2012.

25 Мандрыкин М.У., Мутилин B.C., Новиков E.M., Хорошилов A.B. Обзор инструментов статической верификации Си программ в применении к драйверам устройств операционной системы Linux // Труды Института системного программирования РАН. 2012. Т. 22. С. 293-326.

26 D. Beyer. Competition on Software Verification // Proceedings of TACAS, vol. 7214, pp. 504-524, 2012.

27 D. Beyer. Second Competition on Software Verification // Proceedings of TACAS, vol. 7795, pp. 594-609,2013.

28 Мутилин B.C., Новиков E.M., Страх A.B., Хорошилов A.B., Швед П.Е. Архитектура Linux Driver Verification // Труды Института системного программирования РАН. 2011. Т. 20. С. 163-187.

29 Мандрыкин М.У., Мутилин B.C., Новиков Е.М., Хорошилов А.В., Швед П.Е. Использование драйверов устройств операционной системы Linux для сравнения инструментов статической верификации // Программирование.

2012. №5. С. 54-71.

30 Khoroshilov A., Mutilin V., Novikov E., Shved P., Strakh A. Towards an open framework for С verification tools benchmarking // Perspectives of Systems Informatics, Lecture Notes in Computer Science. 2012. V. 7162. Pp. 179-192.

31 D. Beyer and A. K. Petrenko. Linux driver verication // In Proc. ISoLA, LNCS 7610, Springer, pp. 1-6, 2012.

32 Открытая система верификации модулей ядра Linux Driver Verification [Электронный ресурс] / Режим доступа: http://linuxtesting.org/ldv, свободный.

33 Список ошибок, выявленных в модулях ядра Linux с помощью системы Linux Driver Verification [Электронный ресурс] / Режим доступа: http://linuxtesting.org/results/ldv, свободный.

34 Beyer D., Lowe S., Novikov E., Stahlbauer A., Wendler P. Precision Reuse for Efficient Regression Verification // Proceedings of the 9th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering. 2013. Pp. 389-399.

35 J. Corbet, A. Rubini, and G. Kroah-Hartman. Linux Device Drivers, Third Edition [Электронный ресурс] / Режим доступа: http://lwn.net/Kernel/LDD3, свободный.

36 Документация по ядру ОС Linux [Электронный ресурс] / Режим доступа: https://www.kernel.org/doc/Documentation, свободный.

37 М. Kerrisk. Linux Programming Interface // No Starch Press, 1552 pp., October, 2010.

38 D. M. Berry, M. M. Krieger. From Contract Drafting to Software Specification: Linguistic Sources of Ambiguity - A Handbook Version 1.0 [Электронный ресурс] / Режим доступа: https://cs.uwaterloo.ca/~dberry/handbook/ambiguityHandbook.pdf, свободный.

39 М. Е. Fagan. Design and Code Inspections to Reduce Errors in Program Development//IBM Systems Journal, 15(3), 182-211,1976.

40 В. Boehm, V. Basili. Software Defect Reduction Top 10 List // IEEE Computer, 34(1), 135-137, January, 2001.

41 В. В. Купямин, H. В. Пакулин, О. JI. Петренко, А. А. Сортов, А. В. Хорошнлов. Формализация требований на практике // Препринт 13, ИСП РАН, Москва, 2006.

42 Э. Халл, К. Джексон, Дж. Дик. Разработка и управление требованиями. Практическое руководство пользователя // Telelogic, 2005.

43 Система управления требованиями Requality [Электронный ресурс] / Режим доступа: http://requality.ru/ru, свободный.

44 С. W. George, R. Е. Milne. Specifying and Refining Concurrent Systems — an Example from the RAISE Project // In Proceedings of 3rd Refinement Workshop, Springer-Verlag, 1990.

45 J. Hatcliff, G. T. Leavens, K. R. M. Leino, P. Miiller, and M. Parkinson. Behavioral interface specification languages // ACM Comput. Surv. 44, 3, Article 16, 2012.

46 B.B. Кулямин. Методы верификации программного обеспечения // Всероссийский конкурсный отбор обзорно-аналитических статей по приоритетному направлению "Информационно-телекоммуникационные системы", 2008.

47 Атрибуты для функций — расширение языка программирования Си компилятора GCC [Электронный ресурс] / Режим доступа: http://gcc.gnu.org/onlinedocs/gcc/Function-Attributes.html, свободный.

48 D. С. Luckham, F. W. Von Henke. An Overview of Anna, a Specification Language for Ada // IEEE Software archive, v. 2, issue 2, pp. 9-22, March, 1985.

49 R. C. Holt and J. R. Cordy. The Turing programming language // Commun. ACM 31,12, pp. 1410-1423, December, 1988.

50 B. Meyer. Applying "Design by Contract" // Computer archive, v. 25, issue 10, pp. 40-51, October, 1992.

51 D. S. Rosenblum. A Practical Approach to Programming With Assertions // IEEE Transactions on Software Engineering archive, v. 21, issue 1, pp. 19-31, January, 1995.

52 G. J. Holzmann. Logic Verification of ANSI-C Code with SPIN // In Proceedings of the 7th International SPIN Workshop on SPIN Model Checking and Software Verification, Klaus Havelund, John Penix, and Willem Visser (Eds.), Springer-Verlag, London, UK, pp. 131-147, 2000.

53 D. S. Rosenblum, В. Krishnamurthyio. An Event-Based Model of Software Configuration Management// SCM, pp. 94-97,1991.

54 M. Obayashi, H. Kubota, S. P. McCarron and L. Mallet. The assertion based testing tool for OOP: ADL2 // In International Conference on Software Engineering, 1998.

55 W. Grieskamp, Y. Gurevich, W. Schulte, and M. Veanes. Testing with Abstract State Machines // In R. Moreno-Diaz and A. Quesada-Arencibia, eds., Formal Methods and Tools for Computer Science (Proceedings of Eurocast 2001), Universidad de Las Palmas de Gran Canaria, Canary Islands, Spain, pp. 257-261, February 2001.

56 E. Farchi, A. Hartman, and S. S. Pinter. Using a model-based test generator to test for standard conformance // IBM Systems Journal, v. 41, pp. 89-110, Number 1,2002.

57 A.B. Баранцев, И.Б. Бурдонов, A.B. Демаков, C.B. Зеленов, A.C. Косачев, B.B. Кулямин, В.А. Омельченко, Н.В. Пакулин, А.К. Петренко, A.B. Хорошилов. Подход UniTesK к разработке тестов: достижения и перспективы // Труды Института системного программирования РАН, т. 5,2004.

58 D. Engler, В. Chelf, A. Chou, S. Hallem. Checking system rules using system-specific, programmer-written compiler extensions // Proceedings of the 4th conference on Symposium on Operating System Design & Implementation, San Diego, California, pp.1-16, October 22-25,2000.

59 Coverity Scan: 2011 Open Source Integrity Report [Электронный ресурс] / Режим доступа: http://www.coverity.com/library/pdf/coverity-scan-2011-open-source-integrity-report.pdf, свободный.

60 D. Evans and D. Larochelle. Improving Security Using Extensible Lightweight Static Analysis // In IEEE Software, v. 19, issue 1, pp. 42-51, January, 2002.

61 H. Stuart. Hunting bugs with Coccinelle // Masters Thesis, University of Copenhagen, August, 2008.

62 V. Nesov. Automatically finding bugs in open source programs // Third International Workshop on Foundations and Techniques for Open Source Software Certification. OpenCert, v. 20, pp. 19-29,2009.

63 С. Сыромятников. Декларативный интерфейс поиска дефектов по синтаксическим деревьям: язык KAST // Труды Института системного программирования РАН, т. 20, стр. 51-68, 2011.

64 Sparse - a Semantic Parser for С [Электронный ресурс] / Режим доступа: https://sparse.wiki.kernel.org/index.php/Main_Page, свободный.

65 Dan Carpenter. Killing Bugs in С with Smatch // Linux Plumbers Conference, Santa Rosa, California, September 7-9, 2011.

66 G.J. Holzmann, The model checker SPIN // IEEE Trans, on Software Engineering, Vol. 23, No. 5, pp. 279-295, May, 1997.

67 В. K. Aichernig and P. G. Larsen. A Proof Obligation Generator for VDM-SL // In John S. Fitzgerald, Cliff B. Jones, and Peter Lucas, editors, FME'97: Industrial Applications and Strengthened Foundations of Formal Methods Proc. 4th Intl. Symposium of Formal Methods Europe, Graz, Austria, volume 1313 of Lecture Notes in Computer Science, Springer-Verlag, pp. 338-357, September, 1997.

68 T. Mossakowski, C. Maeder, and K. Liittich. The heterogeneous tool set, HETS // In Proceedings of the 13th international conference on Tools and algorithms for the construction and analysis of systems (TACAS'07), Orna Grumberg and

Michael Huth (Eds.). Springer-Verlag, Berlin, Heidelberg, pp. 519-522, 2007.

69 G.J. Holzmann, J. Patti. Validating SDL Specification: an Experiment // In E. Brinksma, G. Scollo, Ch.A. Vissers, editors, Protocol Specification, Testing and Verification, Enchede, The Netherlands, pp. 317-326, Amsterdam, North-Holland, 1990.

70 J. Hatcliff, M.B. Dwyer, and H. Zheng. Slicing software for model construction // Journal of Higher-Order and Symbolic Computation, Volume 13, Issue 4, pp. 315-353, 2000.

71 K. Havelund, T. Pressburger. Model Checking Java Programs Using Java PathFinder // Int. Journal on Software Tools for Technology Transfer, Volume 2, Issue 4, pp. 366-381,2000.

72 J. C. Corbett, M. B. Dwyer, J. Hatclif, and Robby. A language framework for expressing checkable properties of dynamic software // In SPIN 00: SPIN Workshop, LNCS 1885, Springer-Verlag, 2000.

73 D. Engler, M. Musuvathi. Static analysis versus model checking for bug finding // In VMCAI, pp. 191-210,2004.

74 B.C. Мутилин. Верификация драйверов операционной системы Linux при помощи предикатных абстракций // Диссертация на соискание ученой степени кандидата физико-математических наук, 2012.

75 Zakharov I., Mutilin V., Novikov Е., Khoroshilov A. Generating Environment Model for Linux Device Drivers // Proceedings of the 7th Spring/Summer Young Researchers' Colloquium on Software Engineering. Kazan. 2013. Pp. 77-83.

76 T. Witkowski, N. Blanc, D. Kroening, G. Weissenbacher. Model checking concurrent Linux device drivers // In Proceedings of the twenty-second IEEE/ACM international conference on Automated software engineering, pp. 501-504,2007.

77 T. Ball, E. Bounimova, V. Levin, R. Kumar, J. Lichtenberg. The Static Driver Verifier Research Platform // CAV 2010, 2010.

78 Т. Ball, S. К. Rajamani. SLIC: A specification language for interface checking of С // Technical Report MSR-TR-2001-21, Microsoft Research, 2001.

79 T. Ball, V. Levin, and S. K. Rajamani. A decade of software model checking with SLAM // Commun. ACM 54, 7, pp. 68-76, July, 2011.

80 T. Ball, E. Bounimova, R. Kumar, and V. Levin. SLAM2: static driver verification with under 4% false alarms // In Proceedings of the 2010 Conference on Formal Methods in Computer-Aided Design (FMCAD '10). FMCAD Inc, Austin, TX, pp. 35-42,2010.

81 H. Post, W. Ktichlin. Integration of static analysis for Linux device driver verification // The 6th Intl. Conf. on Integrated Formal Methods, IFM 2007,2007.

82 F. Meissner. Regelbasierte Spezifikation von Linux Kernel-Schnittstellen mit SLIC // Master's Thesis, 2007.

83 E. Clarke, D. Kroening, F. Lerda. A tool for checking ANSI-C programs // In Jensen, K., Podelski, A., eds.: Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Volume 2988 of LNCS, Springer, pp. 168-176,2004.

84 D.L. Parnas. On the Criteria To Be Used in Decomposing Systems into Modules // Communications of the ACM, Vol. 15, No. 12, pp. 1053 - 1058,1972.

85 A.JI. Фуксман. Технологические аспекты создания программных систем // М.: Статистика, 1979.

86 Определения понятий аспектно-ориентированного программирования. [Электронный ресурс] / Режим доступа: http://www.aosd.net/wiki/index.php? title=Glossary, свободный.

87 G. Kiczales, Е. Hilsdale, J. Hugunin, М. Kersten, J. Palm, and W. G. Griswold. An Overview of AspectJ // In Proceedings of the 15th European Conference on Object-Oriented Programming (ECOOP '01), 327-353,2001.

88 O. Spinczyk, D. Lohmann, and M. Urban. AspectC++: an AOP extension for С++ // Software Developer's Journal, pp. 68-76, May, 2005.

89 B.O. Сафонов. Aspect.NET - инструмент аспектно-ориентированного

программирования для разработки надежных и безопасных программ. Компьютерные инструменты в образовании // СПб.: Изд-во ЦПО «Информатизация образования», н. 5, стр. 3-13,2007.

90 M. Gong, С. Zhang, and Н.-А. Jacobsen. AspeCt-oriented С // Technology Showcase, CASCON 2007, Markahm, Ontario, 2007.

91 W. Gong and H.-A. Jacobsen // AspeCt-oriented С Language Spefication Version 0.8. University of Toronto, 2008.

92 J. Seyster, K. Dixit, X. Huang, R. Grosul, K. Havelund, S. A. Smolka, S. D. Stoller, and E. Zadok. Aspect-Oriented Instrumentation with GCC // First International Conference on Runtime Verification, Malta, v. 6418, pp. 405-420,2010.

93 AspectJ: аспектно-ориентированное расширение к языку программирования Java [Электронный ресурс] / Режим доступа: http://www.eclipse.org/aspectj7doc/released/progguide/language.html, свободный.

94 Введение в AspectJ [Электронный ресурс] / Режим доступа: http://eclipse.org/aspectj7doc/released/progguide/starting-aspectj.html, свободный.

95 aje: компилятор языка программирования Java и его расширения AspectJ [Электронный ресурс] / Режим доступа: http://www.eclipse.org/aspectj/doc/released/devguide/ajc-ref.html, свободный.

96 Плагины GCC [Электронный ресурс] / Режим доступа: http://gcc.gnu.org/wiki/plugins, свободный.

97 Новиков Е.М. Использование аспектно-ориентированного подхода программирования в процессе верификации ядра операционной системы Linux // Сборник научных трудов Научно-практической конференции «Актуальные проблемы программной инженерии». Москва, 2009. С. 148-154.

98 Мутилин B.C., Новиков Е.М., Хорошилов A.B. Классификация концепций для аспектно-ориентированного расширения языка программирования С // Труды 52-й научной конференции МФТИ «Современные проблемы фундаментальных и прикладных наук», часть 7 «Управление и

прикладная математика». Долгопрудный, 2009. Т. 2. С. 31-33.

99 Новиков Е.М., Хорошилов А.В. Реализация аспектно-ориентированного программирования для языка Си // Тезисы докладов восьмой конференции разработчиков свободных программ. Обнинск, 2011. С. 23-26.

100 Новиков Е.М. Подход к реализации аспектно-ориентированного программирования для языка Си // Программирование. 2013. №4. С. 47-65.

101 Novikov Е. One Approach to Aspect-Oriented Programming Implementation for the С programming language // Proceedings of the 5th Spring/Summer Young Researchers' Colloquium on Software Engineering. Yekaterinburg. 2011. Pp. 74-81.

102 Новиков Е.М. Упрощение анализа трасс ошибок инструментов статического анализа кода // Сборник научных трудов научно-практической конференции «Актуальные проблемы программной инженерии», 25-26 мая, Москва, 215-221,2011.

103 S. Paul and A. Prakash. Querying Source Code using an Algebraic Query Language // In Proceedings of the International Conference on Software Maintenance, pp. 127-136,1994.

104 S. Paul, A. Prakash. A framework for source code search using program patterns // In IEEE Transactions on Software Engineering, pp. 463-475,1994.

105 W. G. Griswold, D. C. Atkinson, and C. McCurdy. Fast, flexible syntactic pattern matching and processing // In WPC'96: Proceedings of the 4th International Workshop on Program Comprehension (WPC'96), Washington, DC, USA, p. 144, 1996.

106 J. Ebert, B. Kullbach, A. Winter. Querying as an Enabling Technology in Software Reengineering // Proceedings of the Third European Conference on Software Maintenance and Reengineering, p.42, March 03-05, 1999.

107 E. Hajiyev, M. Verbaere, O. de Moor. CodeQuest: scalable source code queries with datalog // Proceedings of the 20th European conference on Object-

Oriented Programming, Nantes, France, July 03-07,2006.

108 M. P. Robillard, G. C. Murphy. Concern graphs: finding and describing concerns using structural program dependencies // Proceedings of the 24th International Conference on Software Engineering, May 19-25, Orlando, Florida, 2002.

109 D. Janzen and K. D. Voider. Navigating and querying code without getting lost // In Proceedings of the 2nd international conference on Aspect-oriented software development (AOSD '03), 178-187,2003.

110 Интегрированная среда разработки Eclipse [Электронный ресурс] / Режим доступа: http://www.eclipse.org, свободный.

111 Y. Padioleau, J. L. Lawall, and G. Muller. Understanding collateral evolution in Linux device drivers // In Proceedings of the 1st ACM SIGOPS/EuroSys European Conference on Computer Systems 2006 (EuroSys '06), 59-71,2006.

112 M. Kimmig, M. Monperrus, and M. Mezini. Querying source code with natural language // In Proceedings of the 2011 26th IEEE/ACM International Conference on Automated Software Engineering (ASE '11), IEEE Computer Society, Washington, DC, USA, 376-379, 2011.

113 Новиков E.M., Хорошилов A.B. Использование аспектно-ориентированного программирования для выполнения запросов по исходному коду программ // Труды Института системного программирования РАН. 2012. Т. 23. С. 371-386.

114 Новиков Е.М. Построение спецификаций программных интерфейсов в открытой системе покомпонентной верификации ядра Linux // Труды Института системного программирования РАН. 2013. Т. 24. С. 293-316.

115 ISO/IEC JTC1 SC22 WG14. ISO/IEC 9899:ТС2 Programming Languages - С. 6 May, 2005.

116 Документация по компилятору GCC версий 4.6.x. [Электронный ресурс] / Режим доступа: http://gcc.gnu.Org/onlinedocs/gcc-4.6.4/gcc, свободный.

117 Новиков Е.М. Свидетельство о государственной регистрации программы для ЭВМ №2012615598 от 20.06.2012 «Система аспектно-ориентированного программирования для языка Си».

118 Мандрыкин М.У, Мутилин B.C., Новиков Е.М., Хорошилов A.B., Швед П.Е. Свидетельство о государственной регистрации программы для ЭВМ №2012615596 от 20.06.2012 «Система проверки выполнения проблемно-ориентированных правил для Си программ».

119 Щепетков И.В., Новиков Е.М. Диагностика синтаксической совместимости правил корректности с ядром ОС Linux при статической верификации драйверов // Сборник научных трудов Научно-практической конференции «Актуальные проблемы системной и программной инженерии». Москва, 2013. С. 192-201.

120 И.В. Щепетков. Диагностика синтаксической совместимости спецификаций правил корректности с программным интерфейсом ядра ОС Linux // Выпускная квалификационная работа на степень бакалавра, 2013.

121 Гратинский В.А. Метод валидации систем верификации драйверов Linux // Сборник научных трудов научно-практической конференции «Актуальные проблемы системной и программной инженерии». Москва, 2013. С. 60-64.

122 D. Chamberlain, D. Cross, A. Wardley. Perl Template Toolkit // O'Reilly Media, pp. 592, December, 2003.

123 N. Gunton. Creating Modular Web Pages With EmbPerl [Электронный ресурс] / Режим доступа: http://www.perl.com/pub/2001/03/embperl.html, свободный.

124 Определение утечки ресурса [Электронный ресурс] / Режим доступа: http://cwe.mitre.org/data/definitions/401 .html, свободный.

125 Определение повторного освобождения ресурса [Электронный ресурс] / Режим доступа: http://cwe.mitre.org/data/definitions/415.html,

свободный.

126 Ошибки в программах, которые могут повредить память [Электронный ресурс] / Режим доступа: http://cwe.mitre.org/data/definitions/633.html, свободный.

127 Определение разыменования нулевого указателя [Электронный ресурс] / Режим доступа: http://cwe.mitre.org/data/defmitions/476.html, свободный.

128 Определение переполнения целых чисел [Электронный ресурс] / Режим доступа: http://cwe.mitre.org/data/definitions/190.html, свободный.

129 J. Corbet. Atomic context and kernel API design [Электронный ресурс] / Режим доступа: http://lwn.net/Articles/274695/, свободный.

130 Определение незащищенности данных [Электронный ресурс] / Режим доступа: http://cwe.mitre.org/data/definitions/200.html, свободный.

131 Определение взаимной блокировки [Электронный ресурс] / Режим доступа: http://cwe.mitre.org/data/definitions/833.html, свободный.

132 Определение гонки [Электронный ресурс] / Режим доступа: http://cwe.mitre.org/data/definitions/362.html, свободный.

Приложение А Каталог наиболее критичных правил корректного использования программного интерфейса сердцевины ядра

ОС Linux

СОДЕРЖАНИЕ

А.1 Выделение и освобождение ресурсов....................................................................................143

А.1.1 Счетчики ссылок USB-устройств...................................................................................145

А. 1.2 DMA-буферы USB-устройств.........................................................................................147

А.1.3 URB для контроллеров USB-шин...................................................................................150

А.1.4 Счетчики ссылок трансиверов USB On-the-Go.............................................................152

А. 1.5 NOP-трансиверы USB On-the-Go...................................................................................155

А.1.6 URB.................................................................................................................................157

А.1.7 DMA-отображения для SCSI-команд.............................................................................158

А. 1.8 DMA-отображения для PCI-устройств..........................................................................160

А. 1.9 Ю-память..........................................................................................................................163

А. 1.10 Отображения Ю-памяти................................................................................................165

А.1.11 Сокет-буферы.................................................................................................................167

А.1.12 ACPI.................................................................................................................................170

A.1.13BLK..................................................................................................................................172

А .1.14 Кэш-память.....................................................................................................................173

A.1.15GPIO................................................................................................................................175

A.1.16IDR...................................................................................................................................177

A.1.17NAPI................................................................................................................................179

А. 1.18 GPIO для ASoC-разъемов..............................................................................................181

А. 1.19 Группы для виртуальных файловых систем................................................................183

А. 1.20 Обработчики прерываний.............................................................................................185

А. 1.21 Потоки ядра....................................................................................................................187

А. 1.22 Элементы списков..........................................................................................................189

А.2 Допустимые фактические параметры....................................................................................192

А.2.1 Заполнение буферов.........................................................................................................192

А.2.2 Копирование строк в буферы..........................................................................................193

А.2.3 Сравнение строк...............................................................................................................193

А.2.4 Работа со строками..........................................................................................................194

А.2.5 Копирование буферов из/в пространства пользователя...............................................197

А.2.6 Работа с ТТУ-устройствами............................................................................................198

А.2.7 Выделение памяти...........................................................................................................203

А.2.8 Работа с программным инструментом упреждающей защиты АррАгшог.................204

А.2.9 Поиск битов......................................................................................................................205

А.2.10 Работа с часами..............................................................................................................206

А.2.11 Задержка выполнения....................................................................................................208

А.2.12 Добавление 12С-адаптера..............................................................................................210

А.2.13 Выделение памяти для ММС-хоста.............................................................................210

А.2.14 Работа с файлами...........................................................................................................211

А.2.15 Добавление данных в сокет-буферы............................................................................212

А.2.16 Обновление времени истечения таймера.....................................................................213

А.2.17 Работа с ШВ-интерфейсами.........................................................................................213

А.З Работа в атомарном контексте................................................................................................216

А. 3.1 Блокирующее выделение памяти...................................................................................218

А.3.2 Функции, которые могут заснуть...................................................................................225

А.3.3 Функции, которые могут делать планирование............................................................226

А.4 Инициализация ресурсов........................................................................................................227

А.4.1 Копирование буферов в пространство пользователя....................................................227

А.4.2 Файлы с атрибутами устройств для виртуальных файловых систем.........................228

А.4.3 Спин-блокировки.............................................................................................................230

А.5 Использование различных примитивов синхронизации в одном потоке...........................233

А. 5.1 Мьютексы.........................................................................................................................233

А.5.2 11еас1Лугке-семафоры.......................................................................................................238

А.5.3 Спин-блокировки.............................................................................................................244

А.5.4 ММС-блокировки............................................................................................................253

А.5.5 Большая блокировка ядра................................................................................................255

При описании элементов программного интерфейса в данном приложении рассмотрена вся их эволюция, начиная с ядра версии 2.6.32 и заканчивая ядром версии 3.10, и всевозможные их конфигурации. Если специально не оговаривается, то элемент входит во все версии ядра и конфигурации. В противном случае в скобках непосредственно за сигнатурой элемента указывается те версии ядра и/или конфигурации, в которых он представлен. Последнее делается обязательно в том случае, если в одной и той же версии ядра имеется несколько вариантов описания одного и того же элемента (совпадение элементов определяется по имени).

При описании общих предположений для всех типов правил, а также непосредственно самих правил корректного использования элементов программного интерфейса были активно задействованы документация по ядру ОС Linux [35, 36] и описание известных нарушений правил, выявленных на основе изменений в модулях стабильных версий ядра за год разработки с 26.10.10 по 26.10.11 [18].

А.1 Выделение и освобождение ресурсов

Правила данного типа описывают корректное использование программного интерфейса для выделения и освобождения ресурсов40 в модулях ядра ОС Linux. Нарушения данных правил могут привести, например, к утечкам ресурсов (модули не освобождают выделенные для них ресурсы после их использования) [124] и повторному освобождению ресурсов [125].

Для выделения ресурсов в модулях используются либо общие функции выделения областей динамически распределяемой памяти, такие как kmalloc, которая выделяет запрашиваемое количество байт, и kzalloc, которая выделяет запрашиваемое количество байт и обнуляет соответствующую область памяти; либо специализированные функции, в число которых входят, например, usb_alloc_urb, scsi_dmajnap и usb_alloc_coherent. В случае успешного выделения указатель на ресурс передается в качестве возвращаемого значения (kmalloc, kzalloc, usb_alloc_urb) или присваивается одному из аргументов, который передается по указателю (usb_alloc_coherenf). При нехватке памяти в системе и в случае ошибок возвращается 0 (kmalloc, kzalloc, usb_alloc_urb, usb_alloc_coherent) или код соответствующей ошибки (scsi_dma_map).

Для освобождения ресурсов в модулях используются элементы программного интерфейса, которые являются парными для соответствующих элментов для выделения памяти. Например, для kmalloc используется kfree, а для usb_alloc_urb - usb_free_urb. В качестве одного из аргументов им передается указатель на выделенный ранее ресурс.

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

Правила для данных элементов программного интерфейса сердцевины ядра ОС Linux формулируются в следующих предположениях:

- на момент начала работы модуля для него не выделено никаких ресурсов;

- при успешном выделении ресурсов в динамически распределяемой области памяти всегда возвращаются указатели на новые и/или освобожденные области памяти;

- модули работают независимо друг от друга и, соответственно, каждому модулю запрещается освобождать те ресурсы, которые не были выделены для него;

- модулям запрещается повторно освобождать одни и те же ресурсы;

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

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

Правила, которые затрагивают счетчики ссылок, формулируются в следующих предположениях:

- на момент начала работы модуля счетчики ссылок для используемых им

ресурсов инициализированы некоторыми положительными значениями (например, 1);

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

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

А.1.1 Счетчики ссылок USB-устройств

Известные нарушения: 927c3fa41.

Описание элементов программного интерфейса.

Счетчик ссылок для USB-устройства увеличивается с помощью функции struct usbjdevice *usb_get_dev(struct usb_device *), если ей в качестве фактического параметра передается ненулевой указатель на структуру USB-устройства. usb_get_dev возвращает значение данного фактического параметра.

Счетчик ссылок для USB-устройства уменьшается с помощью функции void usb_put_dev(struct usb_device *), если ей в качестве фактического параметра передается ненулевой указатель на структуру USB-устройства.

Правила корректного использования элементов программного интерфейса.

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

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

41 Здесь и далее указаны идентификаторы изменений, которые были сделаны в ветках стабильных версий ядра репозитория https://git.kernel.org/cgit/linnx/kernel/git/stable/linux-stable.git с целью исправления нарушений правил корректного использования программного интерфейса сердцевины ядра ОС Linux.

увеличивал.

Модельные переменные и модельные функции.

#include <linux/usb.h> #include <verifier/rcv.h>

Map LDV_USB_DEV_REF_COUNTS = EmptyMap;

struct usb_device *ldv_usb_dev_ref_count_increment (struct usb_device *dev) { if (!dev) { return dev;

}

if (containsKey(LDV_USB_DEV_REF_COUNTS, dev)) { put (LDV_USB_DEV_REF_C0UNT3, dev, get {LDV_USB_DEV_REF_COUNTS) + 1) ; } else {

put (LDV_USB_DEV_REF_COUNTS, dev, 1);

}

return dev?

}

void ldv_usb_dev_ref_count_decrement (struct usb_device *dev) { if (!dev) { return;

}

if (get(LDV_USB_DEV_REF_COUNTS, dev) >1) { put {LDV_USB_DEV_REF_COUNTS, dev

, get (LDV_USB_DEV_REF_COUNTS, dev) - 1) ; } else {

remove {LDV_USB_DEV_REF_COUNTS, dev) ;

}

}

Множества точек использования элементов программного интерфейса.

pointcut USB_DEV_REF_COUNT_INCREMENT:

call(struct usb_device *usb_get_dev{struct usb_device *)) pointcut USB_DEV_REF_COUNT_DECREMENT:

call(void usb_put_dev(struct usb_device *))

Привязка модельных функций к точкам использования элементов программного интерфейса.

around: USB_DEV_REF_COUNT_INCREMENT {

return ldv_usb_dev_ref_count_increment($argl);

}

around: USB_DEV_REF_COUNT_DECREMENT { ldv_usb_dev_ref_count_decrement ($argl) ;

}

Предусловия использования элементов программного интерфейса.

before: USB_DEV_REF_COUNT_DECREMENT { if ($argl) {

ldv_assert (containsKey (LDV_USB_PEV_REF_COUNTS, $argl) && get(LDV_USB_DEV_REF_COUNTS, $argl) > 0);

}

}

after: MODULE_EXIT {

ldv_assert (isEmpty (LDV_USB_DEV_REF_COUNTS)) ;

}

A.1.2 DMA-буферы USB-устройств

Известные нарушения: 0653136.

Описание элементов программного интерфейса.

DMA-буфер для USB-устройства выделяется с помощью функции void *usb_alloc_coherent(struct usb_device * size_t, gfp_t, dma_addr_t *) (с версии 2.6.34), если ей в качестве первого и второго фактических параметров передаются ненулевой указатель на структуру USB-устройства и размер запрашиваемого DMA-буфера. Если DMA-буфер удается выделить, usb_alloc_coherent возвращает указатель на DMA-буфер в пространстве ядра и присваивает четвертому формальному параметру указатель на DMA-буфер на шине. Иначе usb_alloc_coherent возвращает 0.

DMA-буфер для USB-устройства освобождается с помощью функции void usb Jree_coherent (struct usb_device *, size J, void *, dma_addr_t) (с версии

2.6.34), если ей в качестве первого, второго, третьего и четвертого фактических параметров передаются ненулевой указатель на структуру USB-устройства, размер DMA-буфера, ненулевой указатель на DMA-буфер в пространстве ядра и указатель на DMA-буфер на шине.

Правила корректного использования элементов программного интерфейса.

В процессе работы модулю запрещается освобождать невыделенные для него DMA-буферы для USB-устройств и повторно освобождать одни и те же DMA-буферы для USB-устройств.

На момент завершения работы модуль должен освободить все выделенные для него DMA-буферы для всех USB-устройств.

Модельные переменные и модельные функции.

#include <linux/usb.h>

ttinclude <verifier/rcv.h>

Map LDV_USB_DMA_BUFS = EmptyMap;

void *ldv_usb_dma_buf_alloc(struct usb_device *dev, size_t size , dma_addr_t *dma) { void *dma_buf; if (!dev) {

return NULL;

}

dma_buf = ldv_alloc_dma_buf (dma) ; if (dma_buf) {

if (!containsKey{LDV_USB_DMA_BUFS, dev)) { put(LDV_USB_DMA_BUFS, dev, EmptyMap);

}

if (!containsKey(get(LDV_USB_DMA_BUFS, dev), (void *)size)) { put(get{LDV_USB_DMA_BUFS, dev), (void *)size, EmptySet);

}

add (get(get(LDV_USB_DMA_BUFS, dev), (void *)size), dmajbuf);

return dma_buf;

void ldv_usb_dma_buf_free(struct usb_device *dev, size_t size , void *dma_buf, dma_addr_t *dma) { if (!dev || !dma_buf) { return NULL;

}

remove(get(get{LDV_USB_DMA_BUFS, dev), (void *)size), dma_buf) ; if (isEmpty(get(get(LDV_USB_DMA_BUFS, dev), (void *)size))) { remove(get(LDV_USB_DMA_BUFS, dev), (void *)size);

}

if (isEmpty(get(LDV_USB_DMA_BUFS, dev))) { remove (LDV_USB_DMA_BUFS, dev);

}

}

Множества точек использования элементов программного интерфейса.

pointcut USB_DMA_BUF_ALLOC: call(void *usb_alloc_coherent

(struct usb_device *, size_t, gfp_t, dma_addr_t *)) pointcut USB_DMA_BUF_FREE: call(void usb_free_coherent (struct usb_device *, size_t, void *, dma_addr_t))

Привязка модельных функций к точкам использования элементов программного интерфейса.

around: USB_DMA_BUF_ALLOC {

return ldv_usb_dma_buf_alloc($argl, $arg2, $arg3);

}

around: USB_DMA_BUF_FREE {

ldv_usb_dma_buf_free($argl, $arg2, $arg3, $arg4);

}

Предусловия использования элементов программного интерфейса.

before: USB_DMA_BUF_FREE {

ldv_assert(containsKey(LDV_USB_DMA_BUFS, $argl)

&& containsKey (get (LDV_USB_DMA__BUFS, $argl) , (void *)$arg2) && contains(get(get{LDV_USB_DMA_BUFS, $argl), (void *)$arg2), $arg3));

after: MODULE_EXIT {

ldv_assert(isEmpty(LDV_USB_DMA_BUFS)) ;

}

A.1.3 URB для контроллеров USB-шин

Известные нарушения: 2ffacal, a5cd44e.

Описание элементов программного интерфейса.

URB добавляется в очередь контроллера USB-шины с помощью функции int usbjicdJinkjurbjo_ep(struct usbjicd *, struct urb *) (с версии 2.6.35), если ей в качестве первого и второго фактических параметров передаются указатель на структуру контроллера USB-шины и указатель на структуру URB. Если URB удается добавить в очередь контроллера USB-шины, то usbjicdJinkjirbJo_ер возвращает 0. Иначе usbjicd Jinkjirb Jo _ер возвращает код ошибки.

Функция int usbjicd_check_unlink_urb(struct usbjtcd * struct urb *, int) (c версии 2.6.35) проверяет наличие URB в очереди контроллера USB-шины, если ей в качестве первого и второго фактических параметров передаются указатель на структуру контроллера USB-шины и указатель на структуру URB. Если URB был добавлен в очередь контроллера USB-шины, то usbjicd_check_unlink_urb возвращает 0. Иначе usbjicdJinkjirbjo_ep возвращает код ошибки.

URB удаляется из очереди контроллера USB-шины с помощью функции void usbjicdjtnlinkjurb_from_ep(struct usbjicd *, struct urb *) (с версии 2.6.35), если ей в качестве первого и второго фактических параметров передаются передается указатель на структуру контроллера USB-шины и указатель на структуру URB.

Правила корректного использования элементов программного интерфейса.

В процессе работы модулю запрещается удалять из очереди недобавленные им URB для контроллеров USB-шин, повторно добавлять в очередь URB для контроллеров USB-шин без предшествующего удаления и

повторно удалять из очереди одни и те же URB для контроллеров USB-шин.

На момент завершения работы модуль должен удалить из очереди все добавленные им URB для всех контроллеров USB-шин. Модельные переменные и модельные функции.

#include <linux/usb/hcd.h> #include <verifier/rcv.h>

Map LDV_USB_HCD_URBS = EmptyMap;

int ldv_usb_hcd_urb_link(stmct usb_hcd *hcd, struct urb *urb) { if (ldv_undef_int() {

return ldv_undef_int_negative() ;

}

if (icontainsKey(LDV_USB_HCD_URBS, hcd)) { put(LDV_U3B_HCD_URBS, hcd, EmptySet);

}

add(get(LDV_USB_HCD_URBS, hcd), urb); return 0;

}

int 1dv_usb_hcd_urb_is_linked(struct usb_hcd *hcd, struct urb *urb) { if (containsKey(LDV_USB_HCD_URBS, hcd)

&& contains(get(LDV_USB_HCD_URBS, hcd), urb) { return 0;

}

return ldv_undef_int_negative();

}

void 1dv_usb_hcd_urb_unlink(struct usb_hcd *hcd, struct urb *urb) { remove(get(LDV_USB_HCD_URBS, hcd), urb); if (isEmpty(get(LDV_USB_HCD_URBS, hcd))) { remove (LDV_USB_HCD_URBS, hcd);

}

}

Множества точек использования элементов программного интерфейса.

pointcut USB_HCD_URB_LINK:

call(int usb_hcd_link_urb_to_ep(struct usb__hcd *, struct urb *))

pointcut USB_flCD_URB_IS_LINKED:

call(int usb_hcd_check_unlink_urb(struct usb_hcd *, struct urb *, int))

pointcut USB_flCD_URB_UNLINK:

call(void usb_hcd_unlink_urb_from_ep(struet usb_hcd *, struct urb *))

Привязка модельных функций к точкам использования элементов программного интерфейса.

around: USB_HCD_URB_LINK {

return ldv_usb_hcd_urb_link($argl, $arg2);

}

around: USB_HCD_URB_IS_LINKED {

return 1dv_usb_hcd_urb_is_linked($argl, $arg2);

}

around: USB_HCD_URB_UNLINK {

ldv_usb_hcd_urb_unlink($argl, $arg2);

}

Предусловия использования элементов программного интерфейса.

before: USB_HCD_URB_LINK {

ldv_assert(!containsKey(LDV_USB_HCD_URBS, $argl)

|| ! contains (get (LDV_USB__HCD_URBS, $argl) , $arg2));

}

before: USB_HCD_URB_UNLINK {

ldv_assert(containsKey(LDV_USB_HCD_URBS, $argl)

&& contains(get(LDV_USB_HCD_URBS, $argl), $arg2));

}

after: MODULE_EXIT {

ldv_assert (isEmpty (LDV_USB_HCD_URB3)) ;

}

A.1.4 Счетчики ссылок трансиверов USB On-the-Go

Известные нарушения: 5b6ebed.

Описание элементов программного интерфейса.

Трансивер USB On-the-Go устанавливается с помощью функции int otg_set_transceiver(struct otgjransceiver *). В случае успеха otg_set_transceiver возвращает 0. Иначе otg_set_transceiver возвращает -EBUSY.

Счетчик ссылок для трансивера USB On-the-Go увеличивается с помощью функций struct otg_transceiver *otg_getJransceiver(void) и static inline struct otg_transceiver *otg_getJransceiver(void) (с версии 2.6.37 при выключенной опции CONFIGJJSBJDTGJJTILS). otg_get_transceiver возвращает указатель на структуру трансивера USB On-the-Go, который был установлен в настоящий момент. Если возвращаемое значение равно нулю, в текущий момент трансивер USB On-the-Go не доступен и счетчик ссылок для него не увеличивался.

Счетчик ссылок для трансивера USB On-the-Go уменьшается с помощью функций void otg_putJransceiver(struct otgjransceiver *) и static inline void otg_puttransceiver (struct otgjransceiver *) (с версии 2.6.37 при выключенной опции CONFIGJfSB OTGJJTILS), если ей в качестве фактического параметра передается ненулевой указатель на структуру трансивера USB On-the-Go.

Правила корректного использования элементов программного интерфейса.

В процессе работы модулю запрещается уменьшать счетчики ссылок для трансиверов USB On-the-Go настолько, что они станут меньше своих начальных значений.

На момент завершения работы модуль должен уменьшить счетчики ссылок для каждого трансивера USB On-the-Go ровно столько раз, сколько он их увеличивал.

Модельные переменные и модельные функции.

ttinclude <linux/usb/otg.h>

#include <verifier/rcv.h>

Map LDV_USB_OTG_TRANSIVER_REF_COUNTS = EmptyMap;

struct otg__transceiver *LDV_USB_OTG_TRANSIVER = NULL;

int ldv_usb_otg_transiver_set(struct otg_transceiver *x) { if (X && (LDV_USB_OTG_TRANSIVER || ldv_undef_int())) {

return -EBUSY;

LDV_USB_OTG_TRANSIVER = x; return 0;

}

struct otg_transceiver *ldv_usb__otg_transiver_ref_count_increment(void) { if (!LDV_USB_OTG_TRANSIVER) { return NULL;

}

if (containsKey(LDV_USB_OTG_TRANSIVER_REF_COUNTS , LDV_USB_OTG_TRANSIVER) ) { put (LDV_USB_OTG_TRANSIVER_REF_COUNTS, LDV_USB_OTG_TRANSIVER , get (LDV_USB_OTG_TRANSIVER_REF_COUNTS) +1); } else {

put (LDV_USB_OTG__TRANS IVER_REF_COUNTS, LDV_USB_OTG_TRANSIVER, 1) ;

}

return LDV_USB_OTG_TRANSIVER;

}

void 1 dv_usb_otg_transi ver_ref_coun t_decremen t (struct otg_transceiver *x) { if (ix) { return;

}

if (get (LDV_USB_OTG_TRANSIVER_REF_COUNTS, x) > 1) { put (LDV_USB_OTG_TRANSIVER_REF_COUNTS, x

, get (LDV_USB_OTG_TRANSIVER_REF_COUNTS, x) -1); } else {

remove (LDV_USB_OTG_TRANSIVER_REF_COUNTS, x)

}

}

Множества точек использования элементов программного интерфейса.

pointcut USB_OTG_TRANSIVER_SET: