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.

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.

Další info