Binary Analysis based on Symbolic Execution and Reversible x86 Instructions

Issue title: Methods for Distributed and Concurrent Systems: Special Issue on the occasion of the 60th Birthday of Professor Gabriel Ciobanu

Guest editors: Bogdan Aman, Jetty Kleijn, Maciej Koutny and Dorel Lucanu

Article type: Research Article

Authors: Stoenescu, Teodor^a | Stefanescu, Alin^{b; *} | Predut, Sorina^b | Ipate, Florentin^b

Affiliations: [a] Bitdefender, Romania. tstoenescu@bitdefender.com | [b] University of Bucharest, Department of Computer Science, Bucharest, Romania. alin@fmi.unibuc.ro, sina.predut@gmail.com, florentin.ipate@ifsoft.ro

Correspondence: [*] Address for correspondence: Department of Computer Science, University of Bucharest, Str. Academiei 14, 010014 Bucharest, Romania

Abstract: We present a binary analysis framework based on symbolic execution with the distinguishing capability to execute stepwise forward and also backward through the execution tree. It was developed internally at Bitdefender and code-named RIVER. The framework provides components such as a taint engine, a dynamic symbolic execution engine, and integration with Z3 for constraint solving. In this paper we will provide details on the framework and give an example of analysis on binary code.

DOI: 10.3233/FI-2017-1533

Journal: Fundamenta Informaticae, vol. 153, no. 1-2, pp. 105-124, 2017