QFuzz: Quantitative Fuzzing for Side Channels

This paper presents T, an end-to-end static analysis tool for nding resource-usage side-channel vulnerabilities in Java applications. We introduce the notion of -bounded non-interference, a variant and relaxation of Goguen and Meseguer’s well-known non-interference principle. We then present Quantitative Cartesian Hoare Logic (QCHL), a program logic for verifying -bounded noninterference. Our tool, T, combines automated reasoning in CHL with lightweight static taint analysis to improve scalability. We evaluate T on well known Java applications and demonstrate that T can nd unknown side-channel vulnerabilities in widely-used programs. We also show that T can verify the absence of vulnerabilities in repaired versions of vulnerable programs and that T compares favorably against B, a state-of-the-art static analysis tool for nding timing side channels in Java applications. CCS CONCEPTS • Security and privacy→ Logic and verication; Software security engineering; • Theory of computation → Automated reasoning;