| Title | Precise Detection of Side-Channel Vulnerabilities Using Quantitative Cartesian Hoare Logic |
| Publication Type | Conference Paper |
| Year of Publication | 2017 |
| Authors | Chen, Jia, Feng, Yu, Dillig, Isil |
| Conference Name | Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security |
| Publisher | ACM |
| Conference Location | New York, NY, USA |
| ISBN Number | 978-1-4503-4946-8 |
| Keywords | composability, Metrics, pubcrawl, side channels, static analysis, taint analysis, verification, vulnerability detection |
| Abstract | This paper presents Themis, an end-to-end static analysis tool for finding resource-usage side-channel vulnerabilities in Java applications. We introduce the notion of epsilon-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 epsilon-bounded non-interference. Our tool, Themis, combines automated reasoning in CHL with lightweight static taint analysis to improve scalability. We evaluate Themis on well known Java applications and demonstrate that Themis can find unknown side-channel vulnerabilities in widely-used programs. We also show that Themis can verify the absence of vulnerabilities in repaired versions of vulnerable programs and that Themis compares favorably against Blazer, a state-of-the-art static analysis tool for finding timing side channels in Java applications. |
| URL | http://doi.acm.org/10.1145/3133956.3134058 |
| DOI | 10.1145/3133956.3134058 |
| Citation Key | chen_precise_2017 |
Precise Detection of Side-Channel Vulnerabilities Using Quantitative Cartesian Hoare Logic