System-Level Non-interference of Constant-Time Cryptography. Part II: Verified Static Analysis and Stealth Memory
- PDF / 1,518,870 Bytes
- 45 Pages / 439.37 x 666.142 pts Page_size
- 61 Downloads / 194 Views
System-Level Non-interference of Constant-Time Cryptography. Part II: Verified Static Analysis and Stealth Memory Gilles Barthe1 · Gustavo Betarte2 · Juan Diego Campo2 · Carlos Luna2 David Pichardie3
·
Received: 30 March 2019 / Accepted: 8 February 2020 © Springer Nature B.V. 2020
Abstract This paper constitutes the second part of a paper published in Barthe et al. (J Autom Reason, 2017. https://doi.org/10.1007/s10817-017-9441-5). Cache-based attacks are a class of sidechannel 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. those 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. We propose a new information-flow analysis that checks if an x86 application executes in constant-time, and show that constant-time programs do not leak confidential information through the cache to other operating systems executing concurrently on virtualization platforms. Our static analysis targets the pre-assembly language of the CompCert verified compiler. Its soundness proof is based on a connection between CompCert semantics and our idealized model of virtualization, and uses isolation theorems presented in Part I. We then extend our model of virtualization platform and our static analysis to accommodate stealth memory, a countermeasure 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. Our results provide the first rigorous analysis of stealth memory and S-constant-time, and the first tool support for checking if applications are S-constant-time. 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. Keywords Non-interference · Cache-based attacks · Constant-time cryptography · Stealth memory · Coq
Extended author information available on the last page of the article
123
G. Barthe et al.
1 Introduction Cache-based attacks are side-channel attacks in which a malicious party is able to obtain confidential data through observing cache accesses of programs. They are particularly effective in cloud-based environments, where hardware support is virtualized and shared among tenants. In such settings, a malicious tenant can manage that an operating system under its control co-resides with the operating system which executes the program that the attacker targets. This allows the attacker to share the cache with its victim and to make fine-grained observations about its own cac
Data Loading...
