You are viewing a javascript disabled version of the site. Please enable Javascript for this site to function properly.
Go to headerGo to navigationGo to searchGo to contentsGo to footer
In content section. Select this link to jump to navigation

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, Teodora | Stefanescu, Alinb; * | Predut, Sorinab | Ipate, Florentinb

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

Published: 7 June 2017
Price: EUR 27.50
Show more