LINUX.ORG.RU

Архитектура системы верификации кода драйверов Linux

 , ,


0

2

В статье "Архитектура Linux Driver Verification" (PDF, 700 Кб) представлено описание применимости метода статического анализа кода для проверки корректности драйверов устройств для платформы Linux. Представленный метод позволяет выявить ошибки на основании анализа исходных текстов, без непосредственного выполнения кода. В отличие от традиционных методов тестирования статический анализ кода позволяет проследить сразу все пути выполнения программы, в том числе, редко встречающиеся и сложно воспроизводимые при динамическом тестировании.

Проект Linux Driver Verification является открытым и развивается при участии организации Linux Foundation, Института системного программирования Российской Академии Наук (ИСП РАН) и Федерального агентства РФ по науке и инновациям. Наработки проекта распространяются в рамках лицензии Apache. Дополнительно подготовлен online-сервис для проверки драйверов. Список выявленных при помощи LDV проблем можно посмотреть на данной странице.

>>> Источник

★★★★★

Проверено: Shaman007 ()
Последнее исправление: Manhunt (всего исправлений: 1)

Ответ на: комментарий от Manhunt

> Пользовались. Вот ссылка, не будь совсем уж Ъ

Не петросянь. Я спрашиваю о том, есть ли на ЛОР живые юзеры этого LDV.

tailgunner ★★★★★
()
Ответ на: комментарий от tailgunner

игрушка, кхм, как ты ее назвал, там, скорее, бласт — http://mtc.epfl.ch/software-tools/blast/index-epfl.php

а они, как мне показалось при чтении по диагонали, его подзаточили под ядро

кстати — емнип один из них тут имеет аккаунт на лоре, и даже че-то рассказывал, когда речь шла о емнип http://linuxtesting.ru/project/lsb_infrastructure

www_linux_org_ru ★★★★★
()
Ответ на: комментарий от www_linux_org_ru

> игрушка, кхм, как ты ее назвал, там, скорее, бласт — http://mtc.epfl.ch/software-tools/blast/index-epfl.php

У них на странице прямо так и написано. Но мне интересно использование LDV для своих драйверов или Си-программ.

tailgunner ★★★★★
()
Ответ на: комментарий от tailgunner

раз его скастовали сюда, наверно можно и второй раз скастовать

а вообще я сомневаюсь, что тут на лоре кроме тебя кто-то из драйверописателей интересуется формальной верификацией

www_linux_org_ru ★★★★★
()

Статистически анализ не надежен - какой прок в прогнозе что код с вероятностью NN правильный. А ведь надо еще доказать применимость статистических гипотез к конкретному коду.

anonymous
()
Ответ на: комментарий от tailgunner

насколько я понимаю, да

ладно, я прекращаю выступать в роли К.О., интересней почитать, че они там накрутили

www_linux_org_ru ★★★★★
()
Ответ на: комментарий от anonymous

> какой прок в прогнозе что код с вероятностью NN правильный

Никакого. Применение статистических методов не отменяет классического тестирования. Но хуже-то тоже не будет.

Aceler ★★★★★
()

> (ИСП РАН) и Федерального агентства РФ по науке и инновациям

инновациям


Превед Медвед?

self-learningMACHINE
()
Ответ на: комментарий от anonymous

> Статистически анализ не надежен - какой прок в прогнозе что код с вероятностью NN правильный. А ведь надо еще доказать применимость статистических гипотез к конкретному коду

ты где там нашел статистические методы?

www_linux_org_ru ★★★★★
()

>Список выявленных при помощи LDV проблем можно посмотреть на данной странице.

Я не понял - три десятка багов за 2 года? Это драйвера такие хорошие или инструмент....?

r ★★★★★
()
Ответ на: комментарий от www_linux_org_ru

Хы, я тоже написал «статистического» :)

Aceler ★★★★★
()
Ответ на: комментарий от dizza

> Как мне кажется, все эти версификаторы направлены на компенсацию убогости С\С++

после того, как доказан какой-то инвариант, например, что индекс не выходит за границы массива, можно (и нужно) нафиг выкинуть код, проверяющий это в рантайме, и тем ускорить исполнение

www_linux_org_ru ★★★★★
()
Ответ на: комментарий от www_linux_org_ru

кроме того, можно не заставлять программиста тратить время — писать код обработки для ситуации, которая доказанно возникнуть не может

