BINCOA (BINary COde Analysis) is a 3-year basic research project funded by the French research agency ANR (ARPEGE 2008 program). The project began on january 2009 and it will end in january 2012. BINCOA is a collaborative project involving

  • CEA LIST
  • Uni. Bordeaux 1 (LABRI)
  • Uni. Paris 7 (LIAFA)
  • EDF
  • Sagem
  • Trusted Lab




Program analysis at the level of binary code rather than source code is a recently emerging issue in the academic community. Several potential applications have been identified, for example verification of off-the-shelf software components, verification of optimized code, verification of source code containing embedded assembly language, virus analysis and detection of typical vulnerabilities such as call stack overflows.

Binary programs present original problems not yet solved in the state of the art:

  • no syntactical control flow information,
  • unstructured control flow,
  • low level semantics of instructions.

The current project offers to contribute progress to the state of the art. We position ourselves in a fault-detection perspective rather than in a strict formal verification setting. On the other hand, we want to stay as close to the original problem as possible by avoiding exceedingly strong modeling hypotheses, in order to ensure that the techniques developed in the project will really be applicable to industrial software. We plan to tackle the problem with original combinations of concepts coming from several research communities : symbolic computation of the reachable state space (model checking), symbolic execution of paths (test case generation) and dynamic execution (processor simulation). Part of the results will be implemented, either directly in OSMOSE or in other autonomous prototypes.

The main goals of the project are:

  • to identify interesting models and properties for binary code analysis,
  • to develop automated analysis procedures,
  • to implement some of the results in prototypes and conduct experiments.




Main results: (more details can be found in the "Publication" section)

Concepts, methods and algorithms

  • Dynamic Bitvector Automata (DBA), a concise and natural formal model for binary-level program analysis -- see CAV 2011 paper
  • a safe, precise and efficient approach to CFG recovery from executable files (i.e. dynamic jump resolution), and promising experimental results over real-life safety-critical programs -- see VMCAI 2011 paper
  • a new method for solving bitvector formulas without bitbasting -- see TACAS 2010 paper
  • a novel and promising approach to (signature-based) polymorphic virus detection, built upon binary-level static analysis -- see NSS 2011 paper
  • an efficient symbolic procedure to the model checking of pushdown systems and CTL formulas, with early applications to (behavioral) virus detection -- see CONCUR 2011 and TACAS 2012 papers

Prototypes

  • OSMOSE (CEA), a test data generation tool working from executable files
  • CFGBuilder (CEA), a static analysis tool for CFG recovery from executable files
  • DBA toolkit, a small open-source OCaml library for DBA manipulation lien
  • INSIGHT (LABRI), a binary-level static analysis tool
  • a model checker (LIAFA) for pushdown systems and CTL temporal formula




News:

  • january 2012: Dagstuhl seminar "Analysis of executables: benefits and challenges" lien
  • january 2012: ANR review of the project (successful!)
Last modified 5 years ago Last modified on Mar 16, 2012 11:15:19 AM
Agence Nationale de la Recherche
ANR
ARPEGE
ARPEGE
System@tic
System@tic