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

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

некоторые?

отключать надо не некоторые, а только те, что доказано не нужны

третий раз повторять не буду

> Код драйвера «чистится» от «ядерных» особенностей, инструментируется проверками на блокировки/разблокировки/что ещё они там проверяют

Да.

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

Нет.

Раз код (пусть и модифицированный) запускается

Он не запускается. В статье говорится, что инструментированный текст передается чисто статическим чекерам (собственно, запуск драйверного кода невозможен без устройства). Может, там в роли «запуска» выступает абстрактная интерпретация (это объяснило бы время, затрачиваемое на проверку), но это всё равно не является реальным запуском кода.

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

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

Почему?

Потому что правила проверки определяются не во входном языке, который воспринимается компилятором, а в чекере.

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

основной пойнт как раз на статической верификации

и «верификация во время исполнения кода» режет слух

> Он не запускается. В статье говорится, что инструментированный текст передается чисто статическим чекерам (собственно, запуск драйверного кода невозможен без устройства). Может, там в роли «запуска» выступает абстрактная интерпретация (это объяснило бы время, затрачиваемое на проверку), но это всё равно не является реальным запуском кода.

Ну я и написал, что он вроде как после преобразования в промежуточное представление чистится LDV от взаимодействия с ядром и железом. То есть, получается обычная самодостаточная программка с по-умному понатыканными LDV и BLAST-ом ассёртами, принимающая в качестве аргумента снова же абстрагированную последовательность событий/состояний железа/mutexов/переменных/итд, на которой вполне реально прогоняется. И так на всех последовательностях, которые LDV/BLAST считают достаточными для заключения о корректности работы. Собственно, я это и писал:

инструментированный драйвер (т.е. уже по сути дела не драйвер, а инструментированный чекер с идентичной структурой кода) запускается на всех этих тестах

Можно ли считать запуск «выпотрошенного» и инструментированного кода для проверки удовлетворения всем требованиям рантаймовой проверкой, имхо, дело терминологии (а корректную терминологию я не знаю). Я бы считал.

> запуск «выпотрошенного»

Еще раз - там нет запуска.

> Может, там в роли «запуска» выступает абстрактная интерпретация (это объяснило бы время, затрачиваемое на проверку)

бласт в качестве результата может выдать:

1. инвариант доказан

2. инваринат нарушается вот в таком execution path

3. работаю... вот такие-то execution path вроде бы дают нарушение инварианта, но х.з.

в п.3 он может работать бесконечно

> проверки определяются не во входном языке, который воспринимается компилятором, а в чекере

Что понимается под чекером? Если проверки на возможность проведения каких-то оптимизаций (о чём разговор шёл изначально, если я ещё правильно это помню), это делается в миддл-энде. Согласно http://gcc.gnu.org/onlinedocs/gccint/Plugins.html я понял, плагины в миддл-энд вставлять можно, т.е. как раз можно иметь возможность щупать внутреннее представление и делать на основании этого какие-то заключения. Правда, на C, насчёт Питона не знаю.

> Что понимается под чекером? Если проверки на возможность проведения каких-то оптимизаций (о чём разговор шёл изначально, если я ещё правильно это помню), это делается в миддл-энде

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

рассмотри просто проверку правильности программы

> Что понимается под чекером?

Код, проверяющий свойства программы.

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

с этим я согласен, но язык получается немного не похож на то, что сейчас привыкли считать языком

например, компилятор может работать сколь угодно большое время (пытаясь найти контрпример)

ну и наличие в компиляторе SMT-решателя тоже немного необычно

> но это всё равно не является реальным запуском кода.

да, бласт точно код не запускает — там можно описывать заглушки вместо функций, написанных на ассемблере (который бласт не понимает)

> Еще раз - там нет запуска.

