HornFuzz：面向CHC求解器的模糊测试
软件工程
2023-06-09 v2
摘要
许多先进的程序分析与验证方法基于求解约束 Horn 子句（CHC）系统。测试CHC求解器非常重要，因为其工作的正确性决定了被分析程序中的缺陷是被检出还是被遗漏。模糊测试（fuzzing）是一种成熟且高效的自动化软件测试方法：分析程序对随机输入数据的反应。目前尚无针对CHC求解器的模糊器，而针对SMT求解器的模糊器在CHC求解器测试中效率不高，因为它们未考虑CHC的特性。本文中，我们提出HornFuzz，一种基于蜕变测试思想的、用于检测CHC求解器中缺陷的变异型灰盒模糊测试技术。我们在性能最高的CHC求解器之一Spacer上评估了我们的模糊器，并在Spacer中发现了若干缺陷。特别是，某些发现的问题十分严重，需要对求解器进行重大修改才能修复。
引用
@article{arxiv.2306.04281,
title = {HornFuzz: Fuzzing CHC solvers},
author = {Anzhela Sukhanova and Valentyn Sobol},
journal= {arXiv preprint arXiv:2306.04281},
year = {2023}
}