хотя, тут, не все так просто

www_linux_org_ru ★★★★★
()
Ответ на: комментарий от www_linux_org_ru

Ну какие проблемы, вон, некоторые жаве проверки отключают на проде. Все равно такие фичи должны быть встроены в язык.

dizza ★★★★★
()
Ответ на: комментарий от dizza

> Как мне кажется, все эти версификаторы направлены на компенсацию убогости С\С++

Как это ложится на проверки зависимостей? Когда что-то нужно сделать обязательно только после чего-то дрогого. Они, очень часто, чисто логические.

x86_64 ★★★
()

Институт РАН сделал что-то полезное, да к тому же для линукса?

Ущипните меня.

anonymous
()
Ответ на: комментарий от x86_64

Ну и? Я за то, что бы системы верификации была частью языка, а не костылем. Чем язык лучше, тем у него больше встроенных средств обеспечения корректности. Хаскель, который тут любят - только цветочки.

dizza ★★★★★
()
Ответ на: комментарий от tailgunner

Внезапно: ходил по ссылкам в теме, почитал их сайт. Они там нечто похожее на юнит-тесты на libc написали. Цирк.

dizza ★★★★★
()
Ответ на: комментарий от dizza

> Ну какие проблемы, вон, некоторые жаве проверки отключают на проде. Все равно такие фичи должны быть встроены в язык.

Какие? Вызов метода/функции xxx обязательно делать только после вызова метода/функции yyy или метода/функции ййй? :)

x86_64 ★★★
()
Ответ на: комментарий от x86_64

>> Все равно такие фичи должны быть встроены в язык.

Какие? Вызов метода/функции xxx обязательно делать только после вызова метода/функции yyy или метода/функции ййй? :)

Почему нет?

tailgunner ★★★★★
()
Ответ на: комментарий от dizza

> Внезапно: ходил по ссылкам в теме, почитал их сайт. Они там нечто похожее на юнит-тесты на libc написали. Цирк.

Походу, ты не совсем врубаешься. Юнит тесты - это ЧАСТЬ кода, работающая в коде предназначеном для тестирования.

Здесь ВЕСЬ код драйверов прокручивается на поиск противоречий в специальной среде, эти противоречия выявляющей.

x86_64 ★★★
()
Ответ на: комментарий от tailgunner

>>> Все равно такие фичи должны быть встроены в язык.

Какие? Вызов метода/функции xxx обязательно делать только после вызова метода/функции yyy или метода/функции ййй? :)

Почему нет?

Потому что это только примитивнейшая зависимость. Можно, конечно, такие зависимости и более сложные в язык запихнуть, но только нет таких языков и не будет. Ибо для записи таких зависимостей нужен совсем другой язык, более для этого подходящий.

x86_64 ★★★
()
Ответ на: комментарий от x86_64

Не, мы про спецификации разного уровня говорим. Я вот высмеиваю верификаторы низкоуровневых спецификаций, вроде запрета на выход за границы массива.

dizza ★★★★★
()
Ответ на: комментарий от www_linux_org_ru

> после того, как доказан какой-то инвариант, например, что индекс не выходит за границы массива, можно (и нужно) нафиг выкинуть код, проверяющий это в рантайме, и тем ускорить исполнение

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

vovic
()
Ответ на: комментарий от dizza

> Не, мы про спецификации разного уровня говорим. Я вот высмеиваю верификаторы низкоуровневых спецификаций, вроде запрета на выход за границы массива.

В одних языках надо одно проверять. В других - другое. В общем объеме необходимых проверок - это ничего не значащая величина.

x86_64 ★★★
()
Ответ на: комментарий от vovic

> то и рантаймовую проверку выкидывать нельзя.

Вообще-то, если среда не меняется в процессе работы, то можно. Вынести эти проверки на этап инициализации...

x86_64 ★★★
()
Ответ на: комментарий от x86_64

>> то и рантаймовую проверку выкидывать нельзя.

Вообще-то, если среда не меняется в процессе работы, то можно. Вынести эти проверки на этап инициализации...

От выноса проверки из цикла быть рантаймовой она не перестанет.

Кроме того, это тоже должен по-хорошему должны делать и внимательный программист, и компилятор. При чём здесь формальные верификаторы мне не понятно.

vovic
()
Ответ на: комментарий от vovic

>>> то и рантаймовую проверку выкидывать нельзя.

