发表机构
Amazon Web Services（亚马逊云科技）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
提出猜测-检查方法，用LLM生成污点流模型并用符号算法验证可靠性，在97个模型上证明93%可靠且无新误报。
AI 中文摘要
现有的针对命令式编程语言的最先进静态污点流分析，通过使用用户提供的精确库方法污点流模型，可以扩展到大型应用程序。然而，手动且精确地对方法的污点流进行建模既繁琐又可能不可靠。此外，通过过程间污点分析自动对方法进行建模可能效率低下。为解决此问题，我们提出一种猜测-检查方法：（1）一个生成方法精确污点流模型的LLM智能体，以及（2）一个检查模型可靠性的符号算法。该算法推导出为使LLM的污点流模型可靠，方法中必须不发生的污点流，并使用轻量级静态分析（如类型系统和指针分析）来证明这些必须不发生的流。当这些分析不足时，算法推导出最大程度通用的被调用者模型并递归验证其可靠性，在大多数情况下避免了完整的过程间污点分析。由于更精确的模型需要验证更少的必须不发生的流，LLM模型的精确性直接决定了我们方法的效率。我们在6个大型Go代码库中的97个LLM生成的污点流模型上评估了我们的方法，并证明了这些模型对其覆盖的方法的93%是可靠的。被证明可靠的LLM生成模型也是精确的，在证明污点流属性时没有产生新的误报。
英文摘要
Existing state-of-the-art static taint flow analyses for imperative programming languages can scale to large applications by using precise user-provided taint flow models of library methods. However, manually and precisely modeling a method's taint flows is tedious and potentially unsound. Furthermore, automatically modeling the method via an inter- procedural taint analysis can be inefficient. To solve this problem, we propose a guess-and-check approach: (1) an LLM agent that generates a precise taint flow model of a method and (2) a symbolic algorithm to check the soundness of the model. The algorithm deduces which taint flows must not occur in the method for the LLM's taint flow model to be sound, and uses lightweight static analyses (e.g., type system and pointer analysis) to prove these must-not-flows. When these analyses are insufficient, the algorithm deduces maximally-general callee models and recursively verifies their soundness, avoiding a full inter-procedural taint analysis in most cases. Since a more precise model requires fewer must-not-flows to be verified, the precision of the LLM's model directly determines the efficiency of our approach. We evaluate our approach on 97 LLM-generated taint flow models for methods in 6 large Go codebases and prove the models sound for 93% of the methods they cover. The proven-sound LLM-generated models are also precise, resulting in no new false-positives when proving taint flow properties.
