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. doi:10.1109/QRS51102.2020.00044.
Other formats:   BibTeX LaTeX RIS
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
Original language English
Type of outcome Proceedings paper
Field of Study 10200 1.2 Computer and information sciences
Country of publisher United States of America
Confidentiality degree is not subject to a state or trade secret
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
Keywords in English symbolic execution; decompilation; model checking; llvm
Tags firank_B
Tags International impact, Reviewed
Changed by Changed by: RNDr. Pavel Šmerk, Ph.D., učo 3880. Changed: 29/4/2021 08:16.
Abstract
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 projectName: Abstrakce a jiné techniky v semi-symbolické verifikaci programů
Investor: Czech Science Foundation, Standard Projects
MUNI/A/1050/2019, internal MU codeName: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace IX (Acronym: SV-FI MAV IX)
Investor: Masaryk University, Grant Agency of Masaryk University, Category A
MUNI/A/1076/2019, internal MU codeName: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 20 (Acronym: SKOMU)
Investor: Masaryk University, Grant Agency of Masaryk University, Category A
PrintDisplayed: 19/1/2022 15:12