Goran Doychev
Skip Abstract Section
Abstract
We present CacheAudit, a versatile framework for the automatic, static analysis of cache side channels. CacheAudit takes as input a program binary and a cache configuration and derives formal, quantitative security guarantees for a comprehensive set of side-channel adversaries, namely, those based on observing cache states, traces of hits and misses, and execution times. Our technical contributions include novel abstractions to efficiently compute precise overapproximations of the possible side-channel observations for each of these adversaries. These approximations then yield upper bounds on the amount of information that is revealed.
In case studies, we apply CacheAudit to binary executables of algorithms for sorting and encryption, including the AES implementation from the PolarSSL library, and the reference implementations of the finalists of the eSTREAM stream cipher competition. The results we obtain exhibit the influence of cache size, line size, associativity, replacement policy, and coding style on the security of the executables and include the first formal proofs of security for implementations with countermeasures such as preloading and data-independent memory access patterns.
- Andreas Abel and Jan Reineke. 2013. Measurement-based modeling of the cache replacement policy. In Proceedings of the 2013 IEEE 19th Real-Time and Embedded Technology and Applications Symposium (RTAS). IEEE, 65--74. Google Scholar
Digital Library
- AbsInt Angewandte Informatik GmbH. 2015. AbsInt aiT Worst-Case Execution Time Analyzers. Retrieved from http://www.absint.com/ait/.Google Scholar
- Onur Aciiçmez and Ç. K. KoÇ. 2006. Trace-driven cache attacks on AES. In ICICS. Springer, 112--121. Google ScholarDigital Library
- Onur AciiÇmez, Werner Schindler, and Ç. K. KoÇ. 2007. Cache based remote timing attack on the AES. In CT-RSA. Springer, 271--286. Google ScholarDigital Library
- Johan Agat. 2000. Transforming out timing leaks. In POPL 2000. ACM, 40--53. Google ScholarDigital Library
- Johan Agat and David Sands. 2001. On confidentiality and algorithms. In SSP. IEEE, 64--77. Google ScholarDigital Library
- Michael Backes, Boris Köpf, and Andrey Rybalchenko. 2009. Automatic discovery and quantification of information leaks. In SSP. IEEE, 141--153. Google ScholarDigital Library
- Mirza Basim Baig, Connor Fitzsimons, Suryanarayanan Balasubramanian, Radu Sion, and Donald E. Porter. 2014. CloudFlow: Cloud-wide policy enforcement using fast VM introspection. In IC2E. IEEE.Google Scholar
- Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna, and David Pichardie. 2014a. System-level non-interference for constant-time cryptography. Cryptology ePrint Archive, Report 2014/422. (2014).Google Scholar
- Gilles Barthe, Boris Köpf, Laurent Mauborgne, and Martín Ochoa. 2014b. Leakage resilience against concurrent cache attacks. In Proceedings of the 3rd Conference on Principles of Security and Trust (POST’14). Springer.Google ScholarCross Ref
- Come Berbain, Olivier Billet, Anne Canteaut, Nicolas Courtois, Henri Gilbert, Louis Goubin, Aline Gouget, Louis Granboulan, Cdric Lauradoux, Marine Minier, Thomas Pornin, and Herv Sibert. 2005. Sosemanuk, A Fast Software-oriented Stream Cipher. Retrieved from http://www.ecrypt.eu.org/stream/p3ciphers/sosemanuk/sosemanuk_p3.pdf.Google Scholar
- Daniel Bernstein. 2005. Cache-Timing Attacks on AES. Retrieved from http://cr.yp.to/antiforgery/cachetiming-20050414.pdf.Google Scholar
- Daniel Bernstein. 2015a. Leaks. Retrieved from http://cr.yp.to/streamciphers/leaks.html.Google Scholar
- Daniel Bernstein. 2015b. Snuffle 2005: The Salsa20 Encryption Function. Retrieved from http://cr.yp.to/snuffle.html.Google Scholar
- Martin Boesgaard, Mette Vesterager, Thomas Christensen, and Erik Zenner. 2005. The Stream Cipher Rabbit. Retrieved from http://www.ecrypt.eu.org/stream/p3ciphers/rabbit/rabbit_p3.pdf.Google Scholar
- FranÇois Bourdoncle. 1993. Efficient chaotic iteration strategies with widenings. In FMPA. Springer.Google Scholar
- Christelle Braun, Konstantinos Chatzikokolakis, and Catuscia Palamidessi. 2009. Quantitative notions of leakage for one-try attacks. Electron. Notes Theor. Comput. Sci. 249 (2009), 75--91. Google ScholarDigital Library
- Adam Chlipala. 2006. Modular development of certified program verifiers with a proof assistant. In ICFP. ACM, 160--171. Google ScholarDigital Library
- David Clark, Sebastian Hunt, and Pasquale Malacaria. 2007. A static analysis for quantifying information flow in a simple imperative language. JCS 15, 3 (2007), 321--371. Google ScholarDigital Library
- David Cock, Qian Ge, Toby Murray, and Gernot Heiser. 2014. The last mile: An empirical study of timing channels on seL4. In CCS. ACM. Google ScholarDigital Library
- Code Beach. 2008. Sorting Algorithms. Retrieved from http://www.codebeach.com/2008/09/sorting-algorithms-in-c.html.Google Scholar
- Bart Coppens, Ingrid Verbauwhede, Koen De Bosschere, and Bjorn De Sutter. 2009. Practical mitigations for timing-based side-channel attacks on modern x86 processors. In SSP. IEEE, 45--60. Google ScholarDigital Library
- Patrick Cousot and Radhia Cousot. 1977. Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fixpoints. In POPL. 238--252. Google ScholarDigital Library
- Patrick Cousot and Radhia Cousot. 1979. Systematic design of program analysis frameworks. In POPL. Google ScholarDigital Library
- Patrick Cousot, Radhia Cousot, and Laurent Mauborgne. 2012. Theories, solvers and static analysis by abstract interpretation. J. ACM 59, 6 (2012), 31. Google ScholarDigital Library
- Yevgeniy Dodis, Rafail Ostrovsky, Leonid Reyzin, and Adam Smith. 2008. Fuzzy extractors: How to generate strong keys from biometrics and other noisy data. SIAM J. Comput. 38, 1 (2008), 97--139. Google ScholarDigital Library
- Leonid Domnitser, Aamer Jaleel, Jason Loew, Nael B. Abu-Ghazaleh, and Dmitry Ponomarev. 2012. Non-monopolizable caches: Low-complexity mitigation of cache side channel attacks. TACO 8, 4 (2012), 35. Google ScholarDigital Library
- Goran Doychev, Dominik Feld, Boris Köpf, Laurent Mauborgne, and Jan Reineke. 2013. CacheAudit: A tool for the static analysis of cache side channels. In Proceedings of the 22nd USENIX Security Symposium. USENIX. Google ScholarDigital Library
- Stefan Dziembowski and Krzysztof Pietrzak. 2008. Leakage-resilient cryptography. In FOCS. IEEE. Google ScholarDigital Library
- ECRYPT. 2012. The eSTREAM Portfolio in 2012. Retrieved from http://www.ecrypt.eu.org/documents/D.SYM.10-v1.pdf.Google Scholar
- Úlfar Erlingsson and Martín Abadi. 2007. Operating System Protection Against Side-Channel Attacks That Exploit Memory Latency. Technical Report.Google Scholar
- Dominik Feld. 2013. Relational Domains for the Quantification of Cache Side Channels. Master’s thesis. Saarland University.Google Scholar
- Christian Ferdinand, Florian Martin, Reinhard Wilhelm, and Martin Alt. 1999. Cache behavior prediction by abstract interpretation. Sci. Comput. Program. 35, 2 (1999), 163--189. Google ScholarDigital Library
- Bryan Ford. 2012. Plugging side-channel leaks with timing information flow control. In HotCloud. USENIX. Google ScholarDigital Library
- Daniel Grund. 2012. Static Cache Analysis for Real-Time Systems -- LRU, FIFO, PLRU. Ph.D. Dissertation. Saarland University.Google Scholar
- Shay Gueron. 2010. Intel Advanced Encryption Standard (AES) Instructions Set. Retrieved from http://software.intel.com/file/24917.Google Scholar
- David Gullasch, Endre Bangerter, and Stephan Krenn. 2011. Cache games - Bringing access-based cache attacks on AES to practice. In SSP. IEEE, 490--505. Google ScholarDigital Library
- Reinhold Heckmann, Marc Langenbach, Stephan Thesing, and Reinhard Wilhelm. 2003. The influence of processor architecture on the design and the results of WCET tools. IEEE Proc. Real-Time Syst. 91, 7 (2003), 1038--1054.Google ScholarCross Ref
- Daniel Hedin and David Sands. 2005. Timing aware information flow security for a JavaCard-like bytecode. ENTCS 141, 1 (2005), 163--182. Google ScholarDigital Library
- Jonathan Heusser and Pasquale Malacaria. 2010. Quantifying information leaks in software. In ACSAC. ACM, 261--269. Google ScholarDigital Library
- Suman Jana and Vitaly Shmatikov. 2012. Memento: Learning secrets from process footprints. In SSP. IEEE, 143--157. Google ScholarDigital Library
- Emilia Käsper and Peter Schwabe. 2009. Faster and timing-attack resistant AES-GCM. In CHES. 1--17. Google ScholarDigital Library
- Taesoo Kim, Marcus Peinado, and Gloria Mainar-Ruiz. 2012. StealthMem: System-level protection against cache-based side channel attacks in the cloud. In Proceedings of the 19th USENIX Security Symposium. USENIX. Google ScholarDigital Library
- Johannes Kinder, Florian Zuleger, and Helmut Veith. 2009. An abstract interpretation-based framework for control flow reconstruction from binaries. In VMCAI. Springer, 214--228. Google ScholarDigital Library
- Paul Kocher. 1996. Timing attacks on implementations of Diffie-Hellman, RSA, DSS, and other systems. In CRYPTO. Springer, 104--113. Google ScholarDigital Library
- Paul Kocher, Joshua Jaffe, and Benjamin Jun. 1999. Differential power analysis. In CRYPTO. Springer. Google ScholarDigital Library
- Boris Köpf and David Basin. 2007. An information-theoretic model for adaptive side-channel attacks. In CCS. ACM, 286--296. Google ScholarDigital Library
- Boris Köpf, Laurent Mauborgne, and Martín Ochoa. 2012. Automatic quantification of cache side-channels. In CAV. Springer, 564--580. Google ScholarDigital Library
- Boris Köpf and Andrey Rybalchenko. 2010. Approximation and randomization for quantitative information-flow analysis. In CSF. IEEE, 3--14. Google ScholarDigital Library
- Boris Köpf and Geoffrey Smith. 2010. Vulnerability bounds and leakage resilience of blinded cryptography under timing attacks. In CSF. IEEE, 44--56. Google ScholarDigital Library
- Gregor Leander, Erik Zenner, and Philip Hawkes. 2009. Cache timing analysis of LFSR-based stream ciphers. In Cryptography and Coding. Springer, 433--445. Google ScholarDigital Library
- Laurent Mauborgne and Xavier Rival. 2005. Trace partitioning in abstract interpretation based static analyzers. In ESOP (LNCS), Vol. 3444. Springer, 5--20. Google ScholarDigital Library
- Ziyuan Meng and Geoffrey Smith. 2011. Calculating bounds on information leakage using two-bit patterns. In PLAS. ACM. Google ScholarDigital Library
- David Molnar, Matt Piotrowski, David Schultz, and David Wagner. 2006. The program counter security model: Automatic detection and removal of control-flow side channel attacks. In Information Security and Cryptology-ICISC 2005. Springer, 156--168. Google ScholarDigital Library
- James Newsome, Stephen McCamant, and Dawn Song. 2009. Measuring channel capacity to distinguish undue influence. In PLAS. ACM, 73--85. Google ScholarDigital Library
- Dag Arne Osvik, Adi Shamir, and Eran Tromer. 2006. Cache attacks and countermeasures: The case of AES. In CT-RSA (LNCS), Vol. 3860. Springer, 1--20. Google ScholarDigital Library
- Goutam Paul and Shashwat Raizada. 2012. Impact of extending side channel attack on cipher variants: A case study with the HC series of stream ciphers. In Security, Privacy, and Applied Cryptography Engineering. Springer, 32--44. Google ScholarDigital Library
- Colin Percival. 2005. Cache missing for fun and profit. In BSDCan.Google Scholar
- Himanshu Raj, Ripal Nathuji, Abhishek Singh, and Paul England. 2009. Resource management for isolation enhanced cloud services. In Proceedings of the ACM Cloud Computing Security Workshop (CCSW’09). 77--84. Google ScholarDigital Library
- Thomas Ristenpart, Eran Tromer, Hovav Shacham, and Stefan Savage. 2009. Hey, you, get off of my cloud: Exploring information leakage in third-party compute clouds. In CCS. ACM, 199--212. Google ScholarDigital Library
- Geoffrey Smith. 2009. On the foundations of quantitative information flow. In FoSSaCS. Springer. Google ScholarDigital Library
- Mohit Tiwari, Jason Oberg, Xun Li, Jonathan Valamehr, Timothy E. Levin, Ben Hardekopf, Ryan Kastner, Frederic T. Chong, and Timothy Sherwood. 2011. Crafting a usable microkernel, processor, and I/O system with strict and provable information flow security. In ISCA. ACM, 189--200. Google ScholarDigital Library
- Zhenghong Wang and Ruby B. Lee. 2007. New cache designs for thwarting software cache-based side channel attacks. In ISCA. ACM, 494--505. Google ScholarDigital Library
- Zhenghong Wang and Ruby B. Lee. 2008. A novel cache architecture with enhanced performance and security. In 41st IEEE/ACM International Symposium on Microarchitecture (MICRO). 83--93. Google ScholarDigital Library
- Hongjun Wu. 2004. The Stream Cipher HC-128. Retrieved from http://www.ecrypt.eu.org/stream/p3ciphers/hc/hc128_p3.pdf.Google Scholar
- Yuval Yarom and Katrina Falkner. 2014. FLUSH+RELOAD: A high resolution, low noise, L3 cache side-channel attack. In Proceedings of the 23rd USENIX Security Symposium. 719--732. Google ScholarDigital Library
- Yu Yu, FranÇois-Xavier Standaert, Olivier Pereira, and Moti Yung. 2010. Practical leakage-resilient pseudorandom generators. In CCS. ACM, 141--151. Google ScholarDigital Library
- Erik Zenner. 2009. A cache timing analysis of HC-256. In Selected Areas in Cryptography. Springer. Google ScholarDigital Library
- Danfeng Zhang, Aslan Askarov, and Andrew C. Myers. 2012a. Language-based control and mitigation of timing channels. In PLDI. ACM, 99--110. Google ScholarDigital Library
- Yinqian Zhang, Ari Juels, Michael K. Reiter, and Thomas Ristenpart. 2012b. Cross-VM side channels and their use to extract private keys. In CCS. ACM. Google ScholarDigital Library
Index Terms
- CacheAudit: A Tool for the Static Analysis of Cache Side Channels
Recommendations
CleanupSpec: An "Undo" Approach to Safe Speculation
MICRO '52: Proceedings of the 52nd Annual IEEE/ACM International Symposium on MicroarchitectureSpeculation-based attacks affect hundreds of millions of computers. These attacks typically exploit caches to leak information, using speculative instructions to cause changes to the cache state. Hardware-based solutions that protect against such forms ...
DUCATI: High-performance Address Translation by Extending TLB Reach of GPU-accelerated Systems
Conventional on-chip TLB hierarchies are unable to fully cover the growing application working-set sizes. To make things worse, Last-Level TLB (LLT) misses require multiple accesses to the page table even with the use of page walk caches. Consequently, ...
Disruptive prefetching: impact on side-channel attacks and cache designs
SYSTOR '15: Proceedings of the 8th ACM International Systems and Storage ConferenceCaches are integral parts in modern computers; they leverage the memory access patterns of a program to mitigate the gap between the fast processors and slow memory components.
Unfortunately, the behavior of caches can be exploited by attackers to infer ...
Comments