Formally verified countermeasures against cache based attacks in virtualization platforms
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 implement...
Uloženo v:
| Hlavní autor: | |
|---|---|
| Médium: | doctoralThesis |
| Jazyk: | angličtina |
| Vydáno: |
2016
|
| Témata: | |
| On-line přístup: | http://hdl.handle.net/20.500.12008/6401 |
| Tagy: |
Žádné tagy, Buďte první, kdo vytvoří štítek k tomuto záznamu!
|
| _version_ | 1868890061926301696 |
|---|---|
| author | Campo, Juan |
| author_browse | Campo, Juan |
| author_facet | Campo, Juan |
| author_role | author |
| collection | COLIBRI |
| dc.contributor.none.fl_str_mv | Campo Juan, Universidad de la República (Uruguay). Facultad de Ingeniería. |
| dc.creator.none.fl_str_mv | Campo, Juan |
| dc.date.none.fl_str_mv | 2016-06-03T21:20:00Z 2016-06-03T21:20:00Z 2016 |
| dc.format.none.fl_str_mv | 101 h. |
| dc.identifier.none.fl_str_mv | CAMPO, Juan. "Formally verified countermeasures against cache based attacks in virtualization platforms". Tesis de Doctorado. Montevideo : UR.FI.INCO, 2016. 0797-6410 http://hdl.handle.net/20.500.12008/6401 |
| dc.language.none.fl_str_mv | en eng |
| dc.publisher.none.fl_str_mv | UR.FI.INCO |
| dc.rights.none.fl_str_mv | info:eu-repo/semantics/openAccess Licencia Creative Commons Atribución – No Comercial – Sin Derivadas (CC BY-NC-ND 4.0) |
| dc.source.none.fl_str_mv | reponame:COLIBRI instname:Universidad de la República instacron:Universidad de la República |
| dc.subject.none.fl_str_mv | Non-interference Cache-based attacks Constant-time cryptography Stealth memory Coq No interferencia Ataques basados en cache Criptografía constant-time |
| dc.title.none.fl_str_mv | Formally verified countermeasures against cache based attacks in virtualization platforms |
| dc.type.none.fl_str_mv | Tesis de doctorado info:eu-repo/semantics/doctoralThesis info:eu-repo/semantics/acceptedVersion |
| description | 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, 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; 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. We weaken the definition of constant-time, introducing a new program classification called S-constant-time, that captures the behavior of programs that correctly use stealth memory. This new definition encompasses some widely used cryptographic implementations. However, there was no rigorous analysis of stealth memory and S-constant-time, and no tool support for checking if applications are S-constant-time. In this thesis, we propose a new information-flow analysis that checks if an x86 application executes in constant-time or S-constant-time. Moreover, we prove that (S-)constant-time programs do not leak confidential information through the cache to other operating systems executing concurrently on virtualization platforms. The soundness proofs are based on new theorems of independent interest, including isolation theorems for virtualization platforms, and proofs that (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. |
| eu_rights_str_mv | openAccess |
| format | doctoralThesis |
| id | anni_55e04842e0e6fbc158eee806cfd5d675 |
| identifier_str_mv | CAMPO, Juan. "Formally verified countermeasures against cache based attacks in virtualization platforms". Tesis de Doctorado. Montevideo : UR.FI.INCO, 2016. 0797-6410 |
| instacron_str | Universidad de la República |
| institution | Universidad de la República |
| instname_str | Universidad de la República |
| language | eng |
| language_invalid_str_mv | en |
| network_acronym_str | anni |
| network_name_str | oai-lr-anni |
| oai_identifier_str | oai:colibri.udelar.edu.uy:20.500.12008/6401 |
| publishDate | 2016 |
| publishDateSort | 2016 |
| publisher.none.fl_str_mv | UR.FI.INCO |
| reponame_str | COLIBRI |
| repository.mail.fl_str_mv | |
| repository.name.fl_str_mv | |
| repository_id_str | |
| rights_invalid_str_mv | Licencia Creative Commons Atribución – No Comercial – Sin Derivadas (CC BY-NC-ND 4.0) |
| spelling | Formally verified countermeasures against cache based attacks in virtualization platformsCampo, JuanNon-interferenceCache-based attacksConstant-time cryptographyStealth memoryCoqNo interferenciaAtaques basados en cacheCriptografía constant-timeCache 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, 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; 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. We weaken the definition of constant-time, introducing a new program classification called S-constant-time, that captures the behavior of programs that correctly use stealth memory. This new definition encompasses some widely used cryptographic implementations. However, there was no rigorous analysis of stealth memory and S-constant-time, and no tool support for checking if applications are S-constant-time. In this thesis, we propose a new information-flow analysis that checks if an x86 application executes in constant-time or S-constant-time. Moreover, we prove that (S-)constant-time programs do not leak confidential information through the cache to other operating systems executing concurrently on virtualization platforms. The soundness proofs are based on new theorems of independent interest, including isolation theorems for virtualization platforms, and proofs that (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.Los ataques basados en el cache son una clase de ataques de canal lateral (side-channel) particularmente efectivos en entornos virtualizados o basados en la nube, donde han sido usados para recuperar claves secretas de implementaciones criptográficas. Un enfoque común para frustrar los ataques basados en cache es usar implementaciones de tiempo constante (constant-time), las cuales no tienen bifurcaciones basadas en secretos, y no realizan accesos a memoria que dependan de secretos. Sin embargo, no existe una prueba rigurosa de que las implementaciones de tiempo constante están protegidas de ataques concurrentes de cache en plataformas de virtualización. Además, muchas implementaciones populares no son de tiempo constante. Un enfoque alternativo es utilizar mecanismos a nivel del sistema. Uno de los más recientes de estos es stealth memory, que provee una pequeña cantidad de cache privado a los programas para que puedan llevar a cabo de manera segura computaciones que potencialmente filtran información. En este trabajo se debilita la definición de tiempo constante, introduciendo una nueva clasificación de programas llamada S-constant-time, que captura el comportamiento de programas que hacen un uso correcto de stealth memory. Esta nueva definición abarca implementaciones criptográficas ampliamente utilizadas. Sin embargo, hasta el momento no había un análisis riguroso de stealth memory y S-constant-time, y ningún soporte de herramientas que permitan verificar si una aplicación es S-constant-time. En esta tesis, proponemos un nuevo análisis de flujo de información que verifica si una aplicación x86 ejecuta en constant-time o S-constant-time. Además, probamos que los programas (S-)constant-time no filtran información confidencial a través del cache a otros sistemas operativos ejecutando concurrentemente en plataformas de virtualización. La pruebas de corrección están basadas en propiedades que incluyen teoremas, de interés en sí mismos, de aislamiento para plataformas de virtualización y pruebas de que las implementaciones (S-)constant-time son no interferentes con respecto a una política estricta de flujo de información que no permite que el control de flujo y los accesos a memoria dependan de secretos. Formalizamos nuestros resultados utilizando el asistente de pruebas Coq, y mostramos la efectividad de nuestros análisis en implementaciones criptográficas que incluyen PolarSSL AES, DES y RC4, SHA256 y Salsa20.UR.FI.INCOCampo Juan, Universidad de la República (Uruguay). Facultad de Ingeniería.2016-06-03T21:20:00Z2016-06-03T21:20:00Z2016Tesis de doctoradoinfo:eu-repo/semantics/doctoralThesisinfo:eu-repo/semantics/acceptedVersion101 h.CAMPO, Juan. "Formally verified countermeasures against cache based attacks in virtualization platforms". Tesis de Doctorado. Montevideo : UR.FI.INCO, 2016.0797-6410http://hdl.handle.net/20.500.12008/6401reponame:COLIBRIinstname:Universidad de la Repúblicainstacron:Universidad de la RepúblicaenengLas obras depositadas en el Repositorio se rigen por la Ordenanza de los Derechos de la Propiedad Intelectual de la Universidad de la República.(Res. Nº 91 de C.D.C. de 8/III/1994 – D.O. 7/IV/1994) y por la Ordenanza del Repositorio Abierto de la Universidad de la República (Res. Nº 16 de C.D.C. de 07/10/2014)info:eu-repo/semantics/openAccessLicencia Creative Commons Atribución – No Comercial – Sin Derivadas (CC BY-NC-ND 4.0)oai:colibri.udelar.edu.uy:20.500.12008/64012026-04-14T10:27:53Z |
| spellingShingle | Formally verified countermeasures against cache based attacks in virtualization platforms Campo, Juan Non-interference Cache-based attacks Constant-time cryptography Stealth memory Coq No interferencia Ataques basados en cache Criptografía constant-time |
| status_str | acceptedVersion |
| title | Formally verified countermeasures against cache based attacks in virtualization platforms |
| title_full | Formally verified countermeasures against cache based attacks in virtualization platforms |
| title_fullStr | Formally verified countermeasures against cache based attacks in virtualization platforms |
| title_full_unstemmed | Formally verified countermeasures against cache based attacks in virtualization platforms |
| title_short | Formally verified countermeasures against cache based attacks in virtualization platforms |
| title_sort | Formally verified countermeasures against cache based attacks in virtualization platforms |
| topic | Non-interference Cache-based attacks Constant-time cryptography Stealth memory Coq No interferencia Ataques basados en cache Criptografía constant-time |
| url | http://hdl.handle.net/20.500.12008/6401 |