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

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

(Batch edit: replace PCRE \{\{youtubelink\|([^\}]*)\}\} with {{youtubelink|\1}}{{letscomment}})
 
== Примечания и отзывы ==
<!-- <blockquote>[©]</blockquote> -->

<references/>

[[Category:OSSDEVCONF-2013]]
[[Category:Open-source projects]]
[[Category:Верификация]]

<!-- topub -->
{{stats|disqus_comments=0|refresh_time=2018-10-11T0019T21:3145:53.365921290257|vimeo_comments=0|vimeo_plays=24|youtube_comments=0|youtube_plays=10}}

Версия 18:45, 19 октября 2018

Аннотация

Докладчик
Илья Захаров.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

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


Plays:34   Comments:0

Источник — «https://0x1.tv/index.php?title=Генерация_модели_окружения_для_группы_модулей_ядра_для_статической_верификации_(Илья_Захаров,_OSSDEVCONF-2013)&oldid=99003»