KLEESpectre: detecting information leakage through speculative cache attacks via symbolic execution

Guanhua Wang; Sudipta Chattopadhyay; Arnab Kumar Biswas; Tulika Mitra; Abhik Roychoudhury

doi:10.1145/3385897

KLEESpectre: detecting information leakage through speculative cache attacks via symbolic execution

Guanhua Wang
, Sudipta Chattopadhyay
, Arnab Kumar Biswas
, Tulika Mitra
, Abhik Roychoudhury

Research output: Contribution to journal › Article › peer-review

34 Citations (Scopus)

Abstract

Spectre-style attacks disclosed in early 2018 expose data leakage scenarios via cache side channels. Specifically, speculatively executed paths due to branch mis-prediction may bring secret data into the cache, which are then exposed via cache side channels even after the speculative execution is squashed. Symbolic execution is a well-known test generation method to cover program paths at the level of the application software. In this article, we extend symbolic execution with modeling of cache and speculative execution. Our tool KLEESPECTRE, built on top of the KLEE symbolic execution engine, can thus provide a testing engine to check for data leakage through the cache side channel as shown via Spectre attacks. Our symbolic cache model can verify whether the sensitive data leakage due to speculative execution can be observed by an attacker at a given program point. Our experiments show that KLEESPECTRE can effectively detect data leakage along speculatively executed paths and our cache model can make the leakage detection more precise.

Original language	English
Article number	14
Pages (from-to)	1-31
Journal	ACM Transactions on Software Engineering and Methodology
Volume	29
Issue number	3
Early online date	01 Jun 2020
DOIs	https://doi.org/10.1145/3385897
Publication status	Published - 09 Jul 2020
Externally published	Yes

Bibliographical note

Funding Information:
Joint first author. This research is supported by the National Research Foundation, Prime Minister’s Office, Singapore, under its National Cybersecurity R&D Program (Award No. NRF2014NCR-NCR001-21) and administered by the National Cybersecurity R&D Directorate. Authors’ addresses: G. Wang, T. Mitra, A. Roychoudhury and A. K. Biswas, School of Computing, National University of Singapore, COM1, 13 Computing Drive, 117417, Singapore; emails: {guanhua, tulika, abhik}@comp.nus.edu.sg, [email protected]; S. Chattopadhyay, Information Systems Technology and Design (ISTD), Singapore University of Technology and Design, Singapore; email: [email protected].

Keywords

cache side channel
software security
Spectre attacks
symbolic execution

ASJC Scopus subject areas

Software

Access to Document

10.1145/3385897Licence: Unspecified

Cite this

@article{12e4851485f64b548939ac7b99d9d5ac,

title = "KLEESpectre: detecting information leakage through speculative cache attacks via symbolic execution",

abstract = "Spectre-style attacks disclosed in early 2018 expose data leakage scenarios via cache side channels. Specifically, speculatively executed paths due to branch mis-prediction may bring secret data into the cache, which are then exposed via cache side channels even after the speculative execution is squashed. Symbolic execution is a well-known test generation method to cover program paths at the level of the application software. In this article, we extend symbolic execution with modeling of cache and speculative execution. Our tool KLEESPECTRE, built on top of the KLEE symbolic execution engine, can thus provide a testing engine to check for data leakage through the cache side channel as shown via Spectre attacks. Our symbolic cache model can verify whether the sensitive data leakage due to speculative execution can be observed by an attacker at a given program point. Our experiments show that KLEESPECTRE can effectively detect data leakage along speculatively executed paths and our cache model can make the leakage detection more precise. ",

keywords = "cache side channel, software security, Spectre attacks, symbolic execution",

author = "Guanhua Wang and Sudipta Chattopadhyay and Biswas, \{Arnab Kumar\} and Tulika Mitra and Abhik Roychoudhury",

note = "Funding Information: Joint first author. This research is supported by the National Research Foundation, Prime Minister{\textquoteright}s Office, Singapore, under its National Cybersecurity R\&D Program (Award No. NRF2014NCR-NCR001-21) and administered by the National Cybersecurity R\&D Directorate. Authors{\textquoteright} addresses: G. Wang, T. Mitra, A. Roychoudhury and A. K. Biswas, School of Computing, National University of Singapore, COM1, 13 Computing Drive, 117417, Singapore; emails: \{guanhua, tulika, abhik\}@comp.nus.edu.sg, [email protected]; S. Chattopadhyay, Information Systems Technology and Design (ISTD), Singapore University of Technology and Design, Singapore; email: sudipta\[email protected].",

year = "2020",

month = jul,

day = "9",

doi = "10.1145/3385897",

language = "English",

volume = "29",

pages = "1--31",

journal = "ACM Transactions on Software Engineering and Methodology",

issn = "1049-331X",

publisher = "Association for Computing Machinery",

number = "3",

}

