Новости

Сотрудники Центра верификации ОС Linux Евгений Шатохин и Алексей Хорошилов представили на конференции LinuxCon Europe 2011, проходившей с 26 по 28 октября 2011 года в городе Прага, Чехия, текущие достижения проектов по улучшению качества модулей ядра ОС Linux, ведущихся в Центре верификации.

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

Слайды выступлений доступны в разделе Публикации:

• Евгений Шатохин. "Использование динамического анализа для выявления проблем в модулях ядра" .
• Алексей Хорошилов. "Верификация драйверов устройств с помощью Linux Driver Verification" .

Центр верификации ОС Linux приглашает всех заинтересованых лиц посетить наш стенд на выставке SofTool 2011, которая пройдет 25-28 октября 2011 года в 69 павильоне ВВЦ. Наши разработки будут представлены в рамках объединенной экспозиции Российской Академии Наук на стенде E47.

Центр верификации Linux опубликовал новую версию свободного инструмента верификации BLAST 2.7, который автоматически анализирует Си-программы на предмет нарушения заданных правил корректности посредством реализации метода итеративного уточнения абстракции программы на основе контр-примеров CEGAR.

Версия BLAST 2.7 стала результатом улучшений, внесённых специалистами Центра верификации Linux в BLAST 2.6 в рамках программы Linux Driver Verification , а также в рамках подготовки к Competition on Software Verification, которое состоится в рамках конференции TACAS'12.

Основные улучшения коснулись следующих направлений.

Центр верификации Linux опубликовал новую версию свободного инструмента верификации BLAST 2.6, который автоматически анализирует Си-программы на предмет нарушения заданных правил корректности посредством реализации метода итеративного уточнения абстракции программы на основе контр-примеров CEGAR.

Версия BLAST 2.6 стала результатом улучшений, внесённых специалистами Центра верификации Linux в рамках программы Linux Driver Verification в версию BLAST 2.5, которая была разработана командой европейских и американских учёных и развитие которой приостановилось в середине 2008 года.

Основные улучшения коснулись следующих направлений.

Выпущена версия 0.3 системы KEDR, предназначенной для runtime-анализа модулей ядра Linux, в том числе драйверов устройств, модулей файловых систем и т.д. Инструменты из состава KEDR работают с модулем ядра, выбранным пользователем. Они позволяют отслеживать вызовы функций данным модулем и сохранять информацию о них в файле ("трасса вызовов"), имитировать нехватку системных ресурсов, выявлять утечки памяти.

Наиболее важные изменения в этой версии (подробная информация - в ChangeLog):

Выпущена версия 0.2 системы KEDR, предназначенной для runtime-анализа модулей ядра Linux, в том числе драйверов устройств, модулей файловых систем и т.д. Инструменты из состава KEDR позволяют отслеживать вызовы функций из модуля, выбранного пользователем, и сохранять информацию о них в файле ("трасса вызовов"), имитировать нехватку системных ресурсов, выявлять утечки памяти.

В версии 0.2 несколько компонентов KEDR были переработаны, а также были исправлены различные ошибки.

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

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

При поддержке The Linux Foundation мы приняли участие в Google Summer of Code 2010 с проектом "Linux Device Drivers Quality Inspector". В рамках этого проекта студент МФТИ Андрей Третьяков под руководством Алексея Хорошилова разработал инфраструктуру для отслеживания изменений в git репозитории ядра с тем, чтобы инструменты LDV проверяли только те драйвера устройств, в которые могли быть внесены ошибки после предыдущей проверки.

Выпущена очередная версия тестов OLVER Core 1.5 с улучшенными отчётами о результатах тестирования и расширенным тестовым покрытием. См. детальный список изменений ниже.

Используйте следующие сссылки для просмотра текущих результатов проекта:

• систематизированный каталог требований LSB Core 3.1 для всех 1532 архитектурно независимых функций LSB Core 3.1;
• формальные спецификации в базовом качестве для 1450 функций LSB Core 3.1;
• формальные спецификации в минимальном качестве для 80 функций LSB Core 3.1;
• список выявленных сотрудниками Центра проблемных мест в тексте стандарта LSB Core 3.1 и связанного с ним стандарта POSIX;
• демонстрационные примеры исполняемых тестов для избранных групп функций с аннотированными примерами, позволяющие разобраться в используемой технологии и архитектуре тестового набора;
• бинарные и исходные коды разрабатываемого тестового набора OLVER. На данный момент в набор включены тесты для 1530 функций (см. список спецификаций онлайн).

Центр верификации ОС Linux объявляет о публичной доступности нового инструмента для тестирования бинарной совместимости различных версий динамических библиотек - ABI Compliance Checker. Инструмент позволяет обнаружить изменения в публичном интерфейсе библиотеки, которые могут привести к некорректной работе приложений после её обновления. Важным отличием инструмента от существующих аналогов является детальный анализ типов параметров экспортируемых функций на основе разбора заголовочных файлов библиотеки. Мы рекомендуем ABI Compliance Checker разработчикам библиотек и инженерам сопровождения дистрибутивов, которые заинтересованы в предоставлении своим пользователям стабильного бинарного интерфейса.