KORENČIK, Lukáš, Petr ROČKAI, Henrich LAUKO a 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. s. 265-272. ISBN 978-1-7281-8914-7. doi:10.1109/QRS51102.2020.00044. 2020.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název On Symbolic Execution of Decompiled Programs
Autoři KORENČIK, Lukáš (703 Slovensko, domácí), Petr ROČKAI (703 Slovensko, domácí), Henrich LAUKO (703 Slovensko, domácí) a Jiří BARNAT (203 Česká republika, domácí).
Vydání Neuveden, Proceedings - 2020 IEEE 20th International Conference on Software Quality, Reliability, and Security, QRS 2020, od s. 265-272, 8 s. 2020.
Nakladatel IEEE Computer Society
Další údaje
Originální jazyk angličtina
Typ výsledku Stať ve sborníku
Obor 10200 1.2 Computer and information sciences
Stát vydavatele Spojené státy
Utajení není předmětem státního či obchodního tajemství
Forma vydání tištěná verze "print"
Kód RIV RIV/00216224:14330/20:00114781
Organizační jednotka Fakulta informatiky
ISBN 978-1-7281-8914-7
Doi http://dx.doi.org/10.1109/QRS51102.2020.00044
UT WoS 000648778000030
Klíčová slova anglicky symbolic execution; decompilation; model checking; llvm
Štítky firank_B
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 29. 4. 2021 08:16.
Anotace
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ávaznosti
GA18-02177S, projekt VaVNázev: Abstrakce a jiné techniky v semi-symbolické verifikaci programů
Investor: Grantová agentura ČR, Abstrakce a jiné techniky v semi-symbolické verifikaci programů
MUNI/A/1050/2019, interní kód MUNázev: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace IX (Akronym: SV-FI MAV IX)
Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace IX, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
MUNI/A/1076/2019, interní kód MUNázev: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 20 (Akronym: SKOMU)
Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 20, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
VytisknoutZobrazeno: 29. 3. 2024 06:13