AutoSOUP: Safety-Oriented Unit Proof Generation for Component-level Memory-Safety Verification
Authors:
Paschal C. Amusuo,
Ricardo Calvo,
Dharun Anandayuvaraj,
Taylor Le Lievre,
Kevin Kolyakov,
Elijah Jorgensen,
Aravind Machiry,
James C. Davis
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, cu…
▽ More
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.
△ Less
Submitted 11 May, 2026;
originally announced May 2026.
LEGOS-SLEEC: Tool for Formalizing and Analyzing Normative Requirements
Authors:
Kevin Kolyakov,
Lina Marsso,
Nick Feng,
Junwei Quan,
Marsha Chechik
Abstract:
Systems interacting with humans, such as assistive robots or chatbots, are increasingly integrated into our society. To prevent these systems from causing social, legal, ethical, empathetic, or cultural (SLEEC) harms, normative requirements specify the permissible range of their behaviors. These requirements encompass both functional and non-functional aspects and are defined with respect to time.…
▽ More
Systems interacting with humans, such as assistive robots or chatbots, are increasingly integrated into our society. To prevent these systems from causing social, legal, ethical, empathetic, or cultural (SLEEC) harms, normative requirements specify the permissible range of their behaviors. These requirements encompass both functional and non-functional aspects and are defined with respect to time. Typically, these requirements are specified by stakeholders from a broad range of fields, such as lawyers, ethicists, or philosophers, who may lack technical expertise. Because such stakeholders often have different goals, responsibilities, and objectives, ensuring that these requirements are well-formed is crucial. SLEEC DSL, a domain-specific language resembling natural language, has been developed to formalize these requirements as SLEEC rules. In this paper, we present LEGOS-SLEEC, a tool designed to support interdisciplinary stakeholders in specifying normative requirements as SLEEC rules, and in analyzing and debugging their well-formedness. LEGOS-SLEEC is built using four previously published components, which have been shown to be effective and usable across nine case studies. Reflecting on this experience, we have significantly improved the user interface of LEGOS-SLEEC and its diagnostic support, and demonstrate the effectiveness of these improvements using four interdisciplinary stakeholders. Showcase video URL is: https://youtu.be/LLaBLGxSi8A
△ Less
Submitted 21 January, 2025;
originally announced January 2025.