Tools for the Evaluation and Choice of Countermeasures against Side-Channel Attacks

摘要

Side-channel attacks have been successful in breaking cryptographic protections of systems, by using secret-dependent variations of non-functional properties such as timing or traffic volume. Countermeasures against side-channel attacks usually attempt to eliminate or reduce these variations, which may lead to performance penalties such as increases in the running time of programs, or in the traffic volume they induce. This thesis investigates the trade-off between the security of side-channel countermeasures, and their cost in terms of performance penalties. For this, we seek rigorous answers to two research questions: Q1: How to choose a balance between the security guarantees and the performance penalties of side-channel countermeasures? Q2: How to measure the security of side-channel countermeasures on practical systems? This thesis develops tools that enable the security quantification and the choice of practical countermeasures against side-channel attacks. These tools include the necessary formal models, as well as algorithms and software tools to allow the automatic evaluation of practical systems. In addressing Q1, we develop the first systematic approach for choosing side-channel countermeasures. We do this in a game-theoretic model, where a defender chooses a protection against an adversary who performs an attack. We apply this approach for reasoning about countermeasures against timing attacks, i.e., attacks where an adversary can exploit secret-dependent execution time of programs. We identify cases where leaky countermeasures are preferable to leak-free, constant-time implementations, as they offer better performance without sacrificing security. In addressing Q2, we develop the first tools for the automatic formal quantification of the security of side-channel countermeasures in practical systems. We do this for two types of attacks: cache attacks, where an adversary exploits secret-dependent timing differences due to the use of the CPU cache, and web-traffic attacks, where an adversary exploits secret-dependent differences in the volume of encrypted traffic. To capture cache attacks, we develop the tool CacheAudit, which performs static analysis of x86 binaries, and quantifies their security with respect to cache adversaries. Using CacheAudit, we analyze implementations of AES from the PolarSSL library, as well as of the finalists of the eSTREAM stream cipher competition, and we reason about the effects of architectural features such as cache size and replacement policy to side-channel leakage. Furthermore, we devise novel techniques that provide support for bit-level and symbolic reasoning about pointers in the presence of dynamic memory allocation, which we apply for reasoning about the effectiveness of several widely deployed side-channel countermeasures from the libgcrypt and OpenSSL libraries. To capture web-traffic attacks, we develop scalable algorithms that enable the formal quantification of web-traffic leakage, as well as the generating of provable protections. We apply these algorithms on practical instances of web applications. RESUMEN Los ataques de canal lateral han sido utilizados con éxito para romper sistemas protegidos criptográficamente. Dichos ataques explotan variaciones en propiedades no funcionales que dependen de la clave secreta, como por ejemplo variaciones en el volumen de tráfico web o en el tiempo de ejecución de un programa. Como protección ante estos ataques de canal lateral, normalmente se intenta eliminar o reducir dichas variaciones, lo que puede empeorar la eficiencia, por ejemplo aumentando el tiempo de ejecución de los programas o el volumen de tráfico que producen. En esta tesis se investiga cómo encontrar un balance entre seguridad contra estos ataques y coste en términos de eficiencia. Para ello, intentamos dar una respuesta rigurosa a dos preguntas de clave: P1: ¿Cómo elegir protecciones contra un canal lateral? Es decir, ¿cuál es un buen balance entre seguridad y eficiencia? P2: ¿Cómo medir la seguridad de dichas protecciones contra canales laterales en sistemas reales? En esta tesis se desarrollan herramientas que permiten cuantificar la seguridad y elegir protecciones prácticas contra ataques de canal lateral. Estas herramientas se basan tanto en modelos formales como en algoritmos y software que permiten el análisis automático de sistemas reales. Para contestar a P1, hemos desarrollado un método para elegir protecciones contra canales laterales de forma sistemática. Para ello utilizamos un modelo de teoría de juegos, en el que un defensor elige una protección contra un adversario que intenta llevar a cabo un ataque. Hemos aplicado este modelo para prevenir ataques de tiempo, es decir, ataques en los que un adversario puede deducir información sobre la clave secreta midiendo el tiempo de ejecución de programas, ya que existe una dependencia entre ambos. Hemos encontrado casos en los que permitir ataques de tiempo es preferible a implementaciones en tiempo constante (que son completamente seguras ante estos ataques), ya que se consigue mejor eficiencia sin sacrificar seguridad. En lo referente a P2, hemos desarrollado las primeras herramientas para cuantificar automática y formalmente la seguridad de protecciones contra ataques de canal lateral. Distinguimos entre dos tipos de ataque: ataques de cache, en los que un adversario explota las diferencias de tiempo provocadas por el uso de la caché de CPU; y ataques sobre el volumen de tráfico web, en los que un adversario explota las diferencias de volumen de tráfico encriptado. Para analizar ataques de cache´, hemos desarrollado la herramienta CacheAudit, que a través de un análisis estático de binarios x86 cuantifica la seguridad de éstos contra ataques de este tipo. Utilizando CacheAudit, hemos analizado implementaciones de AES de la librería PolarSSL, así como los esquemas finalistas de la competición de cifrados en flujo eSTREAM. Además, hemos analizado los efectos de diferentes características dependientes de la arquitectura, como el tamaño de la caché o las políticas de reemplazo. Incluso, hemos ideado nuevas técnicas que proporcionan soporte para razonamiento simbólico (a nivel de bit) de punteros en el caso de asignación dinámica de memoria. Aplicando estas técnicas, hemos analizado la efectividad de protecciones ampliamente extendidas y utilizadas de las librerías libgcrypt y OpenSSL. Para analizar ataques sobre el volumen de tráfico web, hemos desarrollado algoritmos eficientes que permiten cuantificar de manera formal el posible filtramiento de información debido al volumen de tráfico, así como proporcionar protecciones confiables. Hemos aplicado estos algoritmos en ejemplos prácticos de aplicaciones web.