Informace o projektu

Symbolická exekuce spustitelných programů v nástroji DIVINE

Kód projektu
MUNI/33/07/2018
Období řešení
12/2018 - 11/2019
Investor / Programový rámec / typ projektu
Masarykova univerzita
Fakulta / Pracoviště MU
Fakulta informatiky

DIVINE je nástroj sloužící k verifikaci programů napsaných v jazyce C nebo C++
využitím LLVM bitkódu. Krom explicitní verifikace umožňuje použití symbolických
metod, konkrétně dokáže využít reprezentace dat programu pomocí bitvektorové
logiky. Zatím ale chybí podpora klasické symbolické exekuce. Jedním z cílů
tohoto projektu je tento nedostatek odstranit.

Dále plánujeme využít skutečnost, že LLVM bitkód lze získat i jinak, než jen
překladem vysokoúrovňového kódu. Zejména existují nástroje (RetDec, McSema),
které jsou schopné dekompilovat program ve strojovém kódu zpět do LLVM bitkódu.
V kombinaci s podporou symbolické exekuce LLVM bitkódu bychom pak chtěli umožnit
také použití této techniky na již přeloženém spustitelném programy.