File Parsing Vulnerability Detection with Symbolic Execution

Symbolic execution simulates program execution by replacing concrete values with symbolic variables for inputs. It could be used in software behavior analysis, vulnerability detection and software security assessment. In this paper, we analyze the path explosion problem encountered in vulnerability detection with the state-of-the-art symbolic execution technology for large scale file parsing programs. We also propose 4 alleviations to ease the problem, i.e. loop controlling, irrelevant path elimination, path selecting and parallel symbolic execution. Based on these alleviations, we implemented a prototype tool to detect file parsing vulnerability in large scale programs automatically, and evaluate it with a suit of benchmarks chosen from open source programs. Our tool detected not only all reported vulnerabilities of memory overflow in the benchmarks, but also some unreported vulnerabilities. The evaluation results show these alleviations could effectively ease the path explosion problem while analyzing large scale file parsing programs.