Incremental Vulnerability Detection with 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 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 build a top-down, contextual, compositional, inter-procedural 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.