Primary Investigator:
Jamie Davis

Project Members
Paschal C. Amusuo Ricardo Calvo Dharun Anandayuvaraj Kevin Kolyokav Taylor Le Lievre Elijah Jorgensen Aravind Machiry James C. Davis

Memory-safety errors continue to underlie many high-impact security failures in low-level and embedded software. While bounded model checking can provide precise memory-safety guarantees, its adoption is limited by the cost of constructing suitable proof harnesses. Unlike test drivers or deductive specifications, effective BMC harnesses require symbolic initialization and carefully scoped assumptions specific to the memory-safety defects of interest. We introduce AutoUP, a system that automates proof harness construction for component-level memory-safety verification using bounded model checking. AutoUP is based on the insight that vulnerability discovery and verification often require only minimal bounds and environment models, provided they are chosen systematically and validated incrementally. Our hybrid system combines deterministic refinement techniques for loop bounds and environment assumptions with LLM-based code understanding, and enforces determinism through progress checks. An evaluation on three major embedded operating systems shows that AutoUP generates reusable, low-cost proof harnesses that expose real memory-safety defects in substantial real-world codebases.