Research On Firmware Malicious Code Detection Technology Based On Model Checking

The microcontroller is the core components of electronic equipment. The detection on themalicious code in microcontroller is an important part of security analysis of electronicequipment. Studies on firmware malicious code detection is conducive to remove the securityrisks in equipments. Meanwhile, it contributes to troubleshooting and maintenance of electronicequipment.Taking the research on National "863" Project (2009AA01Z434) as background, the thesisanalyzes the malicious functions mechanism of firmware code based on the features of firmware,and mainly studies on detection method of firmware malicious code, and achieves effectivedetection of firmware malicious code using model checking techniques.Major contributions and innovations endeavored in this thesis are as follows:1. A Kripke structure generation algorithm is presented, which combines control flowanalysis and data flow analysis. Aiming at key problems during the generation of Kripkestructure, such as indirect jump, indirect store, call return, interrupt and time sequence, etc., thealgorithm successfully resolves these problem using critical methods such as analysis of thedetermined value of variables, interval analysis and quick bitwise operation.2. The quick bitwise operation algorithm is proposed, which is a kind of variable intervalanalysis method for bitwise operation. This algorithm includes the variable’s Uncertainty BitForm(UBF) computing algorithm, the bitwise operation algorithm for UBF and the intervalgenerated algorithm, which is used to improve the computational efficiency of variable intervalanalysis due to the coexistence of two different operation: byte-level and bit-level in thefirmware code. The experimental results show that the proposed algorithm is more efficient thaniterative algorithm with variable range large, and its time-consuming is stable, which shows adownward trend when the variable range expands.3. The prototype system FPAnalyzer is designed and implemented for firmware maliciouscode detection based on model checking. The experimental results show that the system cansuccessfully detect the malicious code, and verify the correctness and validity of this study.