Открываем статью с их сайта (http://www.sosy-lab.org/~dbeyer/Publications/2007-STTT.The_Software_Model_Che...), смотрим рис. 12. Анализатор Blasta анализирует код и выплёвывает набор входных векторов, которых по его мнению должно быть достаточно для вынесения вердикта о корректности программы. Затем эти вектора скармливаются изначальному коду, и происходит тестирование. В каком виде происходит тестирование методом прогона всех сгенерированных входов на исходной программе - на уровне абстрактного дерева или в бинарном виде - там я не нашёл, но нашёл это в статьего одного из (видимо) разработчиков http://goto.ucsd.edu/~rjhala/papers/jhala-thesis.pdf

The test-driver generator takes as input the original program and instruments it at the source-code level to create a test driver containing the following components: (1) a wrapping function, (2) a test-feeding function, and (3) a modied version of the original program. The test driver can then be compiled and run to examine the behavior of the original program on the test suite. It can be run on each individual test vector and the user can study the resulting dynamic behavior as she pleases, by using a debugger for example.

То есть, имеет место исполнение именно бинарного кода, что логично - так элементарно быстрее. Но даже если бы исполнение шло по абстрактному дереву - это по сути дела всё равно исполнение, т.к. код проходит те же состояния в том же порядке, что и в бинарном виде.

Где ошибаюсь?

> абстрактному дереву

абстрактному представлению

> Анализатор Blasta анализирует код и выплёвывает набор входных векторов

Да, BLAST умеет генерировать тесты. Что дальше?

Где ошибаюсь?

Твоя главная ошибка - в том, что ты не указал место _в сабжевой статье_, где говориться о выполнении кода, а гонишь какую-то нерелевантную пургу.

>> Твоя главная ошибка - в том, что ты не указал место _в сабжевой статье_, где говориться о выполнении кода, а гонишь какую-то нерелевантную пургу.

В настоящее время для целей тестирования и демонстрации возможностей

реализованы 2 обертки соответственно для верификаторов достижимости BLAST и CPAchecker.

То есть, если из LDV зовётся BLAST, то бласт релевантен. Если бласт релевантен, то моё предыдущее сообщение о том, что Blast «внутри себя» всё-таки (по крайней мере, согласно приведённой мной статье) исполняет бинарное представление кода (пусть и модифицированного) драйвера, также релевантно и доказывает правоту утверждения, что код в конечном счёте (внимание!) всё-таки исполняется. А в самой статье вообще мало чего говорится о внутренней структуре реализованной системы, там только общие слова.

говориться

говорится

Хотя на самом деле, чтобы избежать дальнейшей потери времени, предположу, что разногласие возникает из-за того, что исполнение Blast-ом «кастрированного» кода во время проверки корректности всех входов авторами статьи считается статическим, а не динамическим анализом. В то время, как я его назвал именно динамическим.

> Список выявленных при помощи LDV проблем

Они украли ник у ldv?

> Если бласт релевантен, то моё предыдущее сообщение о том, что Blast «внутри себя» всё-таки (по крайней мере, согласно приведённой мной статье) исполняет бинарное представление кода (пусть и модифицированного) драйвера, также релевантно

О как. Может, еще скажешь, как именно BLAST умудряется исполнять бинарный код драйвера устройства, не имея под собой устройства? %)

> О как. Может, еще скажешь, как именно BLAST умудряется исполнять бинарный код драйвера устройства, не имея под собой устройства? %)

Уже несколько раз сказал - исполнение _модифицированного_ кода в _модифицированном_ окружении. Уже без обращений к самому устройству. Да, и если ты до сих пор думаешь, что проверяется интерфейс доступа к самому физическому устройству - посмотри на список найденных с помощью тула багов и проверки, описанные в статье - там идёт исключительно работа с памятью, mutex-ы, проверки на несрабатывание assert-ов. То есть, чисто программные вещи. То, что драйвер это или нет - уже мало принципиально. Главная сложность - то, как очистить код от системной «шелухи».

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

> и если ты до сих пор думаешь, что проверяется интерфейс доступа к самому физическому устройству

Я так не думаю сейчас и не думал раньше.

А вообще посты ты не читаешь, позицию не аргументируешь,

Я внимательно читал твои посты и объяснял свою позицию, пока не понял, что столкнулся с уверенным в себе профаном.

пишешь мусор

Хотел сказать, что мусор у тебя в голове, но там пусто. Даже мусора нет.

не представляю - как это работает? принципиально

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

Что должен сделать язык со входными данными выходящими за диапазон? И устроит ли тебя его решение.

Видел авторов в прошлом году на софтуле, даже сфоткался с ними, колоритные чувачки )

Надо будет своих на работе пнуть, чтобы потестили самописный драйвер. С прошлого года как-то забыл. А тут такое напоминание )

> Надо будет своих на работе пнуть, чтобы потестили самописный драйвер.

И инструкцию по использованию опубликуй здесь :)

Язык должен предоставить возможность написать пред-условие, ну и гарантировать его выполнение.

>Язык должен предоставить возможность написать пред-условие, ну и гарантировать его выполнение.

Так уже есть давно, но не в питоне с жабой. Комбинация операторов if then begin end goto творит чудеса логики и обрабатывает любое количество условий и просто в коде и во вложенных циклах.

