Research On GCC Compiler Security Verification Methods

Compiler is one of the most important pieces of basic computer software in addition with operating system and database systems. They are the key infrastructures of computer system software. As the producer of all software, the security, reliability and stability attributes of compiler are very important. Especially in the situation of high confidential software environment, we must prove that the machine code which compiler produced is totally accordant with the source code without any insertion of malicious code in order to guarantee transparency and logical correctness of compiler behavior.This paper first reviewed all the recent research work in software verification area, especially in compiler verification, including formal method of verification, model check, object file logical comparison, analysis and discuss the advantage and disadvantage in both theory and practice of these method. This paper mainly focus on the question: does the compiler insert any malicious code or back door program into the output object file?We propose two compiler verification methods in this paper: compiler source code analysis and comparison method and control flow graph logical comparison method.In the first method, as in GCC, we try to classify all the functions in GCC source code into two categories: for those functions that will modify the input data and will affect the output result of the compiler, we label them as category one; For those functions that will not modify the input data and will not affect the output result of the compiler, we label them as category two.For category two, we are supposed to save all the input data before getting into the function, and then compare all the input data after function return with the data saved before. If they are identical, then we prove that the function is safe and will not affect the output result. For category one, we manually check these functions and re-implement all the function by an independent group of people, then we compare all the input data before and after function call with these two versions of the function implementation: the original one and the re-implemented. If they are identical, then we prove that the function is safe and will not affect the output result.In the second method, we try to compare the control flow graph of the source code and the output object file by the compiler. First, we use lex & yacc to extract the control flow graph of the source code, then we use a tool developed for this paper to extract the control flow graph of the object file, then we reduce the both graphs and use isomorphism algorithm to compare these two graphs. If they are isomorphism, then we prove that the compiler is safe.Finally, we propose a combination method of these two above. On one side, this will largely decrease the workload of compiler verification, on the other side, it also prove the completeness of compiler verification. The method we proposed in the paper can be widely used in other compiler.