The use of static analysis to detect malware in embedded systems

Malware is prolific and not always detected until the damage has occurred. The use of Formal Static Analysis techniques to ensure that software-based safety systems are free from compiler introduced errors is well established (Pavey, Winsborrow, 1995) [1]. This technique ensures that the executable binary code created by the compiler is mathematically equivalent to the original source code. This paper reports on extending this technique to detect malware inserted into executable code. The Source-Code Comparison process was originally developed by British Energy for the verification of the Primary Reactor Protection System software of the Sizewell `B´ Nuclear Power Plant. The process takes the executable binary file that is resident on the target computer and re-creates the equivalent assembler code using disassembler tools. This is then formally compared to the original source code using the MALPAS Compliance Analysis tool, and any discrepancies are revealed. The process has the ability to detect any executable binary code that cannot be traced back to the source code, and may therefore be used to detect the presence of malware in the executable. The paper reports on experiments conducted by Atkins to determine whether modern control executable software can be formally proven against the original code. The applicability of the process to software developed for general purpose operating systems (e.g. Windows) will also be evaluated.