Project information

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

Project Identification
MUNI/33/07/2018
Project Period
12/2018 - 11/2019
Investor / Pogramme / Project type
Masaryk University
MU Faculty or unit
Faculty of Informatics

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.