用自然语言生成和验证代码安全规范，提升大模型编程安全性
Natural Language based Specification and Verification
- 用大模型自动生成自然语言形式的安全规范
- 在自然语言规范下实现代码的分层验证，初步效果良好
- 适合关注AI生成代码安全性的研究人员和开发者
近期前沿大语言模型（LLMs）在识别大型成熟开源系统中的安全漏洞方面表现出色。随着大模型生成代码日益普遍，一个自然目标是防止模型在最初就生成存在漏洞的实现。形式化验证为此提供了理论路径，但现有验证流程通常需要使用僵化的形式语言编写规范。此前工作尝试用大模型合成此类规范，但成效有限。本文探索一种新方法：利用大模型同时生成自然语言规范，并在自然语言规范下对实现进行组合式验证。初步结果表明该方法具有潜力。
原文摘要 · Abstract (English)
Recent frontier large language models (LLMs) have shown strong performance in identifying security vulnerabilities in large, mature open-source systems. As LLM-generated code becomes increasingly common, a natural goal is to prevent such models from producing vulnerable implementations in the first place. Formal verification offers a principled route to this objective, but existing verification pipelines typically require specifications written in rigid formal languages. Prior work has explored using LLMs to synthesize such specifications, with limited success. In this paper, we investigate a different approach: using LLMs both to generate specifications and to verify implementations compositionally when the specifications are expressed in natural language. Our preliminary results suggest that this approach is promising.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。