Gilles Barthe
David Pichardie
ABSTRACT
Cache-based attacks are a class of side-channel attacks that are particularly effective in virtualized or cloud-based environments, where they have been used to recover secret keys from cryptographic implementations. One common approach to thwart cache-based attacks is to use constant-time implementations, i.e., which do not branch on secrets and do not perform memory accesses that depend on secrets. However, there is no rigorous proof that constant-time implementations are protected against concurrent cache-attacks in virtualization platforms with shared cache; moreover, many prominent implementations are not constant-time. An alternative approach is to rely on system-level mechanisms. One recent such mechanism is stealth memory, which provisions a small amount of private cache for programs to carry potentially leaking computations securely. Stealth memory induces a weak form of constant-time, called S-constant-time, which encompasses some widely used cryptographic implementations. However, there is no rigorous analysis of stealth memory and S-constant-time, and no tool support for checking if applications are S-constant-time.
We propose a new information-flow analysis that checks if an x86 application executes in constant-time, or in S-constant-time. Moreover, we prove that constant-time (resp. S-constant-time) programs do not leak confidential information through the cache to other operating systems executing concurrently on virtualization platforms (resp. platforms supporting stealth memory). The soundness proofs are based on new theorems of independent interest, including isolation theorems for virtualization platforms (resp. platforms supporting stealth memory), and proofs that constant-time implementations (resp. S-constant-time implementations) are non-interfering with respect to a strict information flow policy which disallows that control flow and memory accesses depend on secrets. We formalize our results using the Coq proof assistant and we demonstrate the effectiveness of our analyses on cryptographic implementations, including PolarSSL AES, DES and RC4, SHA256 and Salsa20.
- O. Aciiçmez and W. Schindler. A vulnerability in rsa implementations due to instruction cache analysis and its demonstration on openssl. In CT-RSA'08, volume 4964 of LNCS, pages 256--273. Springer, 2008. Google Scholar
Digital Library
- O. Aciicmez, W. Schindler, and Cetin Kaya Koc. Cache based remote timing attack on the AES. In CT-RSA 2007, volume 4377 of LNCS, pages 271--286. Springer, 2007. Google ScholarDigital Library
- J. Agat. Transforming out Timing Leaks. In Proceedings POPL'00, pages 40--53. ACM, 2000. Google ScholarDigital Library
- M. Aizatulin, A. D. Gordon, and J. Jurjens. Computational verification of c protocol implementations by symbolic execution. In CCS 2012, pages 712--723. ACM, 2012. Google ScholarDigital Library
- J. B. Almeida, M. Barbosa, G. Barthe, and F. Dupressoir. Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations. In CCS 2013, 2013. Google ScholarDigital Library
- T. Amtoft, J. Dodds, Z. Zhang, A. W. Appel, L. Beringer, J. Hatcliff, X. Ou, and A. Cousino. Acertificate infrastructure for machine-checked proofs of conditional information flow. In POST 2012, volume 7215 of LNCS, pages 369--389. Springer, 2012. Google ScholarDigital Library
- L. O. Andersen. Program analysis and specialization for the C programming language. PhD thesis, 1994.Google Scholar
- A. Azevedo de Amorim, N. Collins, A. DeHon, D. Demange, C. Hritcu, D. Pichardie, B. C. Pierce, R. Pollack, and A. Tolmach. A verified information-flow architecture. In POPL 2014. ACM, 2014. Google ScholarDigital Library
- A. Banerjee and D. Naumann. Stack-based access control for secure information flow. Journal of Functional Programming, 15:131--177, Mar. 2005. Special Issue on Language-Based Security. Google ScholarDigital Library
- G. Barthe, G. Betarte, J. Campo, and C. Luna. Formally verifying isolation and availability in an idealized model of virtualization. In FM 2011, pages 231--245. Springer-Verlag, 2011. Google ScholarDigital Library
- G. Barthe, G. Betarte, J. Campo, and C. Luna. Cache-Leakage Resilient OS Isolation in an Idealized Model of Virtualization. In CSF 2012, pages 186--197, 2012. Google ScholarDigital Library
- G. Barthe, G. Betarte, J. D. Campo, C. Luna, and D. Pichardie. System-level non-interference for constant-time cryptography (full version), 2014.Google Scholar
- G. Barthe, B. Gregoire, S. Heraud, and S. Zanella-B--eguelin. Computer-aided security proofs for the working cryptographer. In CRYPTO 2011, volume 6841 of LNCS, Heidelberg, 2011. Google ScholarDigital Library
- G. Barthe, B. Kopf, L. Mauborgne, and M. Ochoa. Leakage resilience against concurrent cache attacks. In POST, 2014.Google Scholar
- G. Barthe, D. Pichardie, and T. Rezk. A certified lightweight non-interference java bytecode verifier. In ESOP 2007, pages 125--140, 2007. Google ScholarDigital Library
- G. Barthe, T. Rezk, and D. A. Naumann. Deriving an information flow checker and certifying compiler for java. In S&P 2006, pages 230--242. IEEE Computer Society, 2006. Google ScholarDigital Library
- D. J. Bernstein. Cache-timing attacks on AES, 2005. Available from author's webpage.Google Scholar
- K. Bhargavan, C. Fournet, and A. D. Gordon. Modular verification of security protocol code by typing. In POPL 2010. ACM, 2010. Google ScholarDigital Library
- J. Bonneau and I. Mironov. Cache Collision Timing Attacks Against AES. In CHES '06, 2006. Google ScholarDigital Library
- D. Cade and B. Blanchet. From computationally-proved protocol specifications to implementations. In ARES 2012, pages 65--74. IEEE Computer Society, 2012. Google ScholarDigital Library
- A. Canteaut, C. Lauradoux, and A. Seznec. Understanding cache attacks. Rapport de recherche RR-5881, INRIA, 2006.Google Scholar
- T. Chardin, P.-A. Fouque, and D. Leresteux. Cache timing analysis of RC4. In ACNS 2011, volume 6715 of LNCS, pages 110--129, 2011. Google ScholarDigital Library
- J. Chen, R. Chugh, and N. Swamy. Type-preserving compilation of end-to-end verification of security enforcement. In PLDI 2010, pages 412--423. ACM, 2010. Google ScholarDigital Library
- B. Coppens, I. Verbauwhede, K. D. Bosschere, and B. D. Sutter. Practical mitigations for timing-based side-channel attacks on modern x86 processors. In S&P 2009, pages 45--60, 2009. Google ScholarDigital Library
- M. Dam, R. Guanciale, N. Khakpour, H. Nemati, and O. Schwarz. Formal verification of information flow security for a simple ARM-based separation kernel. In CCS 2013, pages 223--234, 2013. Google ScholarDigital Library
- G. Doychev, D. Feld, B. Kopf, L. Mauborgne, and J. Reineke. Cacheaudit: A tool for the static analysis of cache side channels. In Usenix Security 2013, 2013. Google ScholarDigital Library
- F. Dupressoir, A. D. Gordon, J. Jurjens, and D. A. Naumann. Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols. In CSF 2011, pages 3--17. IEEE Computer Society, 2011. Google ScholarDigital Library
- S. Dziembowski and K. Pietrzak. Leakage-resilient cryptography. In FOCS, pages 293--302. IEEE Computer Society, 2008. Google ScholarDigital Library
- U. Erlingsson and M. Abadi. Operating system protection against side-channel attacks that exploit memory latency. Technical Report MSR-TR-2007--117, Microsoft Research, 2007.Google Scholar
- D. Gullasch, E. Bangerter, and S. Krenn. Cache games - bringing access-based cache attacks on AES to practice. In S&P 2011, pages 490--505, 2011. Google ScholarDigital Library
- E. Kasper and P. Schwabe. Faster and timing-attack resistant aes-gcm. In C. Clavier and K. Gaj, editors, CHES, volume 5747 of Lecture Notes in Computer Science, pages 1--17. Springer, 2009. Google ScholarDigital Library
- J. Kelsey, B. Schneier, D. Wagner, and C. Hall. Side Channel Cryptanalysis of Product Ciphers. Journal of Computer Security, 8(2--3):141--158, 2000. Google ScholarDigital Library
- G. A. Kildall. A unified approach to global program optimization. In Proceedings of the 1st annual ACM SIGACT-SIGPLAN symposium on Principles of programming languages, POPL '73, pages 194--206, New York, NY, USA, 1973. ACM. Google ScholarDigital Library
- T. Kim, M. Peinado, and G. Mainar-Ruiz. Stealthmem: system-level protection against cache-based side channel attacks in the cloud. In USENIX Security 2012, pages 11--11, Berkeley, CA, USA, 2012. USENIX Association. Google ScholarDigital Library
- G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, and S. Winwood. seL4: formal verification of an OS kernel. In SOSP 2009, pages 207--220. ACM, 2009. Google ScholarDigital Library
- P. Kocher. Timing Attacks on Implementations of Diffe-Hellman, RSA, DSS, and Other Systems. In CRYPTO'96, volume 1109 of LNCS, pages 104--113. Springer, 1996. Google ScholarDigital Library
- G. Leander, E. Zenner, and P. Hawkes. Cache Timing Analysis of LFSR-Based Stream Ciphers. In IMACC 2009, volume 5921 of LNCS, pages 433--445. Springer, 2009. Google ScholarDigital Library
- X. Leroy. Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In POPL 2006, pages 42--54. ACM, 2006. Google ScholarDigital Library
- C. Liu, M. Hicks, and E. Shi. Memory trace oblivious program execution. In CSF 2013, pages 51--65, 2013. Google ScholarDigital Library
- D. Molnar, M. Piotrowski, D. Schultz, and D. Wagner. The program counter security model: Automatic detection and removal of control-flow side channel attacks. In ICISC 2005, pages 156--168, 2005. Google ScholarDigital Library
- T. Murray, D. Matichuk, M. Brassil, P. Gammie, T. Bourke, S. Seefried, C. Lewis, X. G., and G. Klein. sel4: from general purpose to a proof of information flow enforcement. In S&P 2013, pages 415--429, 2013. Google ScholarDigital Library
- T. Ristenpart, E. Tromer, H. Shacham, and S. Savage. Hey, you, get off of my cloud! Exploring information leakage in third-party compute clouds. In CCS 2009, pages 199--212. ACM Press, 2009. Google ScholarDigital Library
- V. Robert and X. Leroy. A formally-verified alias analysis. In CPP, pages 11--26, 2012. Google ScholarDigital Library
- J. M. Rushby. Noninterference, Transitivity, and Channel-Control Security Policies. Technical Report CSL-92-02, SRI International, 1992.Google Scholar
- T. Sewell, S. Winwood, P. Gammie, T. Murray, J. Andronick, and G. Klein. seL4 enforces integrity. In ITP 2011, Nijmegen, The Netherlands, 2011. Google ScholarDigital Library
- Z. Shao. Certified software. Commun. ACM, 53(12):56--66, 2010. Google ScholarDigital Library
- D. Stefan, P. Buiras, E. Z. Yang, A. Levy, D. Terei, A. Russo, and D. Mazières. Eliminating cache-based timing attacks with instruction-based scheduling. In J. Crampton, S. Jajodia, and K. Mayes, editors, ESORICS, volume 8134 of Lecture Notes in Computer Science, pages 718--735. Springer, 2013.Google Scholar
- E. Tromer, D. A. Osvik, and A. Shamir. Efficient cache attacks on AES, and countermeasures. J. Cryptology, 23(1):37--71, 2010. Google ScholarDigital Library
- Y. Tsunoo, T. Saito, T. Suzaki, M. Shigeri, and H. Miyauchi. Cryptanalysis of DES implemented on computers with cache. In CHES 2003, volume 2779 of LNCS, pages 62--76. Springer, 2003.Google ScholarCross Ref
- Z. Wang and R. B. Lee. New cache designs for thwarting software cache-based side channel attacks. In ISCA 2007, pages 494--505. ACM, 2007. Google ScholarDigital Library
- D. Zhang, A. Askarov, and A. C. Myers. Predictive mitigation of timing channels in interactive systems. In CCS 2011, pages 563--574. ACM, 2011. Google ScholarDigital Library
Index Terms
- System-level Non-interference for Constant-time Cryptography
Recommendations
System-Level Non-interference of Constant-Time Cryptography. Part II: Verified Static Analysis and Stealth Memory
AbstractThis paper constitutes the second part of a paper published in Barthe et al. (J Autom Reason, 2017. 10.1007/s10817-017-9441-5). Cache-based attacks are a class of side-channel attacks that are particularly effective in virtualized or cloud-based ...
System-Level Non-interference of Constant-Time Cryptography. Part I: Model
This work focuses on the study of constant-time implementations; giving formal guarantees that such implementations are protected against cache-based timing attacks in virtualized platforms where their supporting operating system executes concurrently ...
Comments