Research And Implementation Of Practical Concolic Execution Technique For Large Scale Software Systems

In recent years,with the rapid development of information technology,people pay more and more attention to the software security.Concolic execution is a software testing technology that effectively improves the automation degree of testing,playing a positive role in software security assurance.The goal of concolic execution is to automatically generate test cases to explore all feasible paths in the program,thereby detecting program vulnerabilities.Concolic execution has shown good effectiveness in detecting vulnerabilities in small applications.However,for some complex large programs,concolic execution cannot be scaled well because it faces serious state explosion problems.In particular,when performing a completely concolic execution of a large scale software system,it is often impossible to stop in an acceptable time.In this case,the number of feasible program states increases exponentially.Therefore,for large scale software systems,existing concolic execution technique can only explore a small part of the program states,and it is difficult to explore the deep program paths.This paper innovatively proposes a concolic execution technique suitable for large scale software systems.In order to mitigate the serious state explosion problem faced by concolic execution,we distinguish different symbolic memory and design different state generation strategies for the different symbolic memory to prioritize states that are more likely to trigger new paths.First,the correlation between symbolic memory and control flow is determined through static analysis,so as to propose the concept of critical symbolic memory and ordinary symbolic memory.Then,for critical symbolic memory and ordinary symbolic memory,we use different state generation strategies.Each value of critical symbolic memory triggers a new path,so a corresponding program state is generated for each possible value.For ordinary symbolic memory,we propose an adaptive symbolic variable value assignment algorithm based on the greedy algorithm.Under the guidance of path coverage,concrete value sequence of symbolic variable is obtained,and a corresponding state is generated for each value of the sequence.In this way,concolic execution technique we proposed can achieve higher path coverage during a shorter time,and can be extended to large scale software systems.We implement the above approach as a vulnerability detection system,Pracolic.The evaluation results can prove that Pracolic can alleviate state explosion problem,effectively extend to large scale software systems,and has practicability and effectiveness in detecting program vulnerabilities.