Symbolic Execution Of The DSP Programs

Embedded system is a specialized computer system,by means of cutting,the combination of hardware and software resources,can satisfy the performance index of user requirements,including functional requirements,reliability,cost,volume,power consumption and so on.In embedded system equipment,there is a device used for signal analysis,extraction,change and other processing,known as digital signal processor(Digital-Signal Processor DSP).Modern communication is characterized by digital signal,therefore,DSP is playing an increasingly large role in promoting the digitization of information processing,and with the development of communication technology,it will play a greater role.At the same time,because of the development of DSP in digital and network,the security of DSP becomes an urgent problem to be solved.In order to solve this problem,it is necessary to carry out software testing on DSP.There are many kinds of software testing methods,program analysis is one of the most important,it can effectively improve the credibility of the software.This paper uses symbolic execution,which is a kind of accurate program analysis technology,because it has the advantages of good feasibility,no false alarm and wide application,and it has been widely concerned and applied.However,the current symbolic execution technology and tools in the analysis of the effect and efficiency of the DSP program,there are many deficiencies.There are two main reasons,one is because the DSP requires real-time data exchange with the outside world,so there is a random trigger interrupt,the interrupt occurs,will produce a lot of general program analysis is difficult to find loopholes,the symbolic execution tool can not solve this problem very well.Second,the DSP program is a lot of problems are logical,and the general symbolic execution technology can only find the operation of the program error,and can not find the logic of the DSP error.In view of the above two problems,this paper puts forward the method of DSP interrupt handling and the fixed point monitoring technology.Based on symbolic execution technology,the interrupt function is inserted,the interrupt function is realized,and the insertion density of the interrupt function is controlled to improve the efficiency of program analysis.On this basis,according to the user's guiding,can be on the same path conditions,the variables in different paths to detect,there may be a point of defect to record.In this paper,the above two algorithms are implemented in KLEE,and the experiment is carried out.Experimental results show that the two methods proposed in this paper can more effectively find the defects in the DSP program compared to the existing symbolic execution techniques.