AutoSOUP: Safety-Oriented Unit Proof Generation for Component-level Memory-Safety Verification
For developers of low-level and embedded systems, AutoSOUP reduces the manual expertise required for memory-safety verification, though it is an incremental improvement over existing automation.
AutoSOUP automates component-level memory-safety verification by generating Safety-Oriented Unit Proofs, using a hybrid LLM and deterministic synthesis approach. It successfully automates verification and exposes vulnerabilities in previously verified components.
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.