Verification of Executables

Field: machine code analysis, concolic execution, IR recovery
Applications: COTS, mobile code, malware, legacy code


Verification is usually performed on  a high-level view of the software, either specification or program source code. However in certain circumstances verification is more relevant  when performed at the machine code level, either the source code is not available (COTS, mobile code, malware) or the compiler chain cannot be trusted (e.g. strong safety/security requirements and optimising compilers). However verification of native code programs is much more difficult than verification of higher-level formalisms, for at least three reasons: low-level semantics on data, low-level semantics on control and IR recovery (see publications for more details).

The OSMOSE prototype

We develop a prototype named OSMOSE for (semi) automatic analysis of native code programs. The tool takes as input an executable file, an architecture/ISA id and a modelling of the external environment (for embedded systems). Output are a high-level description of the executable behaviour (control-flow graph, call graph, etc.) and a test suite achieving some predefined coverage objectives.   

We rely on four major technologies:


A few slides