We present the first compositional, incremental static analysis for detecting memory-safety and information leakage vulnerabilities in C-like programs. To do so, we develop the first under-approximate relational program logics for reasoning about information flow, including Insecurity Separation Logic (InsecSL). Like prior under-approximate separation logics, we show that InsecSL can be automated via symbolic execution. We then adapt and extend a prior intra-procedural symbolic execution algorithm to build a bottom-up, inter-procedural and incremental analysis for detecting vulnerabilities. We prove our approach sound in Isabelle/HOL and implement it in a proof-of-concept tool, Underflow, for analysing C programs, which we apply to various case studies.

翻译：我们在类似C类方案中提出第一个构成、渐进的静态分析,以发现记忆安全和信息渗漏脆弱性。为此,我们开发了第一个关于信息流动推理的近似关联程序逻辑,包括不安全分离逻辑(InsecSL ) 。和先前的近似分离逻辑一样,我们展示了InsecSL可以通过象征性执行实现自动化。然后我们调整并扩展了先前的程序内象征性执行算法,以建立一个自下而上、程序间和递增分析来检测脆弱性。我们在伊莎贝尔/HOL证明了我们的方法合理,并在概念验证工具“潜流”中加以实施,用于分析我们适用于各种案例研究的C程序。