Вообще-то, если среда не меняется в процессе работы, то можно. Вынести эти проверки на этап инициализации...

От выноса проверки из цикла быть рантаймовой она не перестанет.

Только это будет уже на рантайм-проерка выхода за границы массива а рантайм-проверка на допустимост параметров системы.

Кроме того, это тоже должен по-хорошему должны делать и внимательный программист, и компилятор. При чём здесь формальные верификаторы мне не понятно.

Вот внимательность программиста и проверяется.

x86_64 ★★★
()
Ответ на: комментарий от vovic

> это тоже должен по-хорошему должны делать и внимательный программист, и компилятор

Особенно убедительно выглядит про «внимательного программиста».

При чём здесь формальные верификаторы мне не понятно.

При том, что компилятор тоже может выполнять верификацию, и, следовательно, быть верификатором.

tailgunner ★★★★★
()
Ответ на: комментарий от x86_64

> Только это будет уже на рантайм-проерка выхода за границы массива а рантайм-проверка на допустимост параметров системы.

Это будет рантайм-проверка на то, выйдет ли указатель, по которому осуществляется доступ, за границы массива. То есть, по мне она так и останется «рантайм-проверкой на выход за границы массива», просто станет более умной. :-) В любом случае, это уже проблемы терминологии.

Кроме того, это тоже должен по-хорошему должны делать и внимательный программист, и компилятор. При чём здесь формальные верификаторы мне не понятно.

Вот внимательность программиста и проверяется.

Вы про что? Кем проверяется? И на каком этапе - статически или в рантайме?

vovic
()
Ответ на: комментарий от tailgunner

> При том, что компилятор тоже может выполнять верификацию, и, следовательно, быть верификатором.

Согласен. Более того, этот «верификатор»-компилятор сам стремится исправить код на более оптимальный. Но в такой формулировке верификаторами пользуются все, кто компилирует с ключом -O, отличным от нуля. Речь ведь изначально шла про верификацию во время исполнения кода, а не статическими средствами, не?

vovic
()
Ответ на: комментарий от vovic

> в такой формулировке верификаторами пользуются все, кто компилирует с ключом -O, отличным от нуля

Простым, нерасширяемым верификатором.

Речь ведь изначально шла про верификацию во время исполнения кода

Видимо, я пропустил момент, когда разговор о статической верификации перешел в разговор о динамической (более того, я впервые слышу о «динамической верификации» %)).

tailgunner ★★★★★
()

<вброс>

Линукс - ре-ше-то :)

</вброс>

rtvd ★★★★★
()
Ответ на: комментарий от tailgunner

>> в такой формулировке верификаторами пользуются все, кто компилирует с ключом -O, отличным от нуля

Простым, нерасширяемым верификатором.

Хм... вот насчет нерасширяемости - теперь не верно. Теперь же можно скрипты на питоне писать для gcc. С доступом ко внутренним структурам. Теоритически туда любые проверки запихать можно.

x86_64 ★★★
()

А кто-нибудь уже нашел, где у них собственно список проверяемых правил?

tailgunner ★★★★★
()
Ответ на: комментарий от x86_64

> вот насчет нерасширяемости - теперь не верно.

Всё еще верно.

Теперь же можно скрипты на питоне писать для gcc

Это уже не компилятор, а чекер на основе компиляторного промежуточного представления.

tailgunner ★★★★★
()
Ответ на: комментарий от tailgunner

> Видимо, я пропустил момент, когда разговор о статической верификации перешел в разговор о динамической (более того, я впервые слышу о «динамической верификации» %)).

Статью из новости я, естественно, не читал, однако если правильно помню, их система верификации именно динамическая, по крайней мере, как я бы её назвал (хотя честно признаю, что в этом не разбираюсь): Код драйвера «чистится» от «ядерных» особенностей, инструментируется проверками на блокировки/разблокировки/что ещё они там проверяют, для полученного кода строится набор тестов, покрывающий все возможные варианты его работы, после чего «вычищенный» и инструментированный драйвер (т.е. уже по сути дела не драйвер, а инструментированный чекер с идентичной структурой кода) запускается на всех этих тестах. Раз код (пусть и модифицированный) запускается и вставленные проверки осуществляются во время исполнения - значит, динамическая(рантаймовая) верификация.

Поправьте, что не так.

vovic
()
Вы не можете добавлять комментарии в эту тему. Тема перемещена в архив.