D 2020

On Symbolic Execution of Decompiled Programs

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

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

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

UT WoS

000648778000030

Klíčová slova anglicky

symbolic execution; decompilation; model checking; llvm

Štítky

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 29. 4. 2021 08:16, RNDr. Pavel Šmerk, Ph.D.

Anotace

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.

Návaznosti

GA18-02177S, projekt VaV
Ná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 MU
Ná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 MU
Ná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