使用开放权重模型生成神经符号漏洞证明

软件漏洞是持久存在的，但验证它们仍然很困难：漏洞证明 (PoV) 需要触发易受攻击行为的具体输入，但对于已披露的漏洞，公共触发输入通常不可用。现有技术在有效性、可扩展性、成本和可控性方面做出了不同的权衡，为互补设计留下了空间。为了补充它们，我们提出了 POVGEN，这是一种低成本的神经符号框架，它通过使用开放权重模型的语义聚焦和 LLM 引导的约束推理，使 PoV 生成具有成本效益。 POVGEN 首先定位与漏洞相关的区域（如果可用，则利用补丁信息），然后执行路径敏感的可达性分析，最后通过使用由 SMT 求解器支持的 LLM 引导推理提取和求解约束来生成 PoV。 POVGEN 在最近的基准测试中成功为 78.98% 的漏洞生成 PoV，优于模糊测试（高达 50.20%）和符号执行（2.45%）。在 250 个没有公共 PoV 的现实世界 CVE 上，它为 74.80% 的情况生成有效的 PoV，在没有补丁信息的情况下重现 65.1%。经过微调的开放权重模型在关键子任务（即核心约束推理步骤）上与前沿商业 LLM 相匹配，同时在本地运行，无需每样本 API 成本。应用生成的 PoV 发现已披露的 CVE 中有 6 个有缺陷的补丁（随后全部修复）和 5 个之前未报告的漏洞（其中 4 个已由开发人员确认并修复）。