Compositional Vulnerability Detection with Insecurity Separation Logic

Memory-safety issues and information leakage are known to be depressingly common. We consider the compositional static detection of these kinds of vulnerabilities in first-order C-like programs. Existing methods often treat one type of vulnerability (e.g. memory-safety) but not the other (e.g. information leakage). Indeed the latter are hyper-safety violations, making them more challenging to detect than the former. Existing leakage detection methods like Relational Symbolic Execution treat only non-interactive programs, avoiding the challenges raised by nondeterminism for reasoning about information leakage. Their implementations also do not treat non-trivial leakage policies like value-dependent classification, which are becoming increasingly common. Finally, being whole-program analyses they cannot be applied compositionally -- to deduce the presence of vulnerabilities in a program by analysing each of its parts -- thereby ruling out the possibility of incremental analysis. In this paper we remedy these shortcomings by presenting Insecurity Separation Logic (InsecSL), an under-approximate relational program logic for soundly detecting information leakage and memory-safety issues in interactive programs. We show how InsecSL can be soundly automated by bi-abduction based symbolic execution. Based on this, we design and implement a top-down, contextual, compositional, inter-procedural analysis for vulnerability detection. We implement our approach in a proof-of-concept tool, Underflow, for analysing C programs, which we demonstrate by applying it to various case studies.