On Symbolic Execution of Decompiled Programs

D 2020

On Symbolic Execution of Decompiled Programs

KORENČIK, Lukáš, Petr ROČKAI, Henrich LAUKO and Jiří BARNAT

Basic information

Original name

On Symbolic Execution of Decompiled Programs

Authors

KORENČIK, Lukáš (703 Slovakia, belonging to the institution), Petr ROČKAI (703 Slovakia, belonging to the institution), Henrich LAUKO (703 Slovakia, belonging to the institution) and Jiří BARNAT (203 Czech Republic, belonging to the institution)

Edition

Neuveden, Proceedings - 2020 IEEE 20th International Conference on Software Quality, Reliability, and Security, QRS 2020, p. 265-272, 8 pp. 2020

Publisher

IEEE Computer Society

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10200 1.2 Computer and information sciences

Country of publisher

United States of America

Confidentiality degree

není předmětem státního či obchodního tajemství

Publication form

printed version "print"

RIV identification code

RIV/00216224:14330/20:00114781

Organization unit

Faculty of Informatics

ISBN

978-1-7281-8914-7

DOI

http://dx.doi.org/10.1109/QRS51102.2020.00044

UT WoS

000648778000030

Keywords in English

symbolic execution; decompilation; model checking; llvm

Abstract

V originále

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.

Links

GA18-02177S, research and development project

Name: Abstrakce a jiné techniky v semi-symbolické verifikaci programů

Investor: Czech Science Foundation

MUNI/A/1050/2019, interní kód MU

Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace IX (Acronym: SV-FI MAV IX)

Investor: Masaryk University, Category A

MUNI/A/1076/2019, interní kód MU

Name: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 20 (Acronym: SKOMU)

Investor: Masaryk University, Category A

Citovat

KORENČIK, Lukáš, Petr ROČKAI, Henrich LAUKO and Jiří BARNAT. On Symbolic Execution of Decompiled Programs. In Proceedings - 2020 IEEE 20th International Conference on Software Quality, Reliability, and Security, QRS 2020. Neuveden: IEEE Computer Society, 2020, p. 265-272. ISBN 978-1-7281-8914-7. Available from: https://dx.doi.org/10.1109/QRS51102.2020.00044.

@inproceedings{1760802,
   author = {Korenčik, Lukáš and Ročkai, Petr and Lauko, Henrich and Barnat, Jiří},
   address = {Neuveden},
   booktitle = {Proceedings - 2020 IEEE 20th International Conference on Software Quality, Reliability, and Security, QRS 2020},
   doi = {http://dx.doi.org/10.1109/QRS51102.2020.00044},
   keywords = {symbolic execution; decompilation; model checking; llvm},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Neuveden},
   isbn = {978-1-7281-8914-7},
   pages = {265-272},
   publisher = {IEEE Computer Society},
   title = {On Symbolic Execution of Decompiled Programs},
   year = {2020}
}

TY  - JOUR
ID  - 1760802
AU  - Korenčik, Lukáš - Ročkai, Petr - Lauko, Henrich - Barnat, Jiří
PY  - 2020
TI  - On Symbolic Execution of Decompiled Programs
PB  - IEEE Computer Society
CY  - Neuveden
SN  - 9781728189147
KW  - symbolic execution
KW  - decompilation
KW  - model checking
KW  - llvm
N2  - 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.
ER  -

KORENČIK, Lukáš, Petr ROČKAI, Henrich LAUKO and Jiří BARNAT. On Symbolic Execution of Decompiled Programs. In \textit{Proceedings - 2020 IEEE 20th International Conference on Software Quality, Reliability, and Security, QRS 2020}. Neuveden: IEEE Computer Society, 2020, p.~265-272. ISBN~978-1-7281-8914-7. Available from: https://dx.doi.org/10.1109/QRS51102.2020.00044.

Detailed Information on Publication Record