Fully automated and program-adaptive parameter tuning for symbolic execution

다국어 초록 (Multilingual Abstract)

We present PARASUIT, a program–adaptive technique that enhances symbolic execution by autonomously adjusting its parameters tailored to the program under test. Modern symbolic execution tools are typically equipped with various external parameters to effectively test real–world programs. However, the need for users to fine–tune a multitude of parameters for optimal testing outcomes makes these tools harder to use and limits their potential benefits. Despite recent efforts to automate this tuning process, existing techniques remain semi–automatic and non–adaptive; they still require significant manual intervention and cannot dynamically identify relevant parameters or assign appropriate values suited for the target program. The goal of this thesis is to fully automate the parameter adjustment process for symbolic execution tools, thereby maximizing their performance. To this end, PARASUIT begins by automatically identifying all available parameters in the symbolic execution tool and evaluating each parameter’s impact through interactions with the tool. It then applies a specialized algorithm to iteratively select promising parameters, construct sampling spaces for each, and update their sampling probabilities based on data accumulated from symbolic execution runs using sampled parameter values. We implemented PARASUIT on KLEE and assessed it across 12 open–source C programs. The results demonstrate that PARASUIT significantly outperforms both semi–automatic and manual tuning methods, achieving an average of 10% and 73% higher branch coverage, respectively. Remarkably, PARASUIT identified 11 unique bugs, four of which were exclusively discovered by PARASUIT.

국문 초록 (Abstract)

본 논문에서는 테스트 대상 프로그램에 맞춰 기호 실행의 파라미터를 자동으로 조정하는 프로그램 적응형 기술을 제안한다. 현대의 기호 실행 도구들은 실제 프로그램 테스트를 효과적으로 수행하기 위해 다양한 외부 파라미터를 제공하지만, 최적의 테스트 결과를 얻기 위해 사용자가 수많은 파라미터를 직접 조정해야 하는 점은 도구의 활용도를 제한하고 사용 편의성을 저해한다. 최근 이러한 파라미터 조정 과정을 자동화하려는 여러 시도가 있었으나, 기존 기술은 여전히 반자동적이며 비적응적이다. 즉, 여전히 많은 수동 개입이 필요하고, 대상 프로그램에 적합한 파라미터를 동적으로 식별하거나 적절한 값을 자동으로 설정하지 못한다.

본 논문의 목표는 기호 실행 도구의 파라미터 조정 과정을 완전히 자동화함으로써, 그 성능을 극대화하는 것이다. 이를 위해 본 기술은 먼저 기호 실행 도구 내 사용 가능한 모든 파라미터를 자동으로 식별하고, 각 파라미터가 도구에 미치는 영향을 분석한다. 이후, 특화된 알고리즘을 통해 유망한 파라미터를 반복적으로 선택하고, 각 파라미터의 샘플 공간을 구성한 후, 샘플 공간 내에서 확률적으로 값을 생성한다.

본 기술은 대표적인 기호 실행 도구인 KLEE 위에 구현되었으며, 12개의 오픈소스 C 프로그램을 대상으로 평가되었다. 실험 결과, 본 기술은 기존의 반자동 및 수동 튜닝 방식에 비해 각각 평균 10% 및 73% 더 높은 분기 커버리지를 달성했으며, 총 11개의 오류를 발견하였다.

목차 (Table of Contents)

• Chapter 1. Introduction 1
• 1. Contribution 5
• Chapter 2. Preliminaries 7
• 1. Symbolic Execution and Its Parameters 7
• 2. Approaches for Tuning Parameters and Limitations 9
• Chapter 3. Our Approach 12
• 1. Overview 12
• 2. PARASUIT 13
• 3. Parameter Selection 17
• 4. Value Sampling 20
• Chapter 4. Experiments 25
• 1. Experimental Settings 26
• 2. Branch Coverage 27
• 3. BugFinding Ability 30
• 4. Efficacy of Two Stages in PARASUIT 32
• 5. Analysis of Parameter Selection and Value Sampling 36
• 6. Generality 43
• 7. Effect of Hyperparameters 44
• 8. Discussions 48
• 9. Threats to Validity 52
• Chapter 5. Related Work 54
• Chapter 6. Conclusion 57
• References 58
• Korean Abstract 71