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

== Видео ==

{{vimeoembed|75430925|800|500}}
{{youtubelink|dvbyV_FG2E8}}

<poll>
ALTERNATIVE
REVOTE
UNIQUE
Оцените доклад «{{PAGENAME}}»:
Отлично!
Хорошо.
Нормально…
Не очень :(
Просто хочу узнать результаты.
</poll>

{{letscomment}}
<!-- pollholder --> 
== Слайды ==
[[File:Генерация модели окружения для группы модулей ядра для статической верификации (Илья Захаров, OSSDEVCONF-2013).pdf|left|page=-|256px]]

{{----}}

== Примечания и отзывы ==
<!-- <blockquote>[©]</blockquote> -->

<references/>

[[Category:OSSDEVCONF-2013]]
[[Category:Open-source projects]]
<noinclude>[[Category:ToPublishВерификация]]</noinclude>

<!-- topub -->
{{stats|disqus_comments=0|refresh_time=2021-08-31T16:57:01.849499|vimeo_comments=0|vimeo_plays=24|youtube_comments=0|youtube_plays=10}}

Текущая версия на 12:20, 4 сентября 2021

Аннотация

Докладчик

Илья Захаров

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

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

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

Видео

Слайды

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

Plays:34   Comments:0