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.

翻译：大量最先进的系统在由不透明组件（如Unix shell命令）构成的程序上展现出性能、安全性和可靠性的显著提升。为了对命令进行推理，这些系统需要部分规约。然而，创建此类规约是一个手动、费力且易出错的过程，限制了这些系统的实用性。本文提出Caruca，一个面向不透明命令的自动规约挖掘系统。为克服命令间语言多样性的挑战，Caruca首先利用大语言模型将命令的用户文档翻译为结构化的调用语法。基于此表示，Caruca探索语法有效的命令调用与执行环境空间。Caruca具体执行每个命令-环境对，在系统调用和文件系统层面进行拦截，以提取关键命令属性，如可并行性以及文件系统的前置与后置条件。这些属性能以多种规约格式导出，并可直接被现有系统使用。将Caruca应用于60个GNU Coreutils、POSIX及第三方命令，并在多个依赖规约的系统中进行测试，结果表明除一例外Caruca能为所有情况生成正确规约，完全消除了该过程中的人工工作，目前正为一个最先进的静态分析工具提供完整规约支持。