Ну я это юзаю как могу. Но хочется это более декларативно и в объявлении сигнатур а не внутри реализаций. А потом инварианты уже сильно сложнее запрограммировать.

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

>> Комбинация операторов if then begin end goto творит чудеса логики и обрабатывает любое количество условий

Ну я это юзаю как могу

Херасе.

Не ну не конкретно с goto, но да, предусловия очень часто пишу.

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

Ой, да ну, не, ну правда что-ли? Таки «торадиционные» средства не позволяют анализировать ветви?

Хорошая новость. Наконец-то.

A 3.6 Rule Instrumentor (LLVM)?

> A 3.6 Rule Instrumentor (LLVM)?

«Rule Instrumentor — компонент, основное назначение которого — связывать формализованные в виде моделей правила корректности с исходным кодом для последующей верификации». Насколько я понимаю, это просто аннотация исходников. В любом случае, об исполнении кода речи не идет (тот же BLAST - следующая стадия).

Можно ли считать запуск «выпотрошенного» и инструментированного кода для проверки удовлетворения всем требованиям рантаймовой проверкой, имхо, дело терминологии (а корректную терминологию я не знаю). Я бы считал.

Runtime верификацией всё же называют подходы, когда целевой (или анализируемый) код исполняется на процессоре, возможно, виртуальном. Абстрактную интерпретацию обычно относят к методам статического анализа. В BLAST и CPAchecker же основную роль играют методы анализа моделей (model checking) на основе автоматического инкрементального уточнения моделей, а абстрактная интерпретация используется для решения вспомогательных задач.

Кстати, у нас в Центре верификации ведутся работы как по статическому анализу модулей ядра, так и по динамическому. Недавно мы опубликовали слайды с LinuxCon Europe 2011 по этим проектам: http://linuxtesting.ru/linuxcon2011

«Для выполнения всего процесса инструментирования в целом в настоящее время используется набор инструментов LLVM [27]. Непосредственно для препроцессирования, разбора файлов с исходным кодом и одновременно выполняемого инструментирования на основе аспектных файлов используется LLVM GCC Front End, ввиду того, что GCC является основным для сборки ядра под ОС Linux.»

Что на это скажете?

> Что на это скажете?

Я скажу, что если ты не веришь Хорошилову, то мне и подавно не поверишь %)

Это и была его цитата.

Дело тут не в вере - просто хочется понять как работает эта штука.

>> если ты не веришь Хорошилову, то мне и подавно не поверишь %)

Это и была его цитата.

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

Runtime верификацией всё же называют подходы, когда целевой (или анализируемый) код исполняется на процессоре, возможно, виртуальном. Абстрактную интерпретацию обычно относят к методам статического анализа. В BLAST и CPAchecker же основную роль играют методы анализа моделей (model checking) на основе автоматического инкрементального уточнения моделей, а абстрактная интерпретация используется для решения вспомогательных задач.

просто хочется понять как работает эта штука.

Именно «эта штука» принципиально не сложная (хотя и большая), а для понимания BLAST и прочего лучше читать первоисточники.

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

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

Да, но в языках с зависимыми типами такого рода проверки by design будут в compile time (в системе типов). Так что в этой фразе про убогость (бедность) С и С++ есть доля истины - взять тот же cyclone (там не зависимые, а субструктурные типы) где типы решают часть проблем которые в С решаются только внешним статическим анализом.

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

я не думаю, что «зависимые типы требуют слишком большого внимания к себе»; кстати — субструктурные это про что?

насчет костылей — все сложно

с одной стороны, судя по багам, там часто ловится как раз то, для чего нужен паттерн матчинг:

if (!(card2 = icn_initcard(port, id2))) {
        printk(KERN_INFO
               "icn: (%s) half ICN-4B, port 0x%x added\n",
               card2->interface.id, port);
        return 0;
}

с другой — возможно, что костыли это как раз паттерн матчинг

рассмотрим мой пример:

int f(int* a, int* b, int* c, int* d)
{
  int x = g();

  switch( !!a + !!b + !!c + !!d ) {
    case 0: return x;
    case 1: return f1(x, a, b, c, d);
    case 2: return f2(x, a, b, c, d);
    case 3: return f3(x, a, b, c, d);
    case 4: return x + *a + *b + *c + *d;
  }
}

имеем простой и ясный код (f1, f2 и f3 могут принимать нулевые указатели), а теперь во что это выльется с паттерн матчингом? в спагетти из 16 вариантов, я так понимаю

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

