Incremental Vulnerability Detection via Back-Propagating Symbolic Execution of Insecurity Separation Logic

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, including Insecurity Separation Logic (InsecSL). We show how InsecSL can be automated via back-propagating symbolic execution (BPSE) 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.