Виртуальная машина KLEE для символьного выполнения кода

В этом посте мы попробуем применить технику символьного выполнения на примере символьной ВМ KLEE для решения простого ASCII-лабиринта. Как вы думаете, сколько верных решений мы сможем найти?

Лабиринт

Сам лабиринт представляет собой программу на С, код которой вы можете взять здесь. После запуска игра ожидает ввода последовательности шагов (a — шаг влево, d — вправо, w — вверх и s — вниз). Выглядит это так:

Player pos: 1x4
Iteration no. 2. Action: s.
+-+---+---+
|X|     |#|
|X| --+ | |
|X|   | | |
|X+-- | | |
|     |   |
+-----+---+

Несмотря на кажущуюся простоту, лабиринт скрывает в себе один секрет и поэтому имеет более чем одно решение.

KLEE

KLEE — символьный интерпретатор биткода LLVM, т.е. он может выполнять код, сгенерированный любым фронт-эндом. Суть символьного выполнения сводится к тому, что все входные значения запускаемой программы содержат не конкретные значения, а символьные ограничения на возможные значения. В процессе выполнения могут создаваться новые символьные переменные (например, когда их значения зависят от результата какой-либо операции с символьным операндом), а так же изменяться существующие (при ветвлении на пути выполнения программы). Во втором случае KLEE использует SMT решатель, чтобы определить, возможно ли в принципе выполнение программы по данному пути.
Если вас заинтересовала эта тема, можете посмотреть здесь и почитать это или даже это.

Идея поста проста — скормить программе-лабиринту символьную строку и посмотреть как KLEE найдет решения.

Разберем код

Лабиринт задается в виде двумерного массива символов.

#define H 7
#define W 11
char maze[H][W] = { "+-+---+---+",
                    "| |     |#|",
                    "| | --+ | |",
                    "| |   | | |",
                    "| +-- | | |",
                    "|     |   |",
                    "+-----+---+" };

Задача draw() — рисовать наш массив на экране.

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");
}

Функция main() начинается с объявления переменных, хранящих позицию игрока, итератора и 28-байтного массива, который хранит действия. Затем, начальная позиция игрока устанавливается равной (1,1) и на этом месте рисуется крестик.

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';

Читаем из stdin что там ввел игрок.

    read(0,program,ITERS);

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

    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);
        }

Если игрок дошел до конца — поздравляем его.

        if (maze[y][x] == '#')
        {
                printf ("You win!\n");
                printf ("Your solution \n",program);
                exit (1);
        }

Если что-то не так — возвращаемся на место, где стояли.

        if (maze[y][x] != ' ' &&
            !((y == 2 && maze[y][x] == '|' && x > 0 && x < W)))
		    {
			    x = ox;
			    y = oy;
		    }

Если врезались в стену — игрок проиграл.

        if (ox==x && oy==y){
                printf("You loose\n");
                exit(-2);
        }

Ну а если ничего не случилось — значит мы просто шагнули. Двигаем игрока, рисуем картинку, увеличиваем итератор и возвращаемся на начало.

        maze[y][x]='X';
        draw ();          //draw it
        i++;
        sleep(1); //me wait to human
    }

Пройдем лабиринт вручную

Если вам вдруг захочется пройти игру самим, то, скорее всего, вы получите следующее решение: ssssddddwwaawwddddssssddwwww

А теперь с KLEE

Прежде всего, нам понадобится LLVM, транслятор C -> LLVM IR (llvm-gcc или clang) и, собственно, KLEE. В большинстве дистрибутивов Linux эти пакеты уже есть в репозиториях.
Чтобы транслировать mace.c в биткод LLVM нужно выполнить команду

$ llvm-gcc -c –emit-llvm maze.c -o maze.bc

Как и говорилось ранее, вместо llvm-gcc можно использовать clang.

В результате выполнения этой команды мы получил файл maze.bc, который представляет собой биткод программы-лабиринта. Его даже можно запустить на интерпретаторе LLVM:

$ lli maze.bc

Для тестирования кода с помощью KLEE, нам необходимо пометить какие-нибудь переменные символьными. В данном случае, это будет массив действий, объявленный в начале main(). Итак, заменяем строку

    read(0,program,ITERS);

на

    klee_make_symbolic(program,ITERS,"program");

И не забудем добавить заголовочный файл KLEE

#include <klee/klee.h>

Теперь KLEE сможет пройти по любому возможному пути выполнения (да и коридору лабиринта). Причем, если эти пути могут привести к какой-либо ошибке (например, к переполнению буфера), KLEE сигнализирует нам об этом. Выполняем

$ klee maze.bc

и наблюдаем такую картину:

Как видно из последних 3х сообщений, KLEE нашла 321 разный путь. Правда, это не 321 верное решение.

KLEE: done: total instructions = 112773
KLEE: done: completed paths = 321
KLEE: done: generated tests = 318

Подробный отчет сохраняется в директорию klee-last

$ 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

$ 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′

В данном случае, вы можете просто взять значение переменной program отсюда и воспроизвести тест, передав это значение программе-лабиринту.

Итак, мы и нашли все возможные пути следования в программе. Но не просматривать же каждый тест, чтобы найти все верные решения! Нам нужно заставить KLEE выделить тесты, которые действительно доходят до «You win!».
В интерфейсе KLEE присутствует функция klee_assert(), которая делает то же самое, что и аналогичная ей assert() в C — вычисляет значение булевого выражения и, если оно false — прерывает выполнение программы. Для нашего случая это то, что доктор прописал.
Добавим после строки

printf ("You win!\n");

безусловный вызов klee_assert()

printf ("You win!\n");
klee_assert(0);  //Signal The solution!!

Теперь KLEE не перестанет генерировать тесты для всех возможных путей выполнения, однако тесты, приводящие к вызову klee_assert() будут иметь .err в своем имени:

$ 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 решение — sddwddddssssddwwww
Эй, позвольте! Оно выглядит коротким! Давайте попробуем его на настоящем лабиринте:

Я так и знал!!! В лабиринте есть ненастоящие стены! И KLEE благополучно прошла сквозь них! Но погодите, если KLEE должна была найти все решения, то где наше самое первое? Почему KLEE не нашла его?
Чтож, обычно нам достаточно одного пути до ошибки, если мы ищем саму ошибку, а альтернативные пути до нее нам не требуются. Поэтому, в данном случае воспользуемся одной из 10000 опций командной строки.

$ klee –emit-all-errors maze_klee.o

Смотрим на результат:

Теперь мы получили 4 теста, которые и являются 4 возможными решениями нашего лабиринта:

$ 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′

Итак, решения данного лабиринта:
1. ssssddddwwaawwddddssssddwwww
2. ssssddddwwaawwddddsddw
3. sddwddddssssddwwww
4. sddwddddsddw