Caruca: Effective and Efficient Specification Mining for Opaque Software Components

TL;DR

Caruca automates the generation of specifications for opaque software components by translating command documentation into a structured invocation syntax via an LLM, then exhaustively but pragmatically configuring and tracing command invocations in sandboxed environments to derive formal pre-/post-conditions and parallelizability. The approach yields high correctness across multiple consumer systems (PaSh, POSH, Shellcheck, Shseer) and demonstrates scalable coverage and reasonable runtimes, reducing manual annotation effort to near-zero. Its architecture—syntax inference, configuration generation, isolated tracing, and trace-driven derivation with adapters—enables cross-domain specification mining with strong practical impact for performance optimization and bug finding in complex, language-agnostic command ecosystems.

Abstract

A wealth of state-of-the-art systems demonstrate impressive improvements in performance, security, and reliability on programs composed of opaque components, such as Unix shell commands. To reason about commands, these systems require partial specifications. However, creating such specifications is a manual, laborious, and error-prone process, limiting the practicality of these systems. This paper presents Caruca, a system for automatic specification mining for opaque commands. To overcome the challenge of language diversity across commands, Caruca first instruments a large language model to translate a command's user-facing documentation into a structured invocation syntax. Using this representation, Caruca explores the space of syntactically valid command invocations and execution environments. Caruca concretely executes each command-environment pair, interposing at the system-call and filesystem level to extract key command properties such as parallelizability and filesystem pre- and post-conditions. These properties can be exported in multiple specification formats and are immediately usable by existing systems. Applying Caruca across 60 GNU Coreutils, POSIX, and third-party commands across several specification-dependent systems shows that Caruca generates correct specifications for all but one case, completely eliminating manual effort from the process and currently powering the full specifications for a state-of-the-art static analysis tool.

Figures (7)

• Figure 1: Caruca architecture overview.Caruca takes as input a command binary and its documentation, and first creates a syntax specification (\ref{['sec:syntax-spec']}). From this, its configuration generator (\ref{['sec:config-gen']}) creates diverse invocations and environments. These are executed in a traced sandbox (\ref{['sec:tracing']}), recording all system-level interactions. Finally, the specification derivation subsystem (\ref{['sec:specs']}) analyzes the collected traces to produce specifications for downstream systems (\ref{['sec:eval']}). Colors indicate component roles: red---static inputs; green---subsystems; blue---runtime and analysis outputs.
• Figure 2: Example shell script from the htmx project htmx. The script prepares the htmx library for download. It copies htmx's source code inside a directory, minifies it, and compresses it.
• Figure 3: Specification for rm. Excerpt from the rm specification produced by Caruca. The specification encodes per-invocation pre- and post-conditions related to the command's filesystem effects, the way it interacts with its input ($I$) and output ($O$) streams, alongside summaries of its parallelizability ($\mathcal{P}$) and monotonicity ($\downarrow$) properties (\ref{['sec:specs']}).
• Figure 4: Histogram of command invocation counts. Histogram of the number of invocations per command in the collected dataset for the top 40 most invoked commands.
• Figure 5: Caruca's filesystem model.Caruca's filesystem model describes the possible filesystem states that Caruca considers relevant to command behavior. The model captures the filesystem at the path and object level. A filesystem object can be a file or a directory, and a filesystem path can either point to a filesystem object or be non-existent.