\documentclass[12pt,a4paper,parskip=full]{scrreprt} \usepackage[top=3.5cm,bottom=3.5cm,left=3cm,right=3cm]{geometry} \usepackage[spanish]{babel} \usepackage[utf8]{inputenc} \usepackage{url} \usepackage{graphicx} \usepackage{cite} \usepackage{amsmath} \usepackage{mathtools} \usepackage{listings} \usepackage{syntax} \usepackage[compact,small]{titlesec}\usepackage[usenames,dvipsnames]{xcolor} \usepackage[pagebackref,colorlinks=true,linkcolor=black,urlcolor=black,citecolor=blue]{hyperref} \usepackage{perpage} \input{defs} \MakePerPage{footnote} \def\emptypage{\newpage\thispagestyle{empty}\mbox{}} \title{Trabajo de fin de Grado} \author{Guillermo Ramos Gutiérrez - r090050} \date{TODO} \begin{document} \maketitle \pagenumbering{roman} \emptypage \chapter*{Resumen} \chapter*{Abstract} \emptypage \tableofcontents \chapter{INTRODUCCIÓN} \label{cha:introduccion} \pagenumbering{arabic} \setcounter{page}{1} Con el paso del tiempo, la sociedad está aumentando progresivamente su dependencia de los sistemas informáticos, tanto a nivel local como global (internet). La gente gestiona sus cuentas bancarias por internet, está permanentemente en contacto con sus conocidos a través de aplicaciones de mensajería instantánea y almacena en \textit{la nube} gran cantidad de material personal. Esta dependencia trae consigo la necesidad de tener unas ciertas garantías de seguridad (confidencialidad, disponibilidad, integridad) tanto a la hora de transmitir la información como de almacenarla. Construir un sistema de seguridad no es una tarea fácil, ya que a menudo consta de muchos componentes que han de ser examinados individualmente de forma rigurosa para poder afirmar que el conjunto es seguro. Uno de los componentes básicos de prácticamente cualquier sistema de seguridad es la criptografía. Su utilidad no se limita a impedir que una persona no autorizada con acceso a datos privados pueda entenderlos (cifrado), sino que también cubre otras necesidades como la de verificación de identidad (autenticación) o la de poder garantizar de que una información no ha sido alterada (integridad). Poniendo como ejemplo el caso de una persona accediendo via web a la página web de su banco para realizar una transferencia, la criptografía juega un papel central a la hora de garantizar la seguridad de la operación: un protocolo de transporte seguro empleará un esquema de criptografía asimétrica para garantizar al cliente que el servidor es quien dice ser, un algoritmo de cifrado para hacer imposible que cualquier intermediario pueda interceptar la comunicación, y un código de autenticación de mensaje para verificar que los datos no se modifican mientras están viajando. Por lo general, estas primitivas criptográficas basan su seguridad en la dificultad computacional que tiene resolver ciertos problemas. Por ejemplo, uno de los protocolos más utilizados para autenticar servidores, RSA, se basa en que un atacante que intente suplantar al servidor en cuestión tendrá antes que descomponer un número en dos factores primos, problema que se considera inabordable para números lo suficientemente grandes (con la capacidad computacional actual). Como resultado, normalmente no se habla en términos de seguridad absoluta, sino de seguridad \textbf{condicionada a la capacidad computacional del atacante}. Para estar seguros de que los mecanismos criptográficos realmente cumplen con su cometido, es necesario someterlos a un proceso de verificación riguroso. El objetivo es poder razonar sobre ellos y demostrar que cumplen ciertas propiedades de seguridad que consideramos favorables. En la mayoría de los casos se intenta encontrar una \textbf{reducción} \cite{GoldwasserM84} del criptosistema a un problema difícil computacionalmente, de forma que un ataque exitoso contra el primero implicaría poder resolver de forma eficiente el segundo. Continuando el ejemplo anterior, RSA se considera seguro porque la existencia de un ataque eficiente contra el criptosistema implicaría también la existencia de una forma eficiente de factorizar enteros (que hasta el día de hoy, se desconoce). \section{Criptografía asimétrica} \label{sec:cript-asim} En esta sección se introducirán algunos conceptos fundamentales de criptografía asimétrica, ya que serán de utilidad a la hora de explicar la siguiente sección (\ref{sec:secuencias-de-juegos}) y algunos ejemplos posteriores. La criptografía \textbf{asimétrica} o \textbf{de clave pública} engloba todos aquellos algoritmos criptográficos que usan dos funciones, $\Enc$ y $\Dec$, para cifrar y descifrar la información respectivamente. Intuitivamente, cifrar una información consiste en modificarla hasta hacerla ininteligible. Cada una de estas funciones usa una \textbf{clave} distinta para llevar a cabo su tarea, por lo que es necesario un procedimiento de generación de claves $\KG$ para conseguir un par de claves pública-privada $(pk,sk)$. Las funciones de cifrado y descifrado tienen la siguiente forma: $$\Enc(pk,T) = C$$ $$\Dec(sk,C) = T$$ Donde $T$ significa \textbf{texto en claro} o \textbf{mensaje}, y $C$, \textbf{texto cifrado} o \textbf{cifra}. Para que un esquema de criptografía asimétrica sea útil, siempre que el par $(pk,sk)$ se haya generado en una sola llamada a $\KG$ se debe cumplir la siguiente ecuación: $$\forall t \in T. \Dec(sk, \Enc(pk, t)) = t$$ Dicho de otra forma, la función de descifrado \textbf{invierte} la función de cifrado. El objetivo es que cualquier persona pueda mandar un mensaje cifrado al propietario de un par de claves sabiendo que sólo dicho propietario podrá descifrar el mensaje. \section{Secuencias de juegos} \label{sec:secuencias-de-juegos} Hoy en día, las demostraciones relacionadas con criptografía siguen una estructura denominada \textbf{secuencia de juegos} \cite{Shoup04}. Básicamente consisten en definir \textbf{juegos} entre un \textbf{desafiador} (\textit{challenger}) y un \textbf{adversario} (\textit{adversary}) , ambos representados como programas probabilísticos: \begin{game}[caption=IND-CPA (\cite{BartheGB09})]{}{} $(pk,sk) \leftarrow \KG();$ $(m_0,m_1) \leftarrow A_1(pk);$ $b \overset{\$}{\leftarrow} \{0,1\};$ $c \leftarrow \Enc(pk,m_b);\\$ $\tilde{b} \leftarrow A_2(c)$ \end{game} El Juego 1 define la propiedad de seguridad IND-CPA (<>) de los esquemas de cifrado asimétrico. El adversario está representado como la pareja de procedimientos $(A_1,A_2)$. El desafiador crea un par de claves $(pk,sk)$, permite que el adversario elija dos textos $(m_0,m_1)$ conociendo $pk$, cifra aleatoriamente uno de los dos y se lo entrega al adversario para que adivine cuál de los dos textos originales fue cifrado. Si el adversario no es capaz de acertar con una probabilidad mayor que $1/2$ (intento a ciegas), se considera que el criptosistema cumple la propiedad IND-CPA. En general, a cada juego se le asocia un \textbf{evento} $S$ y una \textbf{probabilidad objetivo}, y se dice que cumple su propiedad de seguridad cuando para cualquier posible adversario, la posibilidad de que ocurra el evento $S$ es arbitrariamente cercana a la probabilidad objetivo. En el Juego 1, el evento al finalizar la ejecución del juego sería $b=\tilde{b}$ (el adversario logra adivinar cuál de sus dos textos fue cifrado); y la probabilidad objetivo, 1/2. Una secuencia de juegos es un conjunto de juegos en el que la probabilidad de que suceda el evento $S$ en cada juego es muy cercana a la del juego previo. En \cite{Shoup04} se demuestra que el criptosistema ElGamal efectivamente cumple la propiedad IND-CPA realizando una reducción del juego original de IND-CPA (para $\KG$ y $\Enc$ los algoritmos de generación de claves y de cifrado, respectivamente, de ElGamal) a uno en el que se resuelve el problema de decisión de Diffie-Hellman, ambos con una probabilidad de $S$ muy cercana. Esta demostración es válida porque el problema de decisión de Diffie-Hellman se considera inabordable a día de hoy. \section{EasyCrypt} \label{sec:easycrypt} El proceso de elaborar estas demostraciones es una tarea ardua y propensa a error, por lo que últimamente se han empezado a desarrollar herramientas para abordar la construcción y verificación de estas demostraciones en forma de secuencias de juegos, como CertiCrypt y su versión mejorada EasyCrypt \cite{BartheGHB11}. EasyCrypt es un marco formado por un \textbf{lenguaje de programación} junto a un motor de resolución de \textbf{lógica de Hoare Relacional Probabilística} (ver sección \ref{sec:juicios}) \cite{BartheGB09}. EasyCrypt funciona como un intérprete de un lenguaje de propósito general y de forma interactiva: cuando se le proporciona un fichero fuente a evaluar, lo recorre de arriba hacia abajo comprobando que todos los pasos de las demostraciones son correctos. Usando Proof General, un modo del editor de texto Emacs, es posible editar un fichero fuente mientras el intérprete lo va evaluando sobre la marcha, ayudando y guiando al usuario a medida que éste desarrolla cada demostración. EasyCrypt usa varios lenguajes de programación distintos a la hora de evaluar un código fuente. A continuación veremos cuáles son, con algunos ejemplos. \subsection{Lenguajes de especificacion} \label{sec:leng-de-espec} Estos lenguajes se usan para declarar y definir tipos, funciones, axiomas, juegos, oráculos, adversarios, entidades involucradas en las pruebas, etc. \paragraph{Lenguaje de expresiones} El lenguaje principal de especificación de EasyCrypt es el de las \textbf{expresiones}, que define una serie de tipos y operadores sobre ellos. EasyCrypt soporta tipos polimórficos de orden superior. Los operadores son funciones totales definidas sobre tipos (conjuntos de valores). Aunque los operadores se definen de forma abstracta (sin proporcionar una implementación), EasyCrypt asume que todos los tipos están habitados, por lo que cualquier aplicación de un operador debe generar un tipo habitado al menos por un valor. La semántica de los operadores viene de la definición de lemas y axiomas que describen su comportamiento de forma observacional, o extensional. Para soportar operadores que reciban varios argumentos se usa la técnica de la \textbf{currificación} (\textit{currying}), que convierte una función de múltiples argumentos en una que al ser aplicada al primer argumento devuelve una nueva función que recibe el segundo argumento, y así sucesivamente. Por ejemplo $f : (A \times B\times C) \rightarrow D$ pasaría a ser $f : A \rightarrow (B \rightarrow (C \rightarrow D))$, o lo que es lo mismo, $f : A \rightarrow B \rightarrow C \rightarrow D$. Los argumentos de los tipos polimórficos se colocan delante del tipo en cuestión (\rawec{int list} significa <>), y se usa una comilla simple delante de las variables de tipo (\rawec{'a list} significa <>). \begin{easycrypt}[caption=Lenguaje de expresiones]{}{} type 'a predicate = 'a -> bool. datatype 'a option = None | Some of 'a. op find : 'a predicate -> 'a list -> 'a option. axiom find_head : forall (x : bool) (l : bool list), hd l = x => find (lambda e, e = x) l = Some x. \end{easycrypt} \paragraph{Lenguaje de expresiones probabilísticas} Para poder razonar sobre distribuciones de probabilidad, EasyCrypt proporciona un tipo (\rawec{'a distr}) que representa sub-distribuciones discretas sobre \rawec{'a}. La principal herramienta para trabajar sobre sub-distribuciones es el operador (\rawec{op mu : 'a distr -> ('a -> bool) -> real}), que devuelve la probabilidad de un evento. Por ejemplo, la distribución uniforme sobre booleanos está definida en la biblioteca estándar de EasyCrypt de la siguiente manera (\rawec{charfun} es la función característica de p evaluado en x, es decir, devuelve 1 si p x = true y 0 si p x = false): \begin{easycrypt}[caption=Distribución uniforme sobre bool]{}{} op dbool : bool distr. axiom mu_def : forall (p : bool -> bool), mu dbool p = (1/2) * charfun p true + (1/2) * charfun p false. \end{easycrypt} \paragraph{Lenguaje pWhile} Los lenguajes de expresiones a menudo son inadecuados para definir juegos y otras estructuras de datos como esquemas de cifrado u oráculos, debido a la necesidad de representar algoritmos secuenciales, entidades con estado, etc. Para ello, EasyCrypt implementa un lenguaje distinto llamado pWhile (probabilistic While) \cite{BartheGB09}. \begin{bnf}[caption=Lenguaje pWhile]{}{} $\mathcal{I ::= V \leftarrow E}$ | $\mathcal{V \overset{\$}{\leftarrow} DE}$ | if $\mathcal{E}$ then $\mathcal{C}$ else $\mathcal{C}$ | while $\mathcal{E}$ do $\mathcal{C}$ | $\mathcal{V} \leftarrow \mathcal{P}(\mathcal{E}, ..., \mathcal{E})$ | $\mathcal{C} ::=$ skip | $\mathcal{I}$; $\mathcal{C}$ \end{bnf} % % https://tex.stackexchange.com/questions/24886/which-package-can-be-used-to-write-bnf-grammars % \setlength{\grammarparsep}{20pt plus 1pt minus 1pt} % \setlength{\grammarindent}{12em} % \begin{grammar} % % ::= '=' % \alt `for' `=' `to' `do' % \alt `{' `}' % \alt % % ::= `;' | % % \end{grammar} \subsection{Lenguajes de demostración} \label{sec:leng-de-demostr} Estos lenguajes se usan para definir lemas y demostrarlos. \paragraph{Juicios} \label{sec:juicios} Los juicios son proposiciones que se pueden realizar en EasyCrypt, y tienen asociado un valor de verdad (pueden ser ciertos o falsos). Para demostrar su veracidad, un juicio deberá demostrarse usando el lenguaje de tácticas (detallado a continuación). Además de los juicios expresados en lógica de primer orden, EasyCrypt cuenta con diversos tipos de juicio derivados de la Lógica de Hoare que se usan para razonar sobre la ejecución de programas: \begin{itemize} \item Lógica de Hoare (\textit{HL}). Tienen la siguiente forma: $$c : P \Longrightarrow Q$$ donde $P$ y $Q$ son aserciones (predicados) y $c$ es un mandato o programa. $P$ es la \textbf{precondición} y $Q$ es la \textbf{postcondición}. El juicio expresa que si la precondición se cumple al momento de ejecutar el mandato, la postcondición también se cumplirá cuando éste termine (si es que lo hace). \item Lógica de Hoare probabilística (\textit{pHL}). A los juicios de Hoare anteriores se les asigna una probabilidad, que puede ser exacta o una cota superior/inferior. $$[c : P \Longrightarrow Q] \leq \delta$$ $$[c : P \Longrightarrow Q] = \delta$$ $$[c : P \Longrightarrow Q] \geq \delta$$ \item Lógica de Hoare relacional probabilística (\textit{pRHL}). Tienen la siguiente forma: $$c_1 \sim c_2 : \Psi \Longrightarrow \Phi$$ En este caso, el juicio expresa que si la precondición $\Psi$ se cumple antes de la ejecución de $c_1$ y $c_2$, tras su ejecución también se cumplirá la postcondición $\Phi$. En este caso las (pre,post)condiciones son \textbf{relaciones} entre las memorias de los dos programas, por lo que este tipo de juicios expresa una \textbf{equivalencia} entre dos programas con respecto a ellas. Además, en este caso los programas $c_1$ y $c_2$ son probabilísticos: su evaluación produce como resultado una distribución de probabilidad sobre los posibles estados en los que se podrá encontrar la memoria al ser ejecutado. \end{itemize} \paragraph{Tácticas} \label{sec:tactics} Para demostrar juicios, EasyCrypt cuenta con un lenguaje basado en tácticas (\textit{tactics}). Una demostración consiste en una secuencia de tácticas que se van ejecutando iterativamente, donde cada táctica aplica una transformación sintáctica al \textbf{objetivo} actual (la fórmula que se está demostrando) hasta que el último resuelve finalmente el objetivo. \begin{easycrypt}[caption=Uso de tácticas]{} lemma hd_tl_cons : forall (xs:'a list), xs <> [] => (hd xs)::(tl xs) = xs. proof. intros xs. elim / list_ind xs. simplify. intros x xs' IH h {h}. rewrite hd_cons. rewrite tl_cons. reflexivity. qed. \end{easycrypt} En este ejemplo obtenido de la biblioteca estándar de EasyCrypt (ligeramente modificado para mejorar su comprensión) se ilustra cómo se realizan las demostraciones. Lo que aparece a continuación del nombre del lema es su especificación formal en lógica de primer orden: una propiedad acerca de la descomposición de las listas en cabeza (\textit{head}) y cola (\textit{tail}). Lo que aparece a continuación es la demostración del lema, con una táctica por cada línea. La demostración se vale de algunos axiomas definidos anteriormente como el de la inducción sobre listas (list_ind) o la definición de <> y <> (hd_cons, tl_cons). Una táctica que vale la pena destacar es \rawec{smt}, que intenta resolver el objetivo actual de la demostración invocando \textbf{resolvedores} (\textit{solvers}) \textbf{SMT}(<>). Estas herramientas están diseñadas para intentar encontrar soluciones a fórmulas expresadas en lógica de primer orden, permitiendo ciertas interpretaciones adicionales sobre los símbolos. Normalmente soportan ciertas teorías muy útiles en criptografía como arrays, listas, aritmética entera, etc., y a menudo son capaces de resolver de forma automática partes repetitivas y tediosas de las demostraciones, liberando de esa carga de trabajo al criptógrafo. \section{Motivación y objetivos} \label{sec:motiv-y-objet} Para este trabajo se ha decidido contribuir dentro de lo posible a mejorar el sistema EasyCrypt, desarrollado principalmente en el Instituto IMDEA Software en Madrid. Aunque es un sistema que ya se ha utilizado para demostrar la seguridad de construcciones criptográficas ampliamente usadas como el criptosistema de Cramer-Shoup o el modo de operación CBC para cifradores de bloque, EasyCrypt sigue en constante desarrollo y tiene muchas posibilidades de ampliación. En concreto, en este trabajo se abordarán e intentarán resolver dos problemas de distinta índole: \begin{itemize} \item \textbf{La posibilidad de trabajar con el coste de algoritmos.} Para poder deducir la capacidad computacional requerida para romper un criptosistema se necesita un método para especificar el coste computacional asociado a computar ciertas operaciones. El objetivo es ser capaz de relacionar la seguridad de un sistema con los recursos del atacante, por ejemplo para afirmar que el sistema es seguro mientras los recursos del atacante no superen cierto límite. Trabajar con costes implica, por una parte, \textbf{especificarlos}, y por otra \textbf{usarlos para demostrar} lemas. La primera parte del proyecto consistirá en la implementación de un mecanismo que permita su \textbf{especificación}, ya que implementar un mecanismo para demostrar con ellos es una tarea considerablemente difícil y que supera los objetivos del Trabajo de Fin de Grado. \item \textbf{Mejorar la usabilidad del sistema.} Idealmente, EasyCrypt debería ser utilizado por criptólogos como herramienta de verificación, pero para ello es necesario hacer su uso lo más sencillo posible. Aunque EasyCrypt es bastante más usable que su predecesor CertiCrypt, sigue estando lejos de ser sencillo. La primera barrera de entrada consiste en su propia instalación: es necesario clonar el repositorio donde está alojado el código y compilarlo junto con sus dependencias (proceso que puede llegar a tardar hasta una hora). Además, toda la interacción con EasyCrypt se realiza a través de ProofGeneral y Emacs, por lo que tiene que estar instalado y el usuario debe de tener cierta experiencia para usarlo cómodamente. Una forma relativamente sencilla de eliminar esta barrera de entrada es ofrecer una interfaz web con todo lo necesario para usar EasyCrypt sin tenerlo instalado en el sistema local. Además de ahorrar tiempo en la instalación y en aprender a usar Emacs, haría más sencillo trabajar desde múltiples sitios al tener toda la estructura del proyecto centralizada en el servidor remoto. En la segunda parte del proyecto se llevará a cabo el diseño e implementación de este sitio web, con el fin de hacer más sencillo usar EasyCrypt y fomentar su utilización en los círculos de gente que se dedica a la criptografía. \end{itemize} \pagebreak \chapter{DESARROLLO: COSTE} \label{cha:desarrollo:-coste} La principal aportación de EasyCrypt con respecto a otros demostradores de teoremas como Coq\footnote{\url{http://coq.inria.fr/}} o Isabelle/HOL\footnote{\url{http://isabelle.in.tum.de/}} son todas las facilidades que proporciona para trabajar concretamente en el ámbito de la criptografía. Algunos ejemplos son el soporte a demostraciones basadas en secuencias de juegos, la riqueza de juicios (lógica de Hoare y variantes) o su exhaustiva biblioteca estándar, que define tipos de datos habituales (cadenas de bits, distribuciones probabilísticas, etc.), funciones para manipularlos, axiomas y lemas de uso común, etc. Un concepto muy significativo en criptografía es el del \textbf{coste}. El coste de un algoritmo es una medida de los recursos (tiempo, espacio, ...) que requiere su ejecución. Como hemos visto en la introducción, salvo en casos muy concretos (OTP \cite{Shannon49}), la criptografía basa su seguridad en la capacidad computacional del adversario. Por tanto, existen muchas propiedades que se pueden expresar acerca de la seguridad de un criptosistema que de una u otra forma dependen del coste de llevar a cabo un ataque contra él. A lo largo de este capítulo se detallará el proceso que se ha seguido para implementar la funcionalidad que permita a la especificación del coste de algoritmos en EasyCrypt. TODO referencias a dónde se explica qué. \newpage \section{Ejemplo de uso} \label{sec:ejemplo-de-uso} Supongamos que el usuario está construyendo una demostración de que un criptosistema de clave pública es seguro siempre que los recursos del adversario no sean superiores a cierto límite. En este caso, por <> nos referimos a que el adversario no es capaz de descifrar un texto cifrado sin poseer la clave privada correspondiente. Como hemos visto en la sección \ref{sec:cript-asim}, esto es equivalente a decir que no es capaz de \textbf{invertir} la función de cifrado. \section{Objetivos} Operador, axioma. \section{Arquitectura de EasyCrypt} \label{sec:arqu-de-easycrypt} EasyCrypt es un programa complejo, y antes de poder modificarlo hay que entender qué partes lo integran y cómo está organizado a nivel de código. \begin{enumerate} \item Lexer \item Parser \item AST \item ... \end{enumerate} % ProofGeneral % EasyCrypt % Why3 % Solvers % \section{Ejemplo de uso (del coste)} % $$\forall (lst : [\alpha]) (p : \alpha -> bool) (x : \alpha). cost[find, p, lst] % <= cost[p, x] * length(lst)$$ \chapter{DESARROLLO: INTERFAZ WEB} \chapter{RESULTADOS Y CONCLUSIONES} \chapter{CONTRIBUCIONES} \chapter{ANEXOS} \pagebreak \bibliography{bib}{} \bibliographystyle{ieeetr} \end{document}