примерно такую мысль высказывал tailgunner, хотя пример для иллюстрации я придумал сам

я кстати тогда с ним резко не согласился

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

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

я не думаю, что «зависимые типы требуют слишком большого внимания к себе»

Ну, если выбирать их как дисциплину программирования, то да. Если человек берёт agda/coq/twelf, он, видимо, знает чего хочет. Просто иногда, бывает, человек берёт haskell и начинает недоумевать по поводу всей этой капризности компилятора по отношению к типам.

кстати — субструктурные это про что?

Это линейные (linear) и упорядоченные (ordered). И те и другие - сужение unrestricted системы типов (unrestricted <- (affine, relevant) <- linear <- ordered, такое вложение). Первые подходят для рассуждений (система типов = логика) о выделении и освобождении объектов в куче (например, линейным программам не нужны ни ручное управление памятью, ни GC), вторые - на стеке. В первой главе ATTAPL об этом есть.

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

icn_initcard возвращает указатель на структуру, этот указатель присваивается card2, и если этот указатель не NULL, то пишем что-то? Ну в типах это будет:

Maybe   : forall (a : Type). a -> Type
nothing : forall (a : Type). Maybe a
just    : forall (a : Type). a -> Maybe a

и код будет писаться как-то так:

card <- initcard port id
case card of
  nothing -> do printk ...
                return ...
  just x  -> do ...

Либо, если нужны именно плоская память (или куча) и указатели, то они должны быть представлены в алгебраических зависимых типах тоже (как inductive families), тогда логика работы с памятью, арифметика указателей и тому подобные вещи будет частью системы типов (на эту тему можно посмотреть публикации Wouter Swierstra). Вообще, все типы должны быть алгебраическими, если хочется тотальности.

для чего нужен паттерн матчинг

Структурные типы (типы произведения) представляются в памяти так же как и сишные struct, а вариантные типы (типы суммы) - как сишные union с тайптегом (без тайптега делать case, который в рантайме, проблематично, case времени компиляции это на тему generic интерфейсов в духе классов типов хаскеля, но это работает только для выводимых типов, фишка вариантных типов в том, что вариант становится известен только в рантайме, это, фактически, динамическая диспетчеризация). Паттерн-матчинг (nested pattern matching) это сахар для (компилируется в) case, который сахар для набора примитивов case_n и get_m (n, m = 1, 2, ...), при этом примитивы case_n работают точно также как сишный switch по тайптегу, а get_m точно также как сишный struct->field.

Как бы, какая разница, делаем мы if (!ptr) ... или case ... of nothing/just...

рассмотрим мой пример

может ли бласт верифицировать такое

Не совсем понял этот пример (что мы тут верифицируем?). Но в свете того что код ADT и PM переписывается механически в код со структурами, объединениями и switch (и обратно), это не важно. Т.е. паттерн-матчинг это не та фишка из систем типов (это, вообще говоря, и не фишка систем типов) которую нужно рассматривать при разговоре о системах типах как средстве верификации.

Я имел ввиду прежде всего, что та логика которую пытаются привязать к программам внешние верификаторы имеется из коробки в мощных системах типов (не будем забывать про изоморфизм Карри-Говарда) - субструктурных типов достаточно для доказательств того, что программа не портит память, зависимые типы могут выводить длинны используемых массивов и, тем самым, не давать индексам выскочить за их границы (если только это не случайный индекс, но он не может быть случайным, по крайней мере вне IO), типы Хоара могут использоваться для рассуждений об I/O, типы пи-исчесления - для рассуждений о процессах и сообщениях ну и т.п.

рассмотрим мой пример

Теперь понял. Какие-то действия в зависимости от того какое количество указателей - NULL. Тут в куче все типы - натуральные числа, булевы числа, машинные слова, указатели. Так что их нужно сначала разделить:

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, TypeSynonymInstances #-}

import Data.Word

-- -----------------------------------------------------------------------------
-- * Primitive types.

-- | Natural numbers.
type N = Integer -- KLUDGE: haskell has no algebraic integers.

-- | Boolean numbers.
type B = Bool

-- | Machine word.
type W = Word -- ui32 or ui64. KLUDGE: not an algebraic type.

-- -----------------------------------------------------------------------------
-- * sizeOf and maxOf.

