HyPFuzz：形式化辅助的处理器模糊测试
HyPFuzz: Formal-Assisted Processor Fuzzing
AI总结：
提出混合模糊测试器HyPFuzz，利用形式化验证工具优化时空调度以测试处理器难以到达的设计空间，在五个开源处理器上发现三个新漏洞并实现11.68倍覆盖率提升。
摘要：
近期研究表明，硬件模糊测试器能有效检测现代处理器中的安全漏洞。然而，现有的硬件模糊测试器难以对难以到达的设计空间进行有效测试。因此，这些模糊测试器无法有效测试处理器中安全关键的控流和数据流逻辑，从而遗漏安全漏洞。为应对这一挑战，我们提出了HyPFuzz，这是一种利用形式化验证工具协助模糊测试处理器中难以到达部分的混合模糊测试器。为提升HyPFuzz的有效性，我们在时间和空间上进行了优化。首先，我们开发了一种调度策略，以防止形式化工具和模糊测试器的能力被低度或过度利用。其次，我们开发了启发式策略，以在设计空间中选择目标点供形式化工具针对。我们在五个广泛使用的开源处理器上评估了HyPFuzz。HyPFuzz检测出了最新处理器模糊测试器所检测到的所有漏洞，并发现了三个此前被广泛模糊测试和形式化验证遗漏的新漏洞。这促成了两个新的通用漏洞披露（CVE）条目。HyPFuzz还实现了比最新处理器模糊测试器快11.68倍的覆盖率。
英文摘要：
Recent research has shown that hardware fuzzers can effectively detect security vulnerabilities in modern processors. However, existing hardware fuzzers do not fuzz well the hard-to-reach design spaces. Consequently, these fuzzers cannot effectively fuzz security-critical control- and data-flow logic in the processors, hence missing security vulnerabilities. To tackle this challenge, we present HyPFuzz, a hybrid fuzzer that leverages formal verification tools to help fuzz the hard-to-reach part of the processors. To increase the effectiveness of HyPFuzz, we perform optimizations in time and space. First, we develop a scheduling strategy to prevent under- or over-utilization of the capabilities of formal tools and fuzzers. Second, we develop heuristic strategies to select points in the design space for the formal tool to target. We evaluate HyPFuzz on five widely-used open-source processors. HyPFuzz detected all the vulnerabilities detected by the most recent processor fuzzer and found three new vulnerabilities that were missed by previous extensive fuzzing and formal verification. This led to two new common vulnerabilities and exposures (CVE) entries. HyPFuzz also achieves 11.68$\times$ faster coverage than the most recent processor fuzzer.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
