Генерация модели окружения для группы модулей ядра для статической верификации (Илья Захаров, OSSDEVCONF-2013) — различия между версиями
Материал из 0x1.tv
StasFomin (обсуждение | вклад) (→Видео) |
StasFomin (обсуждение | вклад) (Batch edit: add <!-- topub -->) |
||
== Примечания и отзывы ==
<!-- <blockquote>[©]</blockquote> -->
<references/>
[[Category:OSSDEVCONF-2013]]
[[Category:Open-source]]
<noinclude>[[Category:ToPublish]]</noinclude>
<!-- topub --> |
Версия 23:21, 9 ноября 2014
Содержание
Аннотация
- Докладчик
- Илья Захаров
Система верификации LDV нацелена на проверку правил корректности использования интерфейсов ядра Linux драйверами при помощи инструментов статической верификации. Одновременно анализировать драйвер вместе с сердцевиной ядра затруднительно для существующих инструментов верификации из-за большого объема и сложности кода такой системы. Для верификации одного модуля ядра в системе LDV генерируется модель окружения, вместе с которой драйвер анализируется инструментом верификации.
В случае взаимосвязанной группы модулей анализ каждого модуля отдельно от остальных приводит к использованию неполной и некорректной модели окружения и получению неверных результатов верификации.
Доклад описывает новый подход к верификации групп модулей ядра, который включает в себя выделение взаимосвязанных групп модулей, генерацию модели окружения для групп и их верификацию.
Видео