path: root/memoria.tex

\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 (<<Indistinguishability under Chosen Plaintext Attack>>) 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 <<lista de enteros>>), y se usa una comilla
simple delante de las variables de tipo (\rawec{'a list} significa <<lista de
cualquier tipo>>).

\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}
%
% <statement> ::= <ident> '=' <expr>
% \alt `for' <ident> `=' <expr> `to' <expr> `do' <statement>
% \alt `{' <stat-list> `}'
% \alt <empty>
%
% <stat-list> ::= <statement> `;' <stat-list> | <statement>
%
% \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
<<hd>> y <<tl>> (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}(<<Satisfiability Modulo Theories>>). 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 <<seguro>> 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}