-- | The size of objects in a flat memory.
class SizeOf t where
  -- | Object size in bytes. Compile-time method.
  sizeOf :: t -> W
  -- | Use it for pointers and fixnums.
  maxOf  :: t -> N
  maxOf x = floor $ 2 ^^ (sizeOf x * 8) - 1

instance SizeOf W where
  sizeOf _ = 4 -- When configured for x86.

-- | The @Word@ type itself, use it in type-level.
word = undefined :: W

-- -----------------------------------------------------------------------------
-- * Pointers in a flat memory.

-- wtf? where is my segments and paging? ;-)

-- | Bad or good pointer.
data Ptr = Null | Ptr N -- isomorphic to (Maybe N)
  -- deriving ( Show, Read, Eq, Ord, Enum, Num, Functor, Applicative, Monad, Binary, etc. )

-- | Pointer arithmetic.
class PtrArith t where
  -- | The sum of two pointers.
  (+.) :: t -> t -> t
  -- | Etc.
  -- ...

instance PtrArith Ptr where
  Null  +. Null  = Null
  Null  +. Ptr y = Ptr y
  Ptr x +. Null  = Ptr x
  Ptr x +. Ptr y
    | x + y < maxOf word = Ptr $ x + y
    | otherwise          = Null

-- -----------------------------------------------------------------------------
-- * Casting.

-- | A casting functor (yeah, really functor).
class Cast a b | a -> b where
  -- | Cast type @a@ to type @b@ when it makes sense.
  cast :: a -> b

-- Forgetful functor.
instance Cast Ptr B where
  cast Null    = False
  cast (Ptr _) = True

-- Just a functor.
instance Cast B W where
  cast False = 0
  cast True  = 1

-- W to B? Yes, if W is an algebraic type.

Тогда этот код так и будет выглядеть:

argh :: Ptr -> W
argh = (cast :: B -> W) . (cast :: Ptr -> B)

test a b c d =
  let x = Ptr 777 in
  case argh a + argh b + argh c + argh d of
    0 -> x
    1 -> x -- f1 ...
    2 -> x -- f2 ...
    3 -> x -- f3 ...
    4 -> x +. a +. b +. c +. d

Чтобы всё стало очень хорошо, нужно обзавестись алгебраическими числами и представлять плоскую память с сегментами, страницами, указателями относительными и абсолютными прямо как есть в типах, т.е. модель машины должна быть в ADT (точнее в inductive families), если мы хотим верифицировать выполнение программы на такой машине. При этом модель кучи со стеком требуют других представлений (примечательно, что на сырой машине нет ни кучи, ни стека - одно готовит ядро, а другое - рантайм языка), и все три представления не должны путаться - они и не будут путаться если будут разными типами.

> switch( !!a + !!b + !!c + !!d ) {

имеем простой и ясный код (f1, f2 и f3 могут принимать нулевые указатели)

Вот лично я не понял, что проверяет эта «простая и ясная» проверка.

Чего вы прицепились к проверке указателя на NULL? Это банальщина. Изобразите хотя бы проверку захвата мютекса (пример есть в статье); изобразите запрет использования kmalloc(*, GFP_KERNEL) из прерывания; выразите условие «при доступе к переменной p->x необходимо захватить спинлок p->y» - короче, что-нибудь менее банальное, но полезное на практике.

Чего вы прицепились к проверке указателя на NULL?

Там не NULL, там !!a + !!b + !!c + !!d. Т.е. ptr -(неявно)-> int -(неявно)-> bool -(logical not)-> bool -(logical not)-> bool -(неявно)-> int (что редуцируется в явные ptr -> bool -> int). Итого, в зависимости от того сколько NULL-pointer-ов среди a, b, c, d, - делаем разные действия.

что-нибудь менее банальное, но полезное на практике.

На код-базе дефолт-ядра? Это никак нельзя (нет, ну можно, конечно, как в сабже).

Как пример верификации чего-то более полезного на практике с использование теории типов можно привести верификацию STM. И как реализацию - монаду STM из GHC с compile-time гарантией атомичности и изолированности транзакций.

запрет использования kmalloc(*, GFP_KERNEL) из прерывания

Вот как раз, два параметрических типа IO и STM с линейными монадическими интерфейсами не могут смешиваться (нельзя делать IO в STM и тем самым разрушить гарантии STM), и этот запрет - следствие правил типизации (довольно простых, причём). Это, конечно, так потому что об этом подумали и сделали именно так - потому что система типов позволяет так делать. У си не позволяет, по чисто историческим причинам (теоретически, нет причин по которым си не мог бы быть безопасным и иметь мощные типы).