Další formáty:
BibTeX
LaTeX
RIS
@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 a 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, s.~265-272. ISBN~978-1-7281-8914-7. Dostupné z: https://dx.doi.org/10.1109/QRS51102.2020.00044.
|