用强类型系统提升大模型生成代码的安全性
TypePilot: Leveraging the Scala Type System for Secure LLM-generated Code
- 通过Scala类型系统引导AI生成代码，自动约束变量和接口
- 在安全验证中显著减少输入验证与注入漏洞，成功率提升明显
- 适合高可靠系统开发，如金融、医疗等安全敏感领域
大型语言模型（LLMs）在多种编程语言的代码生成任务中表现出色，但其输出常包含细微却关键的漏洞，部署于安全敏感或关键任务系统时带来重大风险。本文提出TypePilot，一种基于智能体的AI框架，利用强类型且可验证的语言（以Scala为例）增强LLM生成代码的安全性与鲁棒性。我们在两个场景下评估该方法：使用Stainless框架进行形式化验证，以及通用安全代码生成。实验表明，直接生成代码或简单提示均难以保证安全约束，而我们的类型导向智能体流程显著缓解了输入验证与注入类漏洞。结果表明，结构化、类型驱动的LLM工作流可显著提升高保障领域自动化代码生成的可信度。
原文摘要 · Abstract (English)
Large language Models (LLMs) have shown remarkable proficiency in code generation tasks across various programming languages. However, their outputs often contain subtle but critical vulnerabilities, posing significant risks when deployed in security-sensitive or mission-critical systems. This paper introduces TypePilot, an agentic AI framework designed to enhance the security and robustness of LLM-generated code by leveraging strongly typed and verifiable languages, using Scala as a representative example. We evaluate the effectiveness of our approach in two settings: formal verification with the Stainless framework and general-purpose secure code generation. Our experiments with leading open-source LLMs reveal that while direct code generation often fails to enforce safety constraints, just as naive prompting for more secure code, our type-focused agentic pipeline substantially mitigates input validation and injection vulnerabilities. The results demonstrate the potential of structured, type-guided LLM workflows to improve the SotA of the trustworthiness of automated code generation in high-assurance domains.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。