Faltan las implementaciones

1 files changed, 164 insertions, 8 deletions

diff --git a/memoria.tex b/memoria.tex
index 08cfc3d..e666b72 100755
--- a/memoria.tex
+++ b/memoria.tex
@@ -78,10 +78,17 @@ propiedades de seguridad que consideramos favorables. En la mayoría de los caso
 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).
+segundo (ver figura \ref{fig:proofs}). 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).
+
+\begin{figure}[h]
+    \centering
+    \includegraphics[width=0.6\textwidth]{img/proofs.png}
+    \caption{Construcción de pruebas}
+    \label{fig:proofs}
+\end{figure}
 
 \section{Criptografía asimétrica}
 \label{sec:cript-asim}
@@ -652,7 +659,7 @@ una estructura de datos muy simple pero más sencilla de recorrer y manejar.
   estructura sintáctica del código fuente. Este analizador está especificado por
   la gramática formal del lenguaje (gramáticas libres de contexto, por lo
   general), cuyas reglas determinan el algoritmo a seguir durante la
-  construcción del árbol sintáctico.  L
+  construcción del árbol sintáctico.
 \item \textbf{Análisis semántico/contextual}
 Durante esta fase se recorre el árbol sintáctico generado previamente y se anota
 con información de tipos, se construye la tabla de símbolos y se comprueba que
@@ -700,9 +707,8 @@ El siguiente diagrama resume el proceso de análisis del lenguaje de EasyCrypt:
 \end{center}
 
 Para la implementación del coste es necesario modificar cada uno de los módulos
-involucrados en este proceso. A continuación analizaremos cada una de las etapas
-de la implementación tanto del operador especial de coste como del axioma de
-coste.
+involucrados en este proceso. A continuación analizaremos las etapas de la
+implementación tanto del operador especial de coste como del axioma de coste.
 
 \section{Modificaciones al analizador léxico}
 \label{sec:modif-al-anal-lex}
@@ -727,6 +733,156 @@ TODO: Modificaciones en EcPrinting
 
 \chapter{DESARROLLO: INTERFAZ WEB}
 
+Como ya mencionamos en la sección \ref{sec:objetivos}, EasyCrypt es un programa
+complejo y una de las prioridades para favorecer su adopción es facilitar su uso
+en la medida de lo posible.
+
+A lo largo de este capítulo se describirá el proceso de diseño e implementación
+de una interfaz web para trabajar con EasyCrypt remotamente desde un
+navegador.
+
+\section{Diseño}
+\label{sec:diseno-1}
+
+La mayor inspiración que tenemos para el diseño es el del propio Proof General,
+que es con lo que se trabaja en EasyCrypt normalmente:
+
+//
+\\
+\\
+// [screenshot de Emacs + ProofGeneral]
+\\
+\\
+//
+
+En nuestro caso, la parte fundamental de la interfaz será el editor de código
+fuente. Los resultados de la evaluación del código se mostrarán a la derecha del
+mismo, como en Proof General, y añadiremos un navegador de ficheros (ya que el
+código se almacena remotamente). Por último, necesitaremos una barra de
+navegación en la parte superior para realizar actividades complementarias como
+crear proyectos, iniciar/cerrar sesión, etc. En la figura \ref{fig:prototype} se
+puede ver el primer prototipo de la página principal de la web\footnote{A pesar
+  de que la web debe contar con muchas otras páginas (pantalla de inicio,
+  formulario de creación de cuentas de usuario, etc.), en este documento no se
+  mencionarán por no ser tan relevantes en su interacción con EasyCrypt.}.
+
+\begin{figure}[h]
+    \centering
+    \includegraphics[width=0.8\textwidth]{img/web-prototype.png}
+    \caption{Diseño de la web}
+    \label{fig:prototype}
+\end{figure}
+
+En cuanto al diseño del sistema en general, se han utilizado varios marcos y
+herramientas web para implementar toda la funcionalidad necesaria en un nivel
+superior, evitando en la medida de lo posible el uso directo de las tecnologías
+web básicas (HTML, CSS, JavaScript), más tediosas y propensas a error:
+
+\begin{itemize}
+\item \textbf{Django}\footnote{\url{https://www.djangoproject.com/}}. La base
+  del sistema es Django, un marco web usado para implementar la funcionalidad en
+  el lado del servidor. Django está escrito en Python, que es también el
+  lenguaje que se usa para implementar el resto de la funcionalidad. Se ha
+  utilizado el módulo
+  crispy-forms\footnote{\url{https://django-crispy-forms.readthedocs.org/en/latest/}}
+  para poder definir los formularios HTML directamente en Python.
+
+\item \textbf{Twitter
+    Bootstrap}\footnote{\url{http://getbootstrap.com/}}. Bootstrap es un marco
+  orientado al desarrollo de interfaces web. Sus características más
+  interesantes son la gestión del esquema de la web usando un sistema de
+  rejillas, una gran cantidad de clases CSS predefinidas y funcionalidad
+  JavaScript como generación de ventanas <<modales>> (flotantes).
+
+\item \textbf{jQuery}\footnote{\url{http://jquery.com/}}. En el lado del cliente
+  hay mucha funcionalidad dinámica que debe ser implementada en JavaScript.
+  Buena parte de este trabajo consiste en manipular la estructura HTML del
+  documento: el DOM. Para este tipo de tarea se ha usado jQuery, que tiene una
+  gran biblioteca de funciones para crear, eliminar, buscar y modificar nodos
+  HTML, por ejemplo a la hora de mostrar el navegador de ficheros. Asimismo,
+  para poder tener varios ficheros abiertos al mismo tiempo, se ha usado un
+  widget de gestión de pestañas proporcionado por la biblioteca jQuery
+  UI\footnote{\url{http://jqueryui.com/}}.
+
+\item \textbf{Ace}\footnote{\url{http://ace.c9.io/}}. Ace es un editor de código
+  fuente diseñado para integrarse en sitios web. Además, como permite que la
+  misma instancia del editor pueda tener varias sesiones distintas (estados),
+  podemos asociar una sesión a cada pestaña (fichero abierto) y guardar por
+  separado sus estados: posición del cursor, código evaluado, etc.
+
+\item \textbf{WebSockets}\footnote{\url{http://www.websocket.org/}}. Para
+  evaluar remotamente el código definido en el editor es necesario disponer de
+  una conexión persistente y bidireccional con un servidor que ejecute una
+  instancia de EasyCrypt. Precisamente por estas necesidades se ha decidido
+  implementar las comunicaciones entre el cliente web y el servidor de EasyCrypt
+  usando WebSockets, una tecnología relativamente reciente pero soportada por
+  prácticamente todos los navegadores actuales (a la fecha de redacción del
+  presente documento, el único navegador que no soporta WebSockets es Opera
+  Mini). Para la implementación de WebSockets en el lado del servidor de
+  EasyCrypt se ha usado una biblioteca para Python llamada
+  \textbf{Tornado}\footnote{\url{http://www.tornadoweb.org//}}.
+\end{itemize}
+
+Todas estas partes se integran entre sí tal y como se muestra en el siguiente
+esquema:
+
+\tikzstyle{block} = [rectangle, draw, fill=blue!20,
+    text width=5em, text centered, rounded corners, minimum height=4em]
+\tikzstyle{line} = [draw]
+\tikzstyle{cloud} = [draw, ellipse,fill=blue!10, node distance=3cm,
+    minimum height=2em]
+\tikzstyle{ncloud} = [draw, ellipse,fill=blue!10, node distance=2cm,
+    minimum height=2em]
+
+\begin{center}
+\begin{tikzpicture}[node distance = 6cm, auto]
+    % Nodes
+    \node [block] (client) {Cliente};
+    \node [block, right of=client] (wserver) {Servidor web};
+    \node [block, below of=wserver, node distance=4cm] (ecserver) {Servidor EasyCrypt};
+
+    \node [ncloud, above of=client] (bootstrap) {Twitter Bootstrap};
+    \node [cloud, left of=client] (jquery) {jQuery};
+    \node [ncloud, below of=client] (ace) {Ace Editor};
+
+    \node [cloud, right of=wserver] (django) {Django};
+    \node [ncloud, above of=django] (crispy) {crispy_forms};
+
+    \node [cloud, right of=ecserver, fill=green!20] (easycrypt) {EasyCrypt};
+    \node [ncloud, below of=ecserver] (tornado) {Tornado};
+
+    % Edges
+    \path [line,dashed] (bootstrap) -- (client);
+    \path [line,dashed] (jquery) -- (client);
+    \path [line,dashed] (ace) -- (client);
+
+    \path [line,dashed] (django) -- (wserver);
+    \path [line,dashed] (django) -- (crispy);
+
+    \path [line,dashed] (easycrypt) -- (ecserver);
+    \path [line,dashed] (tornado) -- (ecserver);
+
+    \path [line]
+    (client) edge [] node {\textbf{HTTP}} (wserver)
+    (client) edge [] node {\textbf{WebSockets}} (ecserver);
+\end{tikzpicture}
+\end{center}
+
+A continuación veremos cómo se ha implementado cada uno de estos componentes y
+formado el sistema completo.
+
+\section{Implementación: cliente}
+
+TODO
+
+\section{Implementación: servidor web}
+
+TODO
+
+\section{Implementación: servidor EasyCrypt}
+
+TODO
+
 \chapter{RESULTADOS Y CONCLUSIONES}
 
 \chapter{CONTRIBUCIONES}