一句话：提出 LTL-Fuzzer，将灰盒模糊测试扩展到寻找线性时序逻辑性质违反的反例。
软件模型检测与运行时验证常用于检查时序性质，但实践中多用于缺陷发现。本文提出 LTL-Fuzzer，一个基于 AFL 的灰盒模糊测试框架：输入 C/C++ 顺序程序与 LTL 性质，搜索违反该性质的反例轨迹（不承诺完成验证）。它把 directed greybox fuzzing 从到达特定位置或简单事件序扩展到任意复杂事件序。在 OpenSSL、Telnet 等协议实现上，LTL-Fuzzer 比模型检测器在固定时间预算内更快找到更多反例，复现已知 CVE，并从 RFC 提取性质发现 15 个零日缺陷（12 个获 CVE），覆盖 safety 与 liveness 性质违反，展示了模型检测、运行时验证与灰盒模糊测试的协同潜力。
Software model checking as well as runtime verification are verification techniques which are widely used for checking temporal properties of software systems. Even though they are property verification techniques, their common usage in practice is in “bug finding”, that is, finding violations of temporal properties. Motivated by this observation and leveraging the recent progress in fuzzing, we build a greybox fuzzing framework to find violations of Linear-time Temporal Logic (LTL) properties. Our framework takes as input a sequential program written in C/C++, and an LTL property. It finds violations, or counterexample traces, of the LTL property in stateful software systems; however, it does not achieve verification. Our work substantially extends directed greybox fuzzing to witness arbitrarily complex event or-derings. We note that existing directed greybox fuzzing approaches are limited to witnessing reaching a location or witnessing simple event orderings like use-after-free. At the same time, compared to model checkers, our approach finds the counterexamples faster, thereby finding more counterexamples within a given time budget. Our LTL-FUZZER tool, built on top of the AFL fuzzer, is shown to be effective in detecting bugs in well-known protocol implementations, such as OpenSSL and Telnet. We use LTL-FUZZER to reproduce known vulnerabilities (CVEs), to find 15 zero-day bugs by checking properties extracted from RFCs (for which 12 CVEs have been assigned), and to find violations of both safety as well as liveness properties in real-world protocol implementations. Our work represents a practical advance over software model checkers - while simultaneously representing a conceptual advance over existing greybox fuzzers. Our work thus provides a starting point for understanding the unexplored synergies among software model checking, runtime verification and greybox fuzzing.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@inproceedings{MengDLBR22,
title = {Linear-time temporal logic guided greybox fuzzing},
author = {Ruijie Meng and Zhen Dong and Jialin Li and Ivan Beschastnikh and Abhik Roychoudhury},
booktitle = {ICSE},
year = {2022},
doi = {10.1145/3510003.3510082}
}