В этом посте мы попытаемся использовать технику символического выполнения на примере символической виртуальной машины KLEE для решения простого лабиринта ASCII. Как вы думаете, сколько правильных решений мы сможем найти? 
Лабиринт
Сам лабиринт представляет собой программу на языке C, код для которой можно взять Здесь .После запуска игра ожидает ввода последовательности шагов (a – шаг влево, d – вправо, w – вверх и s – вниз).
Это выглядит так:
Player pos: 1x4 Iteration no. 2. Action: s. +-+---+---+ |X| |#| |X| --+ | | |X| | | | |X+-- | | | | | | +-----+---+Несмотря на кажущуюся простоту, лабиринт скрывает одну тайну и поэтому имеет более одного решения.
КЛЕЕ
KLEE — это символьный интерпретатор битового кода LLVM, т. е.он может выполнять код, сгенерированный любым внешним интерфейсом.
Суть символьного выполнения сводится к тому, что все входные значения запускаемой программы содержат не конкретные значения, а символические ограничения на возможные значения.
В ходе выполнения могут создаваться новые символьные переменные (например, когда их значения зависят от результата какой-либо операции с символьным операндом), а также изменяться существующие (при ветвлениях по пути выполнения программы).
Во втором случае KLEE использует решатель SMT, чтобы определить, возможно ли в принципе выполнить программу по заданному пути.
Если вам интересна эта тема, вы можете посмотреть Здесь и читать Этот или даже Этот .
Идея поста проста — скормите символьную строку программе-лабиринту и посмотрите, как KLEE находит решения.
Давайте проанализируем код
Лабиринт задается как двумерный массив символов.
$ llvm-gcc -c –emit-llvm maze.c -o maze.bcЗадача draw() — отрисовать наш массив на экране.
$ lli maze.bcФункция main() начинается с объявления переменных, хранящих позицию игрока, итератора и 28-байтового массива, хранящего действия.
Затем стартовая позиция игрока устанавливается на (1,1) и в этом месте рисуется крест.
$ klee maze.bcЧитаем со стандартного ввода то, что туда ввел игрок.
KLEE: done: total instructions = 112773 KLEE: done: completed paths = 321 KLEE: done: generated tests = 318Далее на каждой итерации цикла мы сохраняем старые координаты пользователя и перемещаем его в новое место.
$ ls klee-last/ assembly.ll test000078.ktest test000158.ktest info test000079.ktest test000159.ktest messages.txt test000080.ktest test000160.ktest run.istats test000081.ktest test000161.ktest run.stats test000082.ktest test000162.ktest test000001.ktest test000083.ktest test000163.ktest test000075.ktest test000155.ktest warnings.txtЕсли игрок дошел до конца, поздравляем.
$ ktest-tool klee-last/test000222.ktest ktest file : ‘klee-last/test000222.ktest’ args : ['maze_klee.o'] num objects: 1 object 0: name: ‘program’ object 0: size: 29 object 0: data: ‘ssssddddwwaawwddddssssddwwwd\x00′Если что-то не так, возвращаемся на то место, где стояли.
$ ls -1 klee-last/ |grep -A2 -B2 err test000096.ktest test000097.ktest test000098.assert.err test000098.ktest test000098.pcЕсли они врезались в стену, игрок проигрывал.
$ ktest-tool klee-last/test000098.ktest ktest file : ‘klee-last/test000098.ktest’ args : ['maze_klee.o'] num objects: 1 object 0: name: ‘program’ object 0: size: 29 object 0: data: ‘sddwddddssssddwwww\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00′Ну а если ничего не произошло, то мы просто наступили.
Перемещаем игрока, рисуем картинку, увеличиваем итератор и возвращаемся в начало.
$ klee –emit-all-errors maze_klee.o
Пройдемся по лабиринту вручную
Если вы вдруг захотите пройти игру самостоятельно, то скорее всего вы получите следующее решение: сссссдддвваааввдддссссссддwwww
И теперь с KLEE
Прежде всего нам понадобится LLVM, ИК-транслятор C -> LLVM (llvm-gcc или clang) и, собственно, KLEE. Большинство дистрибутивов Linux уже имеют эти пакеты в своих репозиториях.Чтобы перевести mace.c в биткод LLVM, вам нужно запустить команду
$ ktest-tool klee-last/test000097.ktest ktest file : ‘klee-last/test000097.ktest’ args : ['maze_klee.o'] num objects: 1 object 0: name: ‘program’ object 0: size: 29 object 0: data: ‘sddwddddsddw\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00′ $ ktest-tool klee-last/test000136.ktest ktest file : ‘klee-last/test000136.ktest’ args : ['maze_klee.o'] num objects: 1 object 0: name: ‘program’ object 0: size: 29 object 0: data: ‘sddwddddssssddwwww\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00′ $ ktest-tool klee-last/test000239.ktest ktest file : ‘klee-last/test000239.ktest’ args : ['maze_klee.o'] num objects: 1 object 0: name: ‘program’ object 0: size: 29 object 0: data: ‘ssssddddwwaawwddddsddw\x00\x00\x00\x00\x00\x00\x00′ $ ktest-tool klee-last/test000268.ktest ktest file : ‘klee-last/test000268.ktest’ args : ['maze_klee.o'] num objects: 1 object 0: name: ‘program’ object 0: size: 29 object 0: data: ‘ssssddddwwaawwddddssssddwwww\x00′Как упоминалось ранее, вместо llvm-gcc вы можете использовать clang. В результате выполнения этой команды мы получили файл maze.bc, который является биткодом программы лабиринта.
Его даже можно запустить в интерпретаторе LLVM: #define H 7
#define W 11
char maze[H][W] = { "+-+---+---+",
"| | |#|",
"| | --+ | |",
"| | | | |",
"| +-- | | |",
"| | |",
"+-----+---+" };
Чтобы протестировать код с использованием KLEE, нам нужно пометить некоторые переменные как символические.
В данном случае это будет массив действий, объявленный в начале main().
Итак, заменяем строку void draw ()
{
int i, j;
for (i = 0; i < H; i++)
{
for (j = 0; j < W; j++)
printf ("%c", maze[i][j]);
printf ("\n");
}
printf ("\n");
}
на int
main (int argc, char *argv[])
{
int x, y; //Player position
int ox, oy; //Old player position
int i = 0; //Iteration number
#define ITERS 28
char program[ITERS];
x = 1;
y = 1;
maze[y][x]='X';
И не забудьте добавить заголовочный файл KLEE read(0,program,ITERS);
Теперь KLEE сможет пройти по любому возможному пути выполнения (и даже по коридору лабиринта).
Причём, если эти пути могут привести к какой-либо ошибке (например, переполнению буфера), KLEE сигнализирует нам об этом.
Мы осуществляем while(i < ITERS)
{
ox = x; //Save old player position
oy = y;
switch (program[i])
{
case 'w':
y--;
break;
case 's':
y++;
break;
case 'a':
x--;
break;
case 'd':
x++;
break;
default:
printf("Wrong command!(only w,s,a,d accepted!)\n");
printf("You loose!\n");
exit(-1);
}
и видим такую картину:
Как видно из последних трёх постов, KLEE нашел 321 различный путь.
Правда, это не 321 правильное решение.
if (maze[y][x] == '#')
{
printf ("You win!\n");
printf ("Your solution \n",program);
exit (1);
}
Подробный отчет сохраняется в каталоге klee-last. if (maze[y][x] != ' ' &&
!((y == 2 && maze[y][x] == '|' && x > 0 && x < W)))
{
x = ox;
y = oy;
}
Каждый тест можно просмотреть с помощью утилиты ktest-tool. if (ox==x && oy==y){
printf("You loose\n");
exit(-2);
}
В этом случае можно просто взять отсюда значение программной переменной и воспроизвести тест, передав это значение программе лабиринта.
Итак, мы нашли все возможные пути следования в программе.
Но невозможно пройти каждый тест, чтобы найти все правильные решения! Нам нужно, чтобы KLEE выделял тесты, которые действительно приводят к выводу «Вы выиграли!» Интерфейс KLEE содержит функцию klee_assert(), которая делает то же самое, что и ее аналог Assert() в C — она вычисляет значение логического выражения и, если оно ложно, прерывает выполнение программы.
В нашем случае это то, что доктор прописал.
Добавьте после строки maze[y][x]='X';
draw (); //draw it
i++;
sleep(1); //me wait to human
}
безусловный вызов klee_assert() read(0,program,ITERS);
Теперь KLEE не прекратит генерировать тесты для всех возможных путей выполнения, однако тесты, результатом которых является вызов klee_assert(), будут иметь в своем имени .
err: klee_make_symbolic(program,ITERS,"program");
Давайте посмотрим на один из них #include <klee/klee.h>
Итак, решение, предложенное KLEE, следующее: сдддддссссссддвввв
О, позвольте мне! Выглядит коротко! Давайте попробуем это на реальном лабиринте:
Я знал это!!! В лабиринте фальшивые стены! И KLEE благополучно прошел сквозь них! Но подождите, если KLEE должен был найти все решения, то где же наше самое первое? Почему KLEE не нашел его?
Ну, обычно нам нужен только один путь к ошибке, если мы ищем саму ошибку, и нам не нужны альтернативные пути к ней.
Поэтому в данном случае мы будем использовать один из 10 000 вариантов командной строки.
printf ("You win!\n");
Посмотрим на результат:
Теперь у нас есть 4 теста, которые представляют собой 4 возможных решения нашего лабиринта: printf ("You win!\n");
klee_assert(0); //Signal The solution!!
Итак, решения этого лабиринта:
1. сссссдддввааувдддссссддвввв
2. сссссдддввааувдддсдв
3. сдддддссссссддвввв
4. сддвдддсдв
Теги: #llvm #klee #Символическое исполнение #информационная безопасность
-
Скайп: Говорите, Нас Не Слышат.
19 Oct, 24 -
Декабрьский Шведский Стол
19 Oct, 24
