On Symbolic Execution of Decompiled Programs
Identifikátory výsledku
Kód výsledku v IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F20%3A00114781" target="_blank" >RIV/00216224:14330/20:00114781 - isvavai.cz</a>
Výsledek na webu
<a href="http://dx.doi.org/10.1109/QRS51102.2020.00044" target="_blank" >http://dx.doi.org/10.1109/QRS51102.2020.00044</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1109/QRS51102.2020.00044" target="_blank" >10.1109/QRS51102.2020.00044</a>
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
On Symbolic Execution of Decompiled Programs
Popis výsledku v původním jazyce
In this paper, we present a combination of existing and new tools that together make it possible to apply formal verification methods to programs in the form of x86_64 machine code. Our approach first uses a decompilation tool (remill) to extract low-level intermediate representation (LLVM) from the machine code. This step consists of instruction translation(i.e. recovery of operation semantics), control flow extraction and address identification. The main contribution of this paper is the second step, which builds on data flow analysis and refinement of indirect (i.e. data-dependent) control flow. This step makes the processed bitcode much more amenable to formal analysis.To demonstrate the viability of our approach, we have compiled a set of benchmark programs into native executables and analysed them using two LLVM-based tools: DIVINE, a software model checker and KLEE, a symbolic execution engine. We have compared the outcomes to direct analysis of the same programs.
Název v anglickém jazyce
On Symbolic Execution of Decompiled Programs
Popis výsledku anglicky
In this paper, we present a combination of existing and new tools that together make it possible to apply formal verification methods to programs in the form of x86_64 machine code. Our approach first uses a decompilation tool (remill) to extract low-level intermediate representation (LLVM) from the machine code. This step consists of instruction translation(i.e. recovery of operation semantics), control flow extraction and address identification. The main contribution of this paper is the second step, which builds on data flow analysis and refinement of indirect (i.e. data-dependent) control flow. This step makes the processed bitcode much more amenable to formal analysis.To demonstrate the viability of our approach, we have compiled a set of benchmark programs into native executables and analysed them using two LLVM-based tools: DIVINE, a software model checker and KLEE, a symbolic execution engine. We have compared the outcomes to direct analysis of the same programs.
Klasifikace
Druh
D - Stať ve sborníku
CEP obor
—
OECD FORD obor
10200 - Computer and information sciences
Návaznosti výsledku
Projekt
<a href="/cs/project/GA18-02177S" target="_blank" >GA18-02177S: Abstrakce a jiné techniky v semi-symbolické verifikaci programů</a><br>
Návaznosti
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach
Ostatní
Rok uplatnění
2020
Kód důvěrnosti údajů
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Údaje specifické pro druh výsledku
Název statě ve sborníku
Proceedings - 2020 IEEE 20th International Conference on Software Quality, Reliability, and Security, QRS 2020
ISBN
9781728189147
ISSN
—
e-ISSN
—
Počet stran výsledku
8
Strana od-do
265-272
Název nakladatele
IEEE Computer Society
Místo vydání
Neuveden
Místo konání akce
Neuveden
Datum konání akce
1. 1. 2020
Typ akce podle státní příslušnosti
CST - Celostátní akce
Kód UT WoS článku
000648778000030