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.
Download