Lancet: A Formalization Framework for Crash and Exploit Pathology

Vulnerability and exploit analysis are at the heart of software security research and practice. However, a formalization framework for dissecting the cause, development, and impact of common software errors has been missing. To address this gap, we introduce Lancet, a formalization framework that reliably tracks three distinct types of ownership within its operational semantics that can be used to identify and differentiate between various types of vulnerabilities and exploit primitives even in the presence of memory corruption. Additionally, we developed two downstream tools, FCS and EPF, to demonstrate how security analysts can use Lancet for detailed crash and exploit analysis. FCS serves as a fast crash triaging tool, aiding patch synthesis in our system, which was selected as one of the winning teams in the DARPA AIxCC semi-final, while EPF fingerprints the transition of exploitation primitives to facilitate exploit analysis. Experiment results show that both tools are efficient and effective. 1 Distinct from Rust ownership rules (See Section 3.1