path: root/memoria.tex

% Preguntas:
% - BNF?
% - Numeración independiente Juego/Ejemplo/... en lstlisting

\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,citecolor=blue]{hyperref}

\input{defs}

\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}
\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{Secuencias de juegos}

Hoy en día, las demostraciones siguen una estructura denominada
\textbf{secuencia de juegos} \cite{Shoup04}. Básicamente consisten en definir
\textit{juegos} entre un \textit{desafiador} y un \textit{adversario}, ambos
representados como programas probabilísticos:

\renewcommand{\lstlistingname}{Juego}
\begin{lstlisting}[mathescape=true,frame=single,
                   caption=IND-CPA (fuente: \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{lstlisting}

El Juego 1 define la propiedad de seguridad
IND-CPA\footnote{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 una pareja 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 un 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 $E$ 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}

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 \textit{lenguaje de programación} junto a
un motor de resolución de \textit{lógica de Hoare Relacional Probabilística}
\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 es posible ir
escribiendo un fichero fuente a la vez que el intérprete va evaluando lo que ya
se ha escrito, ayudando y guiando al usuario a medida que éste va desarrollando
cada demostración.

EasyCrypt usa varios lenguajes de programación distintos a la hora de evaluar un
código fuente. A continuación veremos mostrará cuáles son, con algunos ejemplos.

\subsection{Lenguajes de especificacion}

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
\textit{currificación}, 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$.

\renewcommand{\lstlistingname}{Ejemplo}
\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
(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=Definición de la 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}.

\renewcommand{\lstlistingname}{Listado}
\begin{lstlisting}[mathescape=true,frame=single,caption=Gramática de pWhile]
  $\mathcal{I} ::= \mathcal{V} \leftarrow \mathcal{E}$
    | $\mathcal{V} \overset{\$}{\leftarrow} \mathcal{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{lstlisting}

% % 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}

Estos lenguajes se usan para definir lemas y demostrarlos.

\paragraph{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 los tactics
(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 (\textbf{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 \textit{precondición} y $Q$ es la
  \textit{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 (\textbf{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 (\textbf{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
  \textit{relaciones} entre las memorias de los dos programas, por lo que este
  tipo de juicios expresa una \textit{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{Tactics}
Para demostrar juicios, EasyCrypt cuenta con un lenguaje basado en
\textit{tactics}. Una demostración consiste en una secuencia de \textit{tactics}
que se van ejecutando iterativamente, donde cada \textit{tactic} aplica una
transformación sintáctica al \textit{objetivo} actual (la fórmula que se está
demostrando) hasta que el último resuelve finalmente el objetivo.

\renewcommand{\lstlistingname}{Ejemplo}
\begin{easycrypt}[caption=Uso de tactics]{}
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 y cola. Lo que aparece a continuación es
la demostración del lema, con un \textit{tactic} 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).

Un \textit{tactic} que vale la pena destacar es \rawec{smt}, que intenta
resolver el objetivo actual de la demostración invocando \textit{resolvedores
  SMT (Satisfiability Modulo Theories)} externos. 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}

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, 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 Emacs
  (editor de texto), 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}

TODO TODO TODO

\section{Arquitectura de EasyCrypt}

\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} % plain, alpha, apalike

\end{document}