从自然语言合成精确协议规范以实现有效测试生成

安全和安全关键系统必须针对其规范进行彻底测试。当前实践是使用_自然语言_规范，从中手动推导出测试用例——这一过程缓慢、易出错且难以扩展。相比之下，_形式规范_适合自动化测试生成，但繁琐且难以维护。在本工作中，我们提出了一个两阶段管道，使用大型语言模型（LLMs）来弥合差距：首先，从自然语言规范中提取_协议元素_；其次，利用协议实现，从这些元素合成和细化形式_协议规范_，我们可以据此对进一步实现进行大规模测试。我们认为这种两阶段方法优于端到端LLM-based 测试生成，原因有四点：1. 它产生一个_可检查的规范_，保留了到原始文本的可追溯性；2. 生成实际测试用例_不再需要LLM_；3. resulting 形式规范_可读性强_，可以被审查、版本控制和逐步细化；4.随着时间推移，我们可以构建一个自然语言到形式规范映射的_corpus_，用于进一步训练和细化LLM以实现更自动的翻译。我们的原型AUTOSPEC在五个广泛使用的_互联网协议_（SMTP、POP3、IMAP、FTP和ManageSieve）上成功地演示了我们方法的可行性，这些方法应用于其_自然语言_的RFC规范，以及最近的_I/O grammar_形式化规范和模糊测试。 在我们的评估中，AUTOSPEC在平均恢复92.8%的客户端和80.2%的服务器消息类型，实现了81.5%的消息接受率。