Research On Security Vulnerability Detection Scheme Based On UEFI Firmware

As a new generation of computer firmware development standard,UEFI defines the interface specification between the hardware platform firmware and the operating system,which solves the bottleneck problem existing in the development of traditional computer firmware.At the same time,the program capacity of UEFI firmware increases geometrically.A large number of novel interfaces and driver loading modes based on C language make UEFI firmware exposed to a wider range of attacks.At present,UEFI firmware security vulnerability detection technology mainly includes fuzzy test,blot analysis,symbol execution.Fuzzy testing technology has low automation degree,low efficiency and low code coverage.Stain analysis technology requires extra system overhead and a lot of prior analysis,and the detection conditions are harsh.Symbol execution technology does not have high analytical accuracy because of its sensitivity to path and serious state explosion problems.To solve above problems,this paper USES the formalized method to form UEFI firmware module specification and verification,based on automata theory foundation of the existing security vulnerabilities in UEFI module properties respectively and UEFI module program control flow for formal modeling,the model to make use of model checking formal verification,to reduce the non-response rates,Increase code coverage and automation.The main work of this paper is as follows:Firstly,the UEFI development specification,code composition and compilation principle are studied and analyzed.According to the UEFI specification and the security problems in C language programming,the UEFI security vulnerability attribute description rules are constructed and the security vulnerability attribute library based on the UEFI firmware module is generated.The formalized modeling algorithm and modeling process of UEFI firmware module security vulnerability attributes are designed by using the formalized method,and the security vulnerability attributes are transformed into the formalized specification to determine the Deterministic Finite Automaton(DFA)representation.The simple security vulnerability attributes are merged into complex security vulnerability attributes to realize the reuse of security vulnerability attributes.Secondly,formalized verification methods and processes are studied,and model detection is used to complete security vulnerability detection of UEFI firmware.In order to alleviate the state explosion in the process of model detection,the code control flow diagram model of UEFI module is designed by using the idea of data abstraction.The code of UEFI module is abstracted into the corresponding program control flow diagram model,and the state is compressed according to the security vulnerability attribute model.Then,the control flow diagram model is transformed into the UEFI module code formalized model represented by PDA.Finally,the UEFI module code model is combined with the security vulnerability attribute model,and the model detection algorithm is used to complete the security vulnerability detection of the UEFI module code.Finally,based on the UEFI module code and the formalized model of security vulnerability attributes,the UEFI module security vulnerability detection prototype is designed and implemented.The test cases of UEFI modules were designed,multiple types of security vulnerabilities were implanted,and the core functional modules were tested.According to the experimental analysis results,the prototype effectively alleviated the problem of state explosion in the process of model detection,and the detection indexes such as missing alarm rate,performance,detectable code size and code coverage rate met the design requirements.