Post-doc or Research Engineer on Binary Analysis of Program
The Insight framework provides tools for analyzing binary programs and extract their control-flow graph and map it to microcode (our intermediate representation for binary program).
The platform is now grounded but we would like to deal with bigger binary programs and gain in precision while reconstructing our CFG.
The possible paths to explore are numerous among others we can already list few:
- Loop summarization (computing a parametrized formula capturing the precise effect of a loop without having to symbolically execute it).
- Expressions or paths simplification (when dealing with obfuscated software, one problem is to simplify the expressions or a path of the CFG while keeping the same semantics).
- Interprocedural analysis (take advantage of the decomposition of the program into procedures in order to perform the rebuild of the CFG in a modular way).
- Dealing with shared-library in a more efficient way (for now we are simply stubbing the external functions by hand, the idea would be to provide a better way to handle the stubbing procedure).
- Interaction with dynamic analysis (for now, Insight works with static-only analysis, the possibility to enrich the analysis with the possibility to execute dynamically the software and extract execution traces has to be investigated).
- ... many other possible ideas are still possible, contact me if you want have some proposals.
We are currently seeking for a Postdoc or a Research Engineering able to work on one or several of these topics and implements it into the Insight framework.
We are looking for a Postdoc or an Research Engineer for a 10-12 months position in Bordeaux, France. This position requires skills in OCaml, C/C++, Python and assembly, and a strong grounding in formal methods.
Contact: Emmanuel Fleury <emmanuel.fleury(at)u-bordeaux.fr>
