Software model checking is a verification technique which is widely used for checking temporal properties of software systems. Even though it is a property verification technique, its 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 orderings. 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 10 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 between software model checking and greybox fuzzing.
翻译:软件模式检查是一种核查技术, 它被广泛用于检查软件系统的时间属性。 尽管它是一种财产核查技术, 它在实际中通常的使用是“ 错误发现”, 也就是说, 发现侵犯时间属性的行为。 受此观察的驱使, 利用最近在模糊化方面的进展, 我们建立了一个灰盒模糊框架, 以查找违反线形时时时时逻辑( LTL) 属性的行为。 我们的框架将C/ C+++ 和一个 LTL 属性的相继程序作为输入。 它在状态化软件系统中发现LTL 属性的违规或反例迹; 但是, 它没有实现核查。 我们的工作大大扩展了灰盒的模糊模糊, 以见证任意复杂的事件。 我们注意到, 现有的Greedbox flzz 模糊方法仅限于看到到达一个位置, 或见证简单事件, 类似“ 免费” 。 与此同时, 我们的模型找到反光碟软件格式, 从而在特定预算中找到更多的反镜; 我们的LTL- Fzer 运行工具, 代表了我们所知道的“ 常规” 。