基于“天使假设”（Angelic Assumptions）的开源程序内存安全性验证

《Proceedings of the ACM on Programming Languages》：Memory-Safety Verification of Open Programs with Angelic Assumptions

内存安全验证中假阳性过滤方法

　　

摘要

开源程序是指其完整源代码无法获取的程序，这在现实世界的程序验证中是普遍存在的现象。软件验证工具往往会对其未受限制的行为持最坏的假设，这可能导致针对开源程序产生大量虚假警告。对于任何严肃的验证工作，工程师都必须预先投入时间来构建缺失代码的合适模型（或模拟代码），而这既耗时又容易出错。模拟代码中的不准确之处可能会导致错误的验证结果。

在本文中，我们展示了一种能够高精度区分开源程序中虚假阳性结果（误报）和实际错误以及潜在内存安全违规的技术。该技术的核心在于能够对缺失的代码做出合理的假设。为此，我们首先使用大型语言模型（LLM）从处理缓冲区的程序中提取一组惯用模式。然后通过一种形式化的合成策略对这些惯用模式进行选择、调整，并将其应用到目标程序中，从而形成合理的假设。总体而言，我们的系统“Seeker”仅会在程序能够通过一组明确定义的“可信”惯用模式进行验证时，才认定该程序是正确的。在对一系列来自流行开源软件的基准测试进行实验时，我们的工具“Seeker”能够识别出79%的虚假阳性结果，同时完全没有误报。