The security flaw in firmware is good concealing, which is hard to be detected and removed. The consequences of the security flaw in firmware could also be devastating. Currently, the security flaw in firmware has been one of the most important factors which threaten the information system security. Consequently, research on the analysis for the security flaw in firmware can help to protect the rock-bottom safety of information system. So the thesis has important application value and research significance.Taking the research on National"863"Project (2009AA01Z434) as background, this thesis selects the firmware of the chips in current electric devices as the object, and focuses on the research on the formal description and analysis methods of malicious behavior in firmware. The main contents and contributions of this thesis are as follows:1. The formal description of malicious behavior in firmware. Assimilating the malicious behavior description method based on specification, considering the characteristics of firmware's structure and function and the method of hardware resources access control, the thesis proposes a formal description method of malicious behavior in firmware which lays a good foundation for the atuomatical analysis on malicious behavior in firmware.2. The thesis proposes an analysis method for malicious behavior in firmware based on the multi-path technology. This analysis method, which could increase the code coverage rate, gets the multi-path branch condition of firmware with data dependency analysis and expression replacement, and generates input vectors with path condition analysis and expression calculation. Moreover, the method, which could get comprehensive behavior information of firmware, could analyze the access hardware resources behaviors of firmware based on the formal description method for malicious behavior.3. A prototype system, amPro-FMBAS, for malicious behavior analysis of firmware is designed and implemented on the basis of the research results. The thesis tests and analyzes the prototype system with several firmware samples with security flaw, which proves the correctness of the formal description and effectiveness of the multi-path analysis. |