Informace o projektu
Symbolická exekuce spustitelných programů v nástroji DIVINE
| Kód projektu | MUNI/33/07/2018 CEP CORDIS MU WEB INET MU |
|---|---|
| Doba řešení | 01.12.2018–30.11.2019 |
| Stav | ukončený |
| Investor | Masarykova univerzita |
| Program | Program děkana FI |
| Řešitel za FI | |
| Členové realizačního týmu za FI |
Anotace
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.
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.