污点流模型的健全性检查

通过使用用户提供的精确的库方法污点流模型，现有最先进的命令式编程语言静态污点流分析可以扩展到大型应用程序。然而，手动精确地对方法的污点流进行建模是乏味的并且可能不合理。此外，通过过程间污点分析自动建模方法可能效率低下。为了解决这个问题，我们提出了一种猜测和检查方法：（1）LLM代理生成方法的精确污点流模型，（2）符号算法来检查模型的健全性。该算法在LLM的污点流模型健全的方法中推导出哪些污点流不能发生，并使用轻量级静态分析（例如类型系统和指针分析）来证明这些不能发生的流。当这些分析不充分时，算法会推导出最通用的被调用者模型并递归地验证它们的可靠性，从而在大多数情况下避免完整的过程间污点分析。由于更精确的模型需要验证更少的禁止流程，因此 LLM 模型的精度直接决定了我们方法的效率。我们在 6 个大型 Go 代码库中的方法的 97 个 LLM 生成的污点流模型上评估了我们的方法，并证明这些模型对于它们涵盖的 93% 的方法来说是正确的。经过验证的 LLM 生成的模型也很精确，在证明污点流属性时不会导致新的误报。