Title
Binary Analysis based on Symbolic Execution and Reversible x86 Instructions.
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.
Year
DOI
Venue
2017
10.3233/FI-2017-1533
FUNDAMENTA INFORMATICAE
Field
DocType
Volume
Information theory,x86,Discrete mathematics,Parallel computing,Binary code,Binary analysis,Theoretical computer science,Symbolic execution,Mathematical model,Mathematics,Binary operation
Journal
153
Issue
ISSN
Citations 
1-2
0169-2968
0
PageRank 
References 
Authors
0.34
0
4
Name
Order
Citations
PageRank
Teodor Stoenescu111.04
Alin Stefanescu220917.79
Sorina Predut300.34
Florentin Ipate441943.20