Basis的研究人员利用大语言模型指导对Linux nftables防火墙编译器进行形式化验证，发现了两个自2022年以来存在于内核中的关键漏洞并进行了修复。这项工作证明了LLM能够有效弥补形式化方法领域的专家缺口，表明关键基础设施组件可以通过“构建即安全”的方式消除语义错误。
背景
形式化验证通过数学证明确保软件正确性，但通常需要稀缺的专业知识。最近大语言模型能力的提升表明，它们可以自动化或协助为复杂系统生成这些证明。
- 来源
- Lobsters
- 发布时间
- 2026年7月20日 21:57
- 评分
- 9.0 / 10