AutoSOUP: Safety-Oriented Unit Proof Generation for Component-level Memory-Safety Verification

TL;DR

AutoSOUP automates component-level memory-safety verification in low-level software, combining formal proofs with LLMs to improve automation and reliability in embedded systems.

Contribution

It introduces a novel system that formalizes safety proofs as artifacts and combines deterministic synthesis with LLMs for automated verification.

Findings

AutoSOUP successfully automates memory-safety verification tasks.

The system can expose vulnerabilities in verified components.

It characterizes assumptions and guarantees of the generated proofs.

Abstract

Memory-safety errors remain a persistent source of zero-day vulnerabilities in low-level software. The problem is especially acute in embedded systems, where hardware protections are often limited and dynamic analysis is difficult to apply effectively. Memory-safety verification can provide stronger assurance by proving the absence of such errors or exposing violations when they exist. However, current verification workflows remain largely manual and require substantial specialized expertise, limiting their adoption in practice. We present AutoSOUP, a system for automating component-level memory-safety verification through Safety-Oriented Unit Proofs. We formalize these unit proofs as artifacts that encode verification choices (scope, loop bounds, and environment models) for verifying safety properties, and introduce three techniques for deriving them automatically. To overcome the limitations of existing automation approaches, we further introduce LLM-As-Function-Call, a hybrid architecture that combines deterministic program synthesis with LLMs to automate these techniques and produce justifiable unit proofs. We evaluate AutoSOUP by assessing its ability to automate memory-safety verification and expose vulnerabilities in verified components, and we characterize the assumptions and guarantees of the resulting proofs.