Генерация модели окружения для группы модулей ядра для статической верификации (Илья Захаров, OSSDEVCONF-2013) — различия между версиями
Материал из 0x1.tv
StasFomin (обсуждение | вклад) |
StasFomin (обсуждение | вклад) () |
||
== Видео ==
{{vimeoembed|75430925|800|500}}
{{youtubelink|dvbyV_FG2E8}}
<poll>
ALTERNATIVE
REVOTE
UNIQUE
Оцените доклад «{{PAGENAME}}»:
Отлично!
Хорошо.
Нормально…
Не очень :(
Просто хочу узнать результаты.
</poll-- pollholder -->
== Слайды ==
[[File:Генерация модели окружения для группы модулей ядра для статической верификации (Илья Захаров, OSSDEVCONF-2013).pdf|left|page=-|256px]]
{{----}}
== Примечания и отзывы ==
<!-- <blockquote>[©]</blockquote> -->
<references/>
[[Category:OSSDEVCONF-2013]]
[[Category:Open-source]]
[[Category:Верификация]]
<noinclude>[[Category:ToPublish]]</noinclude>
<!-- topub --> | |||
Версия 17:55, 16 июля 2015
Содержание
Аннотация
- Докладчик
- Илья Захаров
Система верификации LDV нацелена на проверку правил корректности использования интерфейсов ядра Linux драйверами при помощи инструментов статической верификации. Одновременно анализировать драйвер вместе с сердцевиной ядра затруднительно для существующих инструментов верификации из-за большого объема и сложности кода такой системы. Для верификации одного модуля ядра в системе LDV генерируется модель окружения, вместе с которой драйвер анализируется инструментом верификации.
В случае взаимосвязанной группы модулей анализ каждого модуля отдельно от остальных приводит к использованию неполной и некорректной модели окружения и получению неверных результатов верификации.
Доклад описывает новый подход к верификации групп модулей ядра, который включает в себя выделение взаимосвязанных групп модулей, генерацию модели окружения для групп и их верификацию.
Видео
Слайды
