research-article

Cache Refinement Type for Side-Channel Detection of Cryptographic Software

Authors:

Tianwei ZhangAuthors Info & Claims

CCS '22: Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security

Pages 1583 - 1597

https://doi.org/10.1145/3548606.3560672

Published: 07 November 2022 Publication History

Abstract

Cache side-channel attacks exhibit severe threats to software security and privacy, especially for cryptosystems. In this paper, we propose CaType, a novel refinement type-based tool for detecting cache side channels in crypto software. Compared to previous works, CaType provides the following advantages: (1) For the first time CaType analyzes cache side channels using refinement type over x86 assembly code. It reveals several significant and effective enhancements with refined types, including bit-level granularity tracking, distinguishing different effects of variables, precise type inferences, and high scalability. (2) CaType is the first static analyzer for crypto libraries in consideration of blinding-based defenses. (3) From the perspective of implementation, CaType uses cache layouts of potential vulnerable control-flow branches rather than cache states to suppress false positives. We evaluate CaType in identifying side channel vulnerabilities in real-world crypto software, including RSA, ElGamal, and (EC)DSA from OpenSSL and Libgcrypt. CaType captures all known defects, detects previously-unknown vulnerabilities, and reveals several false positives of previous tools. In terms of performance, CaType is 16X faster than CacheD and 131X faster than CacheS when analyzing the same libraries. These evaluation results confirm the capability of CaType in identifying side channel defects with great precision, efficiency, and scalability.

References

[1]

Adil Ahmad, Byunggill Joe, Yuan Xiao, Yinqian Zhang, Insik Shin, and Byoungyoung Lee. 2019. Obfuscuro: A commodity obfuscation engine on intel sgx. In Network and Distributed System Security Symposium.

[2]

Diego F Aranha, Felipe Rodrigues Novaes, Akira Takahashi, Mehdi Tibouchi, and Yuval Yarom. 2020. Ladderleak: Breaking ecdsa with less than one bit of nonce leakage. In Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security. 225--242.

Digital Library

[3]

Qinkun Bao, Zihao Wang, Xiaoting Li, James R Larus, and Dinghao Wu. 2021. Abacus: Precise side-channel analysis. In 2021 IEEE/ACM 43rd International Conference on Software Engineering (ICSE). IEEE, 797--809.

Digital Library

[4]

Gilles Barthe, Sonia Bela"id, Francc ois Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, and Pierre-Yves Strub. 2015. Verified proofs of higher-order masking. In Annual International Conference on the Theory and Applications of Cryptographic Techniques. Springer, 457--485.

[5]

Gilles Barthe, Sonia Bela"id, Francc ois Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Pierre-Yves Strub, and Rébecca Zucchini. 2016. Strong non-interference and type-directed higher-order masking. In Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security. 116--129.

Digital Library

[6]

Gilles Barthe, Cédric Fournet, Benjamin Grégoire, Pierre-Yves Strub, Nikhil Swamy, and Santiago Zanella-Béguelin. 2014. Probabilistic relational verification for cryptographic implementations. ACM SIGPLAN Notices, Vol. 49, 1 (2014), 193--205.

Digital Library

[7]

Naomi Benger, Joop van de Pol, Nigel P Smart, and Yuval Yarom. 2014. ?Ooh Aah... Just a Little Bit?: a small amount of side channel can go a long way. In International Workshop on Cryptographic Hardware and Embedded Systems. Springer, 75--92.

[8]

Jesper Bengtson, Karthikeyan Bhargavan, Cédric Fournet, Andrew D Gordon, and Sergio Maffeis. 2011. Refinement types for secure implementations. ACM Transactions on Programming Languages and Systems (TOPLAS), Vol. 33, 2 (2011), 1--45.

Digital Library

[9]

Karthikeyan Bhargavan, Cédric Fournet, and Andrew D Gordon. 2010. Modular verification of security protocol code by typing. ACM Sigplan Notices, Vol. 45, 1 (2010), 445--456.

Digital Library

[10]

Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, and Pierre-Yves Strub. 2013. Implementing TLS with verified cryptographic security. In 2013 IEEE Symposium on Security and Privacy. IEEE, 445--459.

Digital Library

[11]

Dan Boneh and Ramarathnam Venkatesan. 1996. Hardness of computing the most significant bits of secret keys in Diffie-Hellman and related schemes. In Annual International Cryptology Conference. Springer, 129--142.

[12]

Dan Boneh and Ramarathnam Venkatesan. 1997. Rounding in Lattices and its Cryptographic Applications. In SODA, Vol. 1997. Citeseer, 675--681.

[13]

Robert Brotzman, Shen Liu, Danfeng Zhang, Gang Tan, and Mahmut Kandemir. 2019. CaSym: Cache aware symbolic execution for side channel detection and mitigation. In 2019 IEEE Symposium on Security and Privacy (SP). IEEE, 505--521.

[14]

David Brumley, Ivan Jager, Thanassis Avgerinos, and Edward J Schwartz. 2011. BAP: A binary analysis platform. In International Conference on Computer Aided Verification. Springer, 463--469.

[15]

Luca Cardelli. 1996. Type systems. ACM Computing Surveys (CSUR), Vol. 28, 1 (1996), 263--264.

Digital Library

[16]

Sudipta Chattopadhyay, Moritz Beck, Ahmed Rezine, and Andreas Zeller. 2019. Quantifying information leakage in cache attacks via symbolic execution. TECS (2019).

[17]

Guoxing Chen, Sanchuan Chen, Yuan Xiao, Yinqian Zhang, Zhiqiang Lin, and Ten H Lai. 2019. Sgxpectre: Stealing intel secrets from sgx enclaves via speculative execution. In 2019 IEEE European Symposium on Security and Privacy (EuroS&P). IEEE, 142--157.

[18]

P. Cousot and R. Cousot. 1977. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 238--252.

[19]

Lesly-Ann Daniel, Sébastien Bardin, and Tamara Rezk. 2020. Binsec/rel: Efficient relational symbolic execution for constant-time at binary-level. In 2020 IEEE Symposium on Security and Privacy (SP). IEEE, 1021--1038.

[20]

Leonid Domnitser, Aamer Jaleel, Jason Loew, Nael Abu-Ghazaleh, and Dmitry Ponomarev. 2012. Non-monopolizable caches: Low-complexity mitigation of cache side channel attacks. ACM Transactions on Architecture and Code Optimization (TACO), Vol. 8, 4 (2012), 1--21.

Digital Library

[21]

Goran Doychev, Dominik Feld, Boris Kopf, Laurent Mauborgne, and Jan Reineke. 2013. $$CacheAudit$$: A Tool for the Static Analysis of Cache Side Channels. In 22nd USENIX Security Symposium (USENIX Security 13). 431--446.

[22]

Goran Doychev and Boris Köpf. 2017. Rigorous analysis of software countermeasures against cache attacks. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation. 406--421.

Digital Library

[23]

Inès Ben El Ouahma, Quentin L Meunier, Karine Heydemann, and Emmanuelle Encrenaz. 2017. Symbolic approach for side-channel resistance analysis of masked assembly codes. In Security Proofs for Embedded Systems.

[24]

Hassan Eldib, Chao Wang, and Patrick Schaumont. 2014a. Formal verification of software countermeasures against side-channel attacks. ACM Transactions on Software Engineering and Methodology (TOSEM), Vol. 24, 2 (2014), 1--24.

Digital Library

[25]

Hassan Eldib, Chao Wang, and Patrick Schaumont. 2014b. SMT-based verification of software countermeasures against side-channel attacks. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 62--77.

[26]

Hassan Eldib, Chao Wang, Mostafa Taha, and Patrick Schaumont. 2014c. QMS: Evaluating the side-channel resistance of masked software from source code. In 2014 51st ACM/EDAC/IEEE Design Automation Conference (DAC). IEEE, 1--6.

Digital Library

[27]

Pengfei Gao, Hongyi Xie, Jun Zhang, Fu Song, and Taolue Chen. 2019a. Quantitative verification of masked arithmetic programs against side-channel attacks. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 155--173.

Digital Library

[28]

Pengfei Gao, Jun Zhang, Fu Song, and Chao Wang. 2019b. Verifying and quantifying side-channel resistance of masked software implementations. ACM Transactions on Software Engineering and Methodology (TOSEM), Vol. 28, 3 (2019), 1--32.

Digital Library

[29]

Daniel Gruss, Clémentine Maurice, Klaus Wagner, and Stefan Mangard. 2016. Flush Flush: a fast and stealthy cache attack. In International Conference on Detection of Intrusions and Malware, and Vulnerability Assessment. Springer, 279--299.

Digital Library

[30]

Ranjit Jhala, Niki Vazou, et al. 2021. Refinement Types: A Tutorial. Foundations and Trends in Programming Languages, Vol. 6, 3--4 (2021), 159--317.

[31]

Ke Jiang, Yuyan Bao, Shuai Wang, Zhibo Liu, and Tianwei Zhang. 2022. Cache Refinement Type for Side-Channel Detection of Cryptographic Software. In arXiv preprint arXiv:2209.04610.

[32]

Paul Kocher, Joshua Jaffe, and Benjamin Jun. 1999. Differential power analysis. In Annual international cryptology conference. Springer, 388--397.

[33]

Libressl-1f6b35b. 2019. Remove the blinding later to avoid leaking information on the length. https://github.com/libressl-portable/openbsd/commit/1f6b35b

[34]

Libressl-2cd28f9. 2018. Use a blinding value when generating a DSA signature. https://github.com/libressl-portable/openbsd/commit/2cd28f9?diff=unified

[35]

Fangfei Liu, Yuval Yarom, Qian Ge, Gernot Heiser, and Ruby B Lee. 2015. Last-level cache side-channel attacks are practical. In 2015 IEEE symposium on security and privacy. IEEE, 605--622.

Digital Library

[36]

Xiaoxuan Lou, Tianwei Zhang, Jun Jiang, and Yinqian Zhang. 2021. A Survey of Microarchitectural Side-channel Vulnerabilities, Attacks, and Defenses in Cryptography. ACM Computing Surveys (CSUR), Vol. 54, 6 (2021), 1--37.

Digital Library

[37]

Chi-Keung Luk, Robert Cohn, Robert Muth, Harish Patil, Artur Klauser, Geoff Lowney, Steven Wallace, Vijay Janapa Reddi, and Kim Hazelwood. 2005. Pin: building customized program analysis tools with dynamic instrumentation. Acm sigplan notices, Vol. 40, 6 (2005), 190--200.

[38]

Amir Moradi, Alessandro Barenghi, Timo Kasper, and Christof Paar. 2011. On the vulnerability of FPGA bitstream encryption against power analysis attacks: Extracting keys from Xilinx Virtex-II FPGAs. In Proceedings of the 18th ACM conference on Computer and communications security. 111--124.

Digital Library

[39]

Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: an efficient SMT solver (TACAS).

[40]

Phong Q Nguyen and Igor E Shparlinski. 2002. The insecurity of the digital signature algorithm with partially known nonces. Journal of Cryptology, Vol. 15, 3 (2002).

Digital Library

[41]

Phong Q Nguyen and Igor E Shparlinski. 2003. The insecurity of the elliptic curve digital signature algorithm with partially known nonces. Designs, codes and cryptography, Vol. 30, 2 (2003), 201--217.

[42]

OpenSSL-2198be3. 2014. Fix for CVE-2014-0076. https://github.com/openssl/openssl/commit/2198be3483259de374f91e57d247d0fc667aef29

[43]

OpenSSL-4b7a4ba. 2014. Fix for CVE-2014-0076. https://github.com/openssl/openssl/commit/4b7a4ba29cafa432fc4266fe6e59e60bc1c96332

[44]

OpenSSL-972c87d. 2018. Make bn_num_bits_word constant-time. https://github.com/openssl/openssl/commit/972c87dfc7e765bd28a4964519c362f0d3a58ca4

[45]

Dag Arne Osvik, Adi Shamir, and Eran Tromer. 2006. Cache attacks and countermeasures: the case of AES. In Cryptographers' track at the RSA conference. Springer, 1--20.

Digital Library

[46]

Gao Pengfei, Xie Hongyi, Pu Sun, Jun Zhang, Fu Song, and Taolue Chen. 2020. Formal verification of masking countermeasures for arithmetic programs. IEEE Transactions on Software Engineering (2020).

[47]

Colin Percival. 2005. Cache missing for fun and profit.

[48]

Benjamin C Pierce. 2002. Types and programming languages. MIT press.

Digital Library

[49]

Antoon Purnal, Lukas Giner, Daniel Gruss, and Ingrid Verbauwhede. 2021. Systematic analysis of randomization-based protected cache architectures. In 2021 IEEE Symposium on Security and Privacy (SP). IEEE, 987--1002.

[50]

Moinuddin K Qureshi. 2018. CEASER: Mitigating conflict-based cache attacks via encrypted-address and remapping. In 2018 51st Annual IEEE/ACM International Symposium on Microarchitecture (MICRO). IEEE, 775--787.

Digital Library

[51]

Keegan Ryan. 2019. Return of the Hidden Number Problem. IACR Transactions on Cryptographic Hardware and Embedded Systems (2019), 146--168.

[52]

Andrei Sabelfeld and Andrew C. Myers. 2003. Language-based information-flow security. IEEE J. Sel. Areas Commun., Vol. 21, 1 (2003), 5--19. https://doi.org/10.1109/JSAC.2002.806121

Digital Library

[53]

Werner Schindler. 2015. Exclusive exponent blinding may not suffice to prevent timing attacks on RSA. In International Workshop on Cryptographic Hardware and Embedded Systems. Springer, 229--247.

Digital Library

[54]

Laurent Simon, David Chisnall, and Ross Anderson. 2018. What you get is what you C: Controlling side effects in mainstream C compilers. In 2018 IEEE European Symposium on Security and Privacy (EuroS&P). IEEE, 1--15.

[55]

Wei Song, Boya Li, Zihan Xue, Zhenzhen Li, Wenhao Wang, and Peng Liu. 2021. Randomized last-level caches are still vulnerable to cache side-channel attacks! But we can fix it. In 2021 IEEE Symposium on Security and Privacy (SP). IEEE, 955--969.

[56]

Chungha Sung, Brandon Paulsen, and Chao Wang. 2018. CANAL: a cache timing analysis framework via LLVM transformation (ASE).

[57]

John Toman, Ren Siqi, Kohei Suenaga, Atsushi Igarashi, and Naoki Kobayashi. 2020. ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs. In ESOP (Lecture Notes in Computer Science, Vol. 12075). Springer, 684--714. https://doi.org/10.1007/978--3-030--44914--8_25

[58]

Niki Vazou, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis, and Simon L. Peyton Jones. 2014. Refinement types for Haskell. In ICFP. ACM, 269--282. https://doi.org/10.1145/2628136.2628161

Digital Library

[59]

Panagiotis Vekris, Benjamin Cosman, and Ranjit Jhala. 2016. Refinement types for TypeScript. In PLDI. ACM, 310--325. https://doi.org/10.1145/2908080.2908110

Digital Library

[60]

Shuai Wang, Yuyan Bao, Xiao Liu, Pei Wang, Danfeng Zhang, and Dinghao Wu. 2019a. Identifying cache-based side channels through secret-augmented abstract interpretation. In 28th $$USENIX$$ Security Symposium ($$USENIX$$ Security 19). 657--674.

[61]

Shuai Wang, Pei Wang, Xiao Liu, Danfeng Zhang, and Dinghao Wu. 2017. Cached: Identifying cache-based timing channels in production software. In 26th $$USENIX$$ Security Symposium ($$USENIX$$ Security 17). 235--252.

[62]

Wubing Wang, Yinqian Zhang, and Zhiqiang Lin. 2019b. Time and Order: Towards Automatically Identifying $$Side-Channel$$ Vulnerabilities in Enclave Binaries. In 22nd International Symposium on Research in Attacks, Intrusions and Defenses (RAID 2019). 443--457.

[63]

Zhenghong Wang and Ruby B Lee. 2007. New cache designs for thwarting software cache-based side channel attacks. In Proceedings of the 34th annual international symposium on Computer architecture. 494--505.

Digital Library

[64]

Zhenghong Wang and Ruby B Lee. 2008. A novel cache architecture with enhanced performance and security. In 2008 41st IEEE/ACM International Symposium on Microarchitecture. IEEE, 83--93.

Digital Library

[65]

Samuel Weiser, David Schrammel, Lukas Bodner, and Raphael Spreitzer. 2020. Big Numbers-Big Troubles: Systematically Analyzing Nonce Leakage in ($$EC) DSA$$ Implementations. In 29th USENIX Security Symposium (USENIX Security 20). 1767--1784.

[66]

Samuel Weiser, Raphael Spreitzer, and Lukas Bodner. 2018a. Single trace attack against RSA key generation in Intel SGX SSL. In Proceedings of the 2018 on Asia Conference on Computer and Communications Security. 575--586.

Digital Library

[67]

Samuel Weiser, Andreas Zankl, Raphael Spreitzer, Katja Miller, Stefan Mangard, and Georg Sigl. 2018b. $$DATA$$--Differential Address Trace Analysis: Finding Address-based $$Side-Channels$$ in Binaries. In 27th USENIX Security Symposium (USENIX Security 18). 603--620.

[68]

Mario Werner, Thomas Unterluggauer, Lukas Giner, Michael Schwarz, Daniel Gruss, and Stefan Mangard. 2019. Scattercache: Thwarting cache attacks via cache set randomization. In USENIX Security Symposium.

[69]

Jan Wichelmann, Ahmad Moghimi, Thomas Eisenbarth, and Berk Sunar. 2018. MicroWalk: A Framework for Finding Side Channels in Binaries. In ACSAC.

[70]

Yuval Yarom and Naomi Benger. 2014. Recovering OpenSSL ECDSA Nonces Using the FLUSH RELOAD Cache Side-channel Attack. IACR Cryptol. ePrint Arch., Vol. 2014 (2014), 140.

[71]

Yuval Yarom and Katrina Falkner. 2014. FLUSH RELOAD: A high resolution, low noise, L3 cache side-channel attack. In 23rd $$USENIX$$ Security Symposium ($$USENIX$$ Security 14). 719--732.

[72]

Danfeng Zhang, Aslan Askarov, and Andrew C Myers. 2012a. Language-based control and mitigation of timing channels. In Proceedings of the 33rd ACM SIGPLAN conference on Programming Language Design and Implementation. 99--110.

Digital Library

[73]

Jun Zhang, Pengfei Gao, Fu Song, and Chao Wang. 2018. SC Infer: refinement-based verification of software countermeasures against side-channel attacks. In International Conference on Computer Aided Verification. Springer, 157--177.

[74]

Yinqian Zhang, Ari Juels, Michael K Reiter, and Thomas Ristenpart. 2012b. Cross-VM side channels and their use to extract private keys. In Proceedings of the 2012 ACM conference on Computer and communications security. 305--316. io

Digital Library

Cited By

Cai LSong FChen T(2024)Towards Efficient Verification of Constant-Time Cryptographic ImplementationsProceedings of the ACM on Software Engineering10.1145/36437721:FSE(1019-1042)Online publication date: 12-Jul-2024
https://dl.acm.org/doi/10.1145/3643772
Geimer AVergnolle MRecoules FDaniel LBardin SMaurice CMeng WJensen CCremers CKirda E(2023)A Systematic Evaluation of Automated Tools for Side-Channel Vulnerabilities Detection in Cryptographic LibrariesProceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security10.1145/3576915.3623112(1690-1704)Online publication date: 15-Nov-2023
https://dl.acm.org/doi/10.1145/3576915.3623112

Index Terms

Cache Refinement Type for Side-Channel Detection of Cryptographic Software
1. Security and privacy

Recommendations

Side-Channel Attacks on Cryptographic Software

When it comes to cryptographic software, side channels are an often-overlooked threat. A side channel is any observable side effect of computation that an attacker could measure and possibly influence. In the software world, side-channel attacks have ...
Architecting against Software Cache-Based Side-Channel Attacks

Using cache-like architectural components including data caches, instruction caches, or branch target buffers as a side channel, software cache-based side-channel attacks are able to derive secret keys used in cryptographic operations through legitimate ...
New cache designs for thwarting software cache-based side channel attacks

Software cache-based side channel attacks are a serious new class of threats for computers. Unlike physical side channel attacks that mostly target embedded cryptographic devices, cache-based side channel attacks can also undermine general purpose ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

CCS '22: Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security

November 2022

3598 pages

ISBN:9781450394505

DOI:10.1145/3548606

General Chairs:
Heng Yin
University of California, Riverside
,
Angelos Stavrou
Virginia Tech
,
Program Chairs:
Cas Cremers
CISPA Helmholtz Center for Information Security
,
Elaine Shi
Carnegie Mellon University

Copyright © 2022 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGSAC: ACM Special Interest Group on Security, Audit, and Control

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 07 November 2022

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

CCS '22

Sponsor:

SIGSAC

CCS '22: 2022 ACM SIGSAC Conference on Computer and Communications Security

November 7 - 11, 2022

CA, Los Angeles, USA

Acceptance Rates

Overall Acceptance Rate 1,261 of 6,999 submissions, 18%

Upcoming Conference

CCS '24

Sponsor:
sigsac

ACM SIGSAC Conference on Computer and Communications Security

October 14 - 18, 2024

Salt Lake City , UT , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
321
Total Downloads

Downloads (Last 12 months)100
Downloads (Last 6 weeks)8

Reflects downloads up to 14 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Cai LSong FChen T(2024)Towards Efficient Verification of Constant-Time Cryptographic ImplementationsProceedings of the ACM on Software Engineering10.1145/36437721:FSE(1019-1042)Online publication date: 12-Jul-2024
https://dl.acm.org/doi/10.1145/3643772
Geimer AVergnolle MRecoules FDaniel LBardin SMaurice CMeng WJensen CCremers CKirda E(2023)A Systematic Evaluation of Automated Tools for Side-Channel Vulnerabilities Detection in Cryptographic LibrariesProceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security10.1145/3576915.3623112(1690-1704)Online publication date: 15-Nov-2023
https://dl.acm.org/doi/10.1145/3576915.3623112

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents