Генерация модели окружения для группы модулей ядра для статической верификации (Илья Захаров, OSSDEVCONF-2013)

Материал из 0x1.tv

Аннотация

Докладчик
Илья Захаров.jpg
Илья Захаров

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

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

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

Видео

on youtube

Оцените доклад «Генерация модели окружения для группы модулей ядра для статической верификации (Илья Захаров, OSSDEVCONF-2013)»:

  •  Отлично!
  •  Хорошо.
  •  Нормально…
  •  Не очень :(
  •  Просто хочу узнать результаты.

Слайды

Генерация модели окружения для группы модулей ядра для статической верификации (Илья Захаров, OSSDEVCONF-2013).pdf Генерация модели окружения для группы модулей ядра для статической верификации (Илья Захаров, OSSDEVCONF-2013).pdf Генерация модели окружения для группы модулей ядра для статической верификации (Илья Захаров, OSSDEVCONF-2013).pdf Генерация модели окружения для группы модулей ядра для статической верификации (Илья Захаров, OSSDEVCONF-2013).pdf Генерация модели окружения для группы модулей ядра для статической верификации (Илья Захаров, OSSDEVCONF-2013).pdf Генерация модели окружения для группы модулей ядра для статической верификации (Илья Захаров, OSSDEVCONF-2013).pdf Генерация модели окружения для группы модулей ядра для статической верификации (Илья Захаров, OSSDEVCONF-2013).pdf Генерация модели окружения для группы модулей ядра для статической верификации (Илья Захаров, OSSDEVCONF-2013).pdf Генерация модели окружения для группы модулей ядра для статической верификации (Илья Захаров, OSSDEVCONF-2013).pdf Генерация модели окружения для группы модулей ядра для статической верификации (Илья Захаров, OSSDEVCONF-2013).pdf Генерация модели окружения для группы модулей ядра для статической верификации (Илья Захаров, OSSDEVCONF-2013).pdf Генерация модели окружения для группы модулей ядра для статической верификации (Илья Захаров, OSSDEVCONF-2013).pdf Генерация модели окружения для группы модулей ядра для статической верификации (Илья Захаров, OSSDEVCONF-2013).pdf Генерация модели окружения для группы модулей ядра для статической верификации (Илья Захаров, OSSDEVCONF-2013).pdf Генерация модели окружения для группы модулей ядра для статической верификации (Илья Захаров, OSSDEVCONF-2013).pdf Генерация модели окружения для группы модулей ядра для статической верификации (Илья Захаров, OSSDEVCONF-2013).pdf Генерация модели окружения для группы модулей ядра для статической верификации (Илья Захаров, OSSDEVCONF-2013).pdf Генерация модели окружения для группы модулей ядра для статической верификации (Илья Захаров, OSSDEVCONF-2013).pdf Генерация модели окружения для группы модулей ядра для статической верификации (Илья Захаров, OSSDEVCONF-2013).pdf Генерация модели окружения для группы модулей ядра для статической верификации (Илья Захаров, OSSDEVCONF-2013).pdf Генерация модели окружения для группы модулей ядра для статической верификации (Илья Захаров, OSSDEVCONF-2013).pdf Генерация модели окружения для группы модулей ядра для статической верификации (Илья Захаров, OSSDEVCONF-2013).pdf Генерация модели окружения для группы модулей ядра для статической верификации (Илья Захаров, OSSDEVCONF-2013).pdf Генерация модели окружения для группы модулей ядра для статической верификации (Илья Захаров, OSSDEVCONF-2013).pdf Генерация модели окружения для группы модулей ядра для статической верификации (Илья Захаров, OSSDEVCONF-2013).pdf Генерация модели окружения для группы модулей ядра для статической верификации (Илья Захаров, OSSDEVCONF-2013).pdf Генерация модели окружения для группы модулей ядра для статической верификации (Илья Захаров, OSSDEVCONF-2013).pdf Генерация модели окружения для группы модулей ядра для статической верификации (Илья Захаров, OSSDEVCONF-2013).pdf

Примечания и отзывы