Caruca：用于不透明软件组件的高效规范矿工
软件工程
2025-10-17 v1 编程语言
摘要
众多前沿系统在由不透明组件组成的程序上 demonstrate了在性能、安全性和可靠性方面的显著提升。要对这些系统中的组件进行建模，需要部分规范。然而，创建此类规范是手动的、费力的且容易出错的过程，限制了这些系统的实用性。本文提出了 Caruca，一个用于不透明命令的自动规范矿工系统。为克服命令之间语言多样性带来的挑战，Caruca 首先仪器化一个大语言模型，将命令的用户文档翻译为结构化的调用语法。使用此表示形式，Caruca 探索语法有效的命令调用和执行环境的空间。Caruca 在每个命令-环境对上具体执行，拦截系统调用和文件系统层，以提取诸如并行性和文件系统前后条件等关键命令属性。这些属性可以多种规范格式导出，并立即供现有系统使用。将 Caruca 应用于 60 个 GNU Coreutils、POSIX 和第三方命令，经过多个依赖规范的系统测试，显示 Caruca 为除一种情况外的所有情况生成正确的规范，完全消除了该过程中的手动工作，目前为一个最先进的静态分析工具提供完整的规范。
引用
@article{arxiv.2510.14279,
title = {Caruca: Effective and Efficient Specification Mining for Opaque Software Components},
author = {Evangelos Lamprou and Seong-Heon Jung and Mayank Keoliya and Lukas Lazarek and Konstantinos Kallas and Michael Greenberg and Nikos Vasilakis},
journal= {arXiv preprint arXiv:2510.14279},
year = {2025}
}