Research On Concolic Execution For Firmware Program

In recent years,in the context of increasing PC software protection measures,embedded device firmware has become the preferred target of cyber attackers,and attacks against firmware programs have emerged in endlessly.As an important program analysis technology,concolic execution has the capabilities of automated program state space exploration,test case generation,vulnerability detection,etc.How to apply concolic execution technology to the field of firmware analysis is one of the current research hotspots in the field of network security,and is of great significance for improving the security of embedded devices.This article takes embedded Linux system firmware as the research object,and studies the methods and key technologies related to the concolic execution for firmware programs.The main work and contributions are as follows:1.We present a novel concolic execution system design for firmware programs.The debug computer uses the debugging instrumentation method to monitor the concrete execution of the firmware program on the device and then extracts the executed basic block code from the device memory.Symbolic engine converts basic block into an intermediate representation after semantic lifting and executes the intermediate representation symbolly.During the execution we can obtain the test cases after solving the path constraint.The selected test case can be injected into the device memory,which in turn controls the execution path of the firmware program and realizes the exploration of the program state space.The design avoids the inaccuracies and instability of the common firmware symbolic execution system based on software simulation,and has the characteristics of on-demand symbolic execution of firmware code fragments and the support of multiple embedded processor architecture firmware symbolic execution.2.We have implemented a prototype of the concolic execution system F3 CE for firmware programs.F3 CE implements dynamic binary instrumentation of firmware programs based on GDB remote debugging and extended script technology to monitor the execution of firmware programs and extract runtime information.F3 CE semantically lift firmware program instructions and implement the symbolic engine which execute on VEX intermediate representations based on VEX intermediate representations.F3 CE extracts the data page of the firmware program as needed and converts it into architecture-independent symbol storage based on backup storage's ability of symbolizing the firmware program memory;We implement depth-first and path guidance two strategies to achieve the path exploration function,so F3 CE can control the firmware concrete execution path.3.We conduct detail tests of the concolic execution system prototype F3 CE.We test the basic functions of F3CE's dynamic binary instrumentation,instruction conversion to intermediate representation,symbolic execution,symbolic data introduction,path constraint extraction and solution,and verify F3CE's ability of cross-platform concolic execution.First,the unit test was performed on the binary instrumentation module and the intermediate representation lifter to prove the effectiveness of the key modules.Then the basic functions of the concolic execution framework F3 CE were tested to verify the framework's ability to execute symbols under various architectures,and it is proved that the solution in this paper solves the problem of environment modeling when symbolic execution is used for firmware program analysis.Finally,combined with static analysis,the framework's path exploration algorithm is tested,which proves that the solution of this paper partially alleviates the path explosion problem.