TY - JOUR

T1 - KLEESpectre: detecting information leakage through speculative cache attacks via symbolic execution

AU - Wang, Guanhua

AU - Chattopadhyay, Sudipta

AU - Biswas, Arnab Kumar

AU - Mitra, Tulika

AU - Roychoudhury, Abhik

N1 - Funding Information: Joint first author. This research is supported by the National Research Foundation, Prime Minister’s Office, Singapore, under its National Cybersecurity R&D Program (Award No. NRF2014NCR-NCR001-21) and administered by the National Cybersecurity R&D Directorate. Authors’ addresses: G. Wang, T. Mitra, A. Roychoudhury and A. K. Biswas, School of Computing, National University of Singapore, COM1, 13 Computing Drive, 117417, Singapore; emails: {guanhua, tulika, abhik}@comp.nus.edu.sg, [email protected]; S. Chattopadhyay, Information Systems Technology and Design (ISTD), Singapore University of Technology and Design, Singapore; email: [email protected].

PY - 2020/7/9

Y1 - 2020/7/9

N2 - Spectre-style attacks disclosed in early 2018 expose data leakage scenarios via cache side channels. Specifically, speculatively executed paths due to branch mis-prediction may bring secret data into the cache, which are then exposed via cache side channels even after the speculative execution is squashed. Symbolic execution is a well-known test generation method to cover program paths at the level of the application software. In this article, we extend symbolic execution with modeling of cache and speculative execution. Our tool KLEESPECTRE, built on top of the KLEE symbolic execution engine, can thus provide a testing engine to check for data leakage through the cache side channel as shown via Spectre attacks. Our symbolic cache model can verify whether the sensitive data leakage due to speculative execution can be observed by an attacker at a given program point. Our experiments show that KLEESPECTRE can effectively detect data leakage along speculatively executed paths and our cache model can make the leakage detection more precise.

AB - Spectre-style attacks disclosed in early 2018 expose data leakage scenarios via cache side channels. Specifically, speculatively executed paths due to branch mis-prediction may bring secret data into the cache, which are then exposed via cache side channels even after the speculative execution is squashed. Symbolic execution is a well-known test generation method to cover program paths at the level of the application software. In this article, we extend symbolic execution with modeling of cache and speculative execution. Our tool KLEESPECTRE, built on top of the KLEE symbolic execution engine, can thus provide a testing engine to check for data leakage through the cache side channel as shown via Spectre attacks. Our symbolic cache model can verify whether the sensitive data leakage due to speculative execution can be observed by an attacker at a given program point. Our experiments show that KLEESPECTRE can effectively detect data leakage along speculatively executed paths and our cache model can make the leakage detection more precise.

KW - cache side channel

KW - software security

KW - Spectre attacks

KW - symbolic execution

U2 - 10.1145/3385897

DO - 10.1145/3385897

M3 - Article

AN - SCOPUS:85088297802

SN - 1049-331X

VL - 29

SP - 1

EP - 31

JO - ACM Transactions on Software Engineering and Methodology

JF - ACM Transactions on Software Engineering and Methodology

IS - 3

M1 - 14

ER -

KLEESpectre: detecting information leakage through speculative cache attacks via symbolic execution

Abstract

Bibliographical note

Keywords

ASJC Scopus subject areas

Access to Document

Fingerprint

Cite this