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.

You are running an old browser version. We recommend updating your browser to its latest version.

More info