AutoSOUP: Safety-Oriented Unit Proof Generation for Component-level Memory-Safety Verification
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , , , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2026
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866916001097973760 |
|---|---|
| author | Amusuo, Paschal C. Calvo, Ricardo Anandayuvaraj, Dharun Lievre, Taylor Le Kolyakov, Kevin Jorgensen, Elijah Machiry, Aravind Davis, James C. |
| author_facet | Amusuo, Paschal C. Calvo, Ricardo Anandayuvaraj, Dharun Lievre, Taylor Le Kolyakov, Kevin Jorgensen, Elijah Machiry, Aravind Davis, James C. |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2605_10712 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | AutoSOUP: Safety-Oriented Unit Proof Generation for Component-level Memory-Safety Verification Amusuo, Paschal C. Calvo, Ricardo Anandayuvaraj, Dharun Lievre, Taylor Le Kolyakov, Kevin Jorgensen, Elijah Machiry, Aravind Davis, James C. Software Engineering Cryptography and Security D.2.4; F.3.1 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. |
| title | AutoSOUP: Safety-Oriented Unit Proof Generation for Component-level Memory-Safety Verification |
| topic | Software Engineering Cryptography and Security D.2.4; F.3.1 |
| url | https://arxiv.org/abs/2605.10712 |