A pioneering approach to the checking of binary code

The techniques used when automatically checking software programs by analyzing the software itself are generally based on an analysis of the program’s source code (e.g. the LIST’s Frama-C and PathCrawler tools) or a model of the program (e.g. the LIST’s GaTEL and Ag@tha tools). No method of automatically checking semantics currently uses the final product, in other words, the binary code alone. This is because it is more difficult to analyze binary code than it is to analyze more abstract formalisms, since it introduces special problems such as the total lack of definitive information on the executable’s structure or its handling of extremely low level control management mechanisms (exceptions, computed jumps, stack handling, etc.). As a result, a preference for the analysis of high-level formalisms is highly understandable.
There is, however, a considerable industrial need for safety- or security-related analysis based on the software’s binary code alone. Among other applications, these techniques are essential in understanding the source of computer attacks (viruses and Trojan horses), detecting vulnerabilities resulting from code compilation or optimization (compiler weaknesses, order of calculation, etc.), certifying “off the shelf” software components (whose source code is not available) or checking programs partly or entirely written in assembler or a language for which no modern analysis tool exists (Pascal, Fortran, Cobol, ADA, etc.).
In reply to EdF’s stated need for certification of components purchased “off the shelf,” LIST recently developed a highly innovative method of checking binary code. The OSMOSE tool, which is developed from the techniques already used within LIST to generate tests for C language programs, can automatically reconstruct a model of the original program’s control structure and generate tests covering the binary code. One of OSMOSE’s main advantages lies in its genericity regarding which instruction set the analyzed code is based upon: the code is translated (by a dedicated module) into a representation within OSMOSE, and it is this representation which is then analyzed. OSMOSE can be used to handle a new instruction set simply by developing the appropriate translation module.
As a result of the OSMOSE tool’s successful development, the quality of LIST’s research has been recognized in two IEEE publications†; in 2010, EDF wishes to begin using OSMOSE to expand its security files on programs initially written in 6800 assembler and still in operation but requiring partial updates (as part of the third ten-yearly inspection of 1300MW nuclear plants).
LIST’s approach is a world first in testing the security of programs by checking the binary code alone. The ANR BINCOA (2009-2012) project, which is managed by LIST, will provide an ideal opportunity for creating and building a community of academic and industrial players interested in this subject, with the aim of rapidly reaching critical mass and achieving worldwide recognition. Trusted Labs (the smartcard security audit company) and Hispano-Suiza (the aeronautics OEM supplier) have already expressed an interest in OSMOSE and joined the BINCOA project.