Please enable JavaScript.
Coggle requires JavaScript to display documents.
2015 - BINSEC: Binary Code Analysis with Low-Level Regions (Information…
2015 - BINSEC: Binary Code Analysis
with Low-Level Regions
Authors
Djoudi A
Bardin S
Goals
Presents BINSEC, open source platform for (formal) binary-level code analysis
Ease the development of binary code analyzers by providing an open formal model for binary programs and an open-source platform allowing to share front-ends and ISA support.
Contribution
Information
Based on an extension of the DBA Intermediate Representation
Composed of three main modules
Front-end
Loading and Decoding
Decoding function taking a (virtual) address and returning a block of DBA instructions simulating the semantics of the corresponding machine code instruction
Disassembly
Goal of disassembly is to give the semantics of the whole executable file
Formal Stubs
A block of DBA instructions that will be inserted at some address of the retrieved program, either in place of the result of the decoder
(@replace
) or in combination with it
(@insert
)
Useful either when the corresponding code is not available (analysis of object files rather than executable files), or for abstracting parts of the code
Static analysis module
CFG recovery
Simulator
Handle extended DBA
Provide simulation and random testing modes supporting all features of extended DBA
Memory models
Flat model
Standard region-based model
Low-level region-based model
Platform for (formal) binary-level code analysis
DBA
Dynamic Bit-vector Automata, IR language
Advantages
Very concise set of instructions and operators
A simple semantics, without any implicit side-effect
Architecture-independent formalism
Extended DBA
DBA lack abstraction and specification mechanisms in order to handle binary-level analysis over large non-critical codes
Improvements over DBA
Access permissions for read, write and execute operations; permissions are defined on region zones
More abstract operations
Tags on instructions and variables for embedding useful information available at decoding
What is?
Stub
Formal