Memory-safety issues and information leakage are known to be depressingly common. We consider the compositional static detection of these kinds of vulnerabilities in first-order C-like programs. Indeed the latter are relational hyper-safety violations, comparing pairs of program executions, making them more challenging to detect than the former, which require reasoning only over individual executions. Existing symbolic leakage detection methods treat only non-interactive programs, avoiding the challenges of nondeterminism. Also, being whole-program analyses they cannot be applied one-function-at-a-time, thereby ruling out incremental analysis. We remedy these shortcomings by presenting Insecurity Separation Logic (InsecSL), an under-approximate relational program logic for soundly detecting information leakage and memory-safety issues in interactive programs. Importantly, InsecSL reasons about pairs of executions, and so is relational, but purposefully resembles the non-relational Incorrectness Separation Logic (ISL) that is already automated in the Infer tool. We show how InsecSL can be automated by bi-abduction based symbolic execution, and we evaluate two implementations of this idea (one based on Infer) on various case-studies.

翻译：内存安全问题和信息泄露已知令人沮丧地普遍存在。我们考虑对一阶类C语言程序中的此类漏洞进行组件化静态检测。事实上，后者（信息泄露）属于关系型超安全性违反，需要比较程序执行对，这使得其比前者（内存安全问题）更难检测，因为前者只需对单个执行进行推理。现有符号化泄露检测方法仅处理非交互式程序，避免了非确定性的挑战。同时，作为全程序分析，它们无法逐个函数地应用，从而排除了增量分析的可能性。我们通过提出不安全性分离逻辑（InsecSL）来弥补这些缺陷，这是一种欠近似关系型程序逻辑，用于可靠地检测交互式程序中的信息泄露和内存安全问题。关键在于，InsecSL对执行对进行推理，因此是关系型的，但有意与非关系型的、已在Infer工具中实现自动化错误分离逻辑（ISL）相似。我们展示了如何通过基于双向归结的符号执行自动化InsecSL，并在多个案例研究中对这一思想的两种实现（一种基于Infer）进行了评估。