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

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

Версия от 14:59, 18 июня 2016; StasFomin (обсуждение | вклад) (Batch edit: replace :Open-source]] with :Open-source projects]])

Аннотация

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

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

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

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

Видео

on youtube







Слайды

Генерация модели окружения для группы модулей ядра для статической верификации (Илья Захаров, 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

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