The firmware code is different from the software run in application layer.The defects are hidden more deeply. It is harder to detect and remove.This defect can damage the hardware directly. The detection and defense for firmware defects has aroused attention and research gradually. Research in this respect can guarantee the whole information system run normally from the hardware layer.lt has great significance both for business and academic.In this paper, firmware program stored in the hardware chip is the research object. This thesis focuses on the research on the formal description of malicious behavior in firmware and analysis methods of malicious behavior in firmware. The main contributions of this paper are as follows:1This paper describes several common description methods for firmware malicious behavior, and discusses the advantages and disadvantages of various methods. Drawing on previous malicious behavior based on the standard description method, a new method is proposed to describe the formal.2This paper presents a multipath for the firmware code analysis method. This method is based on the formal theory to describe the firmware malicious behavior and the characteristics of the firmware code. Data dependence analysis and expression replacement to get firmware multi-path branch condition is the basic thought. Based on this idea, we can solve two key problems---the channel condition analysis and expression the input vectors. The information of firmware code behavior can be accessed more comprehensively, and judge whether the firmware code behavior is malicious.3According to the theory of malicious behavior of the formalized description of the firmware code and multi-channel analysis method, we design a technical verification system named racPE-FMBAS. The technical verification system take racPE as a platform which is developed independently by our unit. We build a legitimate firmware behavior database and write a multi-path analysis plug-in.Finally the theory and method are proposed to be correct and effective. |