On Symbolic Execution of Decompiled Programs

Result code in 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>
Result on the web
<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>

Result language
angličtina
Original language name
On Symbolic Execution of Decompiled Programs
Original language description
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.
Czech name
—
Czech description
—

Project
<a href="/en/project/GA18-02177S" target="_blank" >GA18-02177S: Abstraction and Other Techniques in Semi-Symbolic Program Verification</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach

Publication year
2020
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection
Proceedings - 2020 IEEE 20th International Conference on Software Quality, Reliability, and Security, QRS 2020
ISBN
9781728189147
ISSN
—
e-ISSN
—
Number of pages
8
Pages from-to
265-272
Publisher name
IEEE Computer Society
Place of publication
Neuveden
Event location
Neuveden
Event date
Jan 1, 2020
Type of event by nationality
CST - Celostátní akce
UT code for WoS article
000648778000030

Similar results(10)