Quantifying Information Leak Vulnerabilities

TL;DR

This paper presents a scalable technique using bounded model checking to quantify information leaks in large, real-world programs, verifying vulnerabilities and the effectiveness of patches in industrial software.

Contribution

It introduces a novel approach for applying quantitative information flow analysis to complex, real-world programs, including verification of security patches in industrial software.

Findings

Successfully identified information leaks in Linux Kernel vulnerabilities

Verified that security patches effectively eliminate leaks

Demonstrated applicability to large-scale industrial programs

Abstract

Leakage of confidential information represents a serious security risk. Despite a number of novel, theoretical advances, it has been unclear if and how quantitative approaches to measuring leakage of confidential information could be applied to substantial, real-world programs. This is mostly due to the high complexity of computing precise leakage quantities. In this paper, we introduce a technique which makes it possible to decide if a program conforms to a quantitative policy which scales to large state-spaces with the help of bounded model checking. Our technique is applied to a number of officially reported information leak vulnerabilities in the Linux Kernel. Additionally, we also analysed authentication routines in the Secure Remote Password suite and of a Internet Message Support Protocol implementation. Our technique shows when there is unacceptable leakage; the same technique is also used to verify, for the first time, that the applied software patches indeed plug the information leaks. This is the first demonstration of quantitative information flow addressing security concerns of real-world industrial programs.