一句话:提出 SymTuner,通过在线学习自动调节符号执行的外部参数,提升分支覆盖与缺陷发现能力。
符号执行工具的外部参数(如符号参数、种子输入)会显著影响其性能,但参数空间巨大,人工调优即便对专家也很困难,实践中常依赖默认设置而错失更优表现。SymTuner 将待调参数空间作为输入,在符号执行过程中观察执行行为,并通过学习算法更新各参数空间的采样概率,从而自动学习并调整参数值,使工具无需人工配置即可运行。作者在 12 个开源 C 程序上用 KLEE 进行评估,结果显示 SymTuner 平均提升分支覆盖率 56%,并在这些程序的最新版本中比默认参数多发现 8 个缺陷。
We present SymTuner, a novel technique to automatically tune external parameters of symbolic execution. Practical symbolic execution tools have important external parameters (e.g., symbolic arguments, seed input) that critically affect their performance. Due to the huge parameter space, however, manually customizing those parameters is notoriously difficult even for experts. As a consequence, symbolic execution tools have typically been used in a suboptimal manner that, for example, simply relies on the default parameter settings of the tools and loses the opportunity for better performance. In this paper, we aim to change this situation by automatically configuring symbolic execution parameters. With SymTuner that takes parameter spaces to be tuned, symbolic executors are run without manual parameter configurations; instead, appropriate parameter values are learned and adjusted during symbolic execution. To achieve this, we present a learning algorithm that observes the behavior of symbolic execution and accordingly updates the sampling probability of each parameter space. We evaluated SymTuner with KLEE on 12 open-source C programs. The results show that SymTuner increases branch coverage of KLEE by 56% on average and finds 8 more bugs than KLEE with its default parameters over the latest releases of the programs.