CNnotator: LLM-Guided Memory Safety Annotation Synthesis
该论文介绍了 CNnotator，这是一个利用大语言模型为遗留 C 代码自动合成并验证内存安全注解（CN 规范）的工具，证明了当前的 AI 模型能够通过识别内存使用模式来实现向更安全语言的迁移，并取得较高的成功率。
原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
想象一下，你拥有一本用一种非常危险的厨房语言——C语言——编写的旧手写食谱。在这种语言中，厨师（程序员）必须手动管理每一件食材。如果他们忘记给锅盖上盖子，或者试图使用一把已经被扔进垃圾桶的勺子，整个厨房就会起火。这些被称为内存安全错误，它们导致了我们每天使用的软件中出现了大量的安全漏洞。
现代语言如 Rust 就像是一个配备了智能电器的厨房：如果你试图在烤箱还很烫的时候打开它，它会自动锁定烤箱；或者它不会让你去拿一把并不存在的勺子。但我们不能直接扔掉旧的食谱。我们需要弄清楚那些旧厨师究竟是如何使用食材的，这样我们才能修复食谱，或者将它们翻译成新的、安全的语言。
问题在于，在旧的食谱中，使用食材的规则并没有被写下来。它们隐藏在混乱的步骤之中。弄清楚这些规则就像仅仅通过观察别人烹饪来猜测一个秘密代码一样。这既繁琐又容易出错。
新工具：CNnotator
作者开发了一个名为 CNnotator 的工具来提供帮助。你可以把它想象成一个由两个人组成的团队：
- 猜测厨师（AI）： 这是一个大语言模型（LLM）。它非常擅长观察混乱的食谱并进行猜测，比如：“噢，我敢打赌这位厨师会一直拿着这把勺子直到最后。”它尝试将隐藏的规则写成一份正式的契约。
- 严格检查员（形式化工具）： 这是一个名为 CN 的计算机程序。它不信任猜测厨师。它的唯一工作就是检查这些猜测。它根据写好的规则运行食谱 100 次，使用不同的随机食材，看看厨房是否保持安全。
它是如何工作的（“猜测与检查”循环）
该工具遵循一个简单的循环：
- 挑选食谱： 工具查看 C 代码中的一个函数（一个特定的烹饪步骤）。
- 询问 AI： “嘿，AI，请写下这个步骤处理食材的规则。”
- AI 进行猜测： AI 写下一份“契约”（一套规则），描述谁拥有哪些食材，以及何时可以安全地使用它们。
- 检查员进行测试： 工具根据这些规则运行代码 100 次。
- 如果通过： 太棒了！规则很可能是正确的。进入下一个食谱。
- 如果失败： 检查员会说：“你说明明勺子是安全的，但它却爆炸了！”工具会将这个错误发回给 AI：“再试一次，但请修复这个具体的错误。”
- 重复： AI 会再次尝试，最多尝试六次，直到它做对或者放弃为止。
结果
研究人员在 31 个不同的“食谱”（C 函数）上测试了该工具，涵盖了从简单任务到稍复杂任务的各种情况。他们使用了五种不同的 AI 模型进行测试。
- 明星选手： 被称为 o3 的 AI 模型表现最好。它在 90% 的食谱上第一次尝试就写对了规则。到允许它多次尝试后，它在 97% 的食谱上取得了成功。
- 聊天机器人： 即便是较旧的标准聊天模型（GPT-4o）也做得相当不错，它在第一次尝试时能写对大约 65% 的情况。
- 安全网： 该工具也非常聪明，能够识别出“损坏的”食谱。如果代码存在一个保证存在的 Bug（比如尝试使用一把已经被扔掉的勺子），AI 会说：“我无法写出一个安全的规则，因为食谱本身是损坏的，”然后停止运行。
为什么这很重要
论文指出，我们不需要要求 AI 是完美的。我们只需要它成为一个优秀的猜测者。因为我们有一个严格的检查员（形式化工具）来检查每一个猜测，所以即使 AI 在过程中犯了错，我们也可以信任最终的结果。
这种方法表明，我们现在可以利用 AI 来帮助我们理解和现代化旧的、危险的 C 代码，使它们变得更安全，而无需手动重写每一行代码。这就像是拥有一个超快的手下，可以起草安全规则，同时还有一个大师级的检查员来确保建筑不会坍塌。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。