Search papers, labs, and topics across Lattice.
This paper introduces POVGEN, a neuro-symbolic framework designed to generate Proofs-of-Vulnerability (PoVs) for software vulnerabilities by leveraging semantic focusing and LLM-guided constraint reasoning with open-weight models. The method effectively localizes vulnerability-relevant regions and employs path-sensitive reachability analysis, achieving a PoV generation success rate of 78.98% on a benchmark, significantly surpassing traditional methods like fuzzing and symbolic execution. Notably, POVGEN not only identifies flaws in existing patches but also uncovers previously unreported vulnerabilities, demonstrating its practical utility in enhancing software security.
POVGEN generates Proofs-of-Vulnerability for 78.98% of cases, revealing flaws in existing patches and uncovering new vulnerabilities, all while minimizing costs.
Software vulnerabilities are persistent, but validating them remains difficult: a Proof-of-Vulnerability (PoV) requires a concrete input that triggers the vulnerable behavior, yet public triggering inputs are often unavailable for disclosed vulnerabilities. Existing techniques make different tradeoffs in effectiveness, scalability, cost, and controllability, leaving room for complementary designs. To complement them, we present POVGEN, a low-cost neuro-symbolic framework that makes PoV generation cost-effective via semantic focusing and LLM-guided constraint reasoning using open-weight models. POVGEN first localizes vulnerability-relevant regions (utilizing patch information if available), then performs path-sensitive reachability analysis, and finally generates PoVs by extracting and solving constraints with LLM-guided reasoning backed by an SMT solver. POVGEN successfully generates PoVs for 78.98% of vulnerabilities in a recent benchmark, outperforming fuzzing (up to 50.20%) and symbolic execution (2.45%). On 250 real-world CVEs without public PoVs, it generates valid PoVs for 74.80% of cases and reproduces 65.1% when without patch information. The fine-tuned open-weight models match frontier commercial LLMs on key sub-tasks (i.e., the core constraint-reasoning steps) while running locally at no per-sample API cost. Applying the generated PoVs revealed six flawed patches in disclosed CVEs (all subsequently fixed) and five previously unreported vulnerabilities (of which four have been confirmed and fixed by the developers).
