Lancet: A Formalization Framework for Crash and Exploit Pathology

Vulnerability and exploit analysis are at the heart of soft- ware 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 differ- entiate between various types of vulnerabilities and exploit primitives even in the presence of memory corruption. Addi- tionally, we developed two downstream tools, FCS and EPF, to demonstrate how security analysts can use Lancet for de- tailed crash and exploit analysis. FCS serves as a fast crash triaging tool, aiding patch synthesis in our winning system in the DARPA AIxCC semi-final, while EPF fingerprints the transition of exploitation primitives to facilitate exploit analy- sis. Experiment results show that both tools are efficient and effective.