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.

By admin