diff options
Diffstat (limited to 'memoria.tex')
| -rwxr-xr-x | memoria.tex | 155 |
1 files changed, 114 insertions, 41 deletions
diff --git a/memoria.tex b/memoria.tex index 1cfdf99..74f85db 100755 --- a/memoria.tex +++ b/memoria.tex @@ -63,14 +63,14 @@ increasing. Cryptography is one of the cornerstones of security, so there has been a considerable amount of effort devoted recently to the development of tools oriented to the evaluation and improvement of cryptographic algorithms. One of these tools is EasyCrypt, developed recently at IMDEA -Software Institute in response to the increasing need of reliable cryptographic +Software Institute in response to the increasing need of reliable cryptography verification tools. Throughout this document we will design and implement two -additional EasyCrypt features. +different EasyCrypt features. In the first part of the document we will consider the importance of having a way to specify the cost of algorithms in order to develop proofs that depend on -it, and then we will modify the EasyCrypt's language so the user can tackle a -wider range of problems. +it, and then we will modify the EasyCrypt's language so that the user can tackle +a wider range of problems. In the second part we will assess EasyCrypt's poor usability and try to improve it by developing a web interface which enables the user to use it easily and @@ -168,6 +168,7 @@ En esta sección se introducirán algunos conceptos fundamentales de criptografà 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. +\newpage 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 @@ -310,6 +311,7 @@ axiom find_head : hd l = x => find (lambda e, e = x) l = Some x. \end{easycrypt} +\newpage Las primeras dos lÃneas defininen los tipos \rawec{predicate} y \rawec{option}. El primero representa funciones que devuelven \rawec{bool}, y el segundo, datos que pueden tomar los valores \rawec{None} o \rawec{Some x} (se @@ -355,6 +357,7 @@ necesidad de representar algoritmos secuenciales, entidades con estado, etc. Para ello, EasyCrypt implementa un lenguaje distinto llamado pWhile (probabilistic While) \cite{BartheGB09}. +\newpage \begin{bnf}[caption=Lenguaje pWhile, label={lst:pwhile}]{}{} $\mathcal{I ::= V \leftarrow E}$ | $\mathcal{V \overset{\$}{\leftarrow} DE}$ @@ -741,15 +744,19 @@ siguientes: bien formado sintácticamente, tiene sentido semánticamente. \end{itemize} -EasyCrypt implementa cada una de estas etapas en tres módulos (EcLexer, EcParser -y EcTyping) y define las estructuras de datos intermedias en otros dos -(EcParseTree para el árbol sintáctico abstracto y EcFol para el árbol sintáctico -anotado con información de tipos). Los módulos EcLexer y EcParser hacen uso de -la biblioteca Menhir mencionada anteriormente para generar los analizadores. -Estos módulos contienen las definiciones de tokens y las reglas de las -gramáticas regular y libre de contexto usadas para indicar, respectivamente, el -comportamiento de los analizadores léxico y sintáctico. Todo este proceso -aparece ilustrado en la figura \ref{fig:ecparser}. +EasyCrypt implementa las dos primeras etapas en los módulos EcLexer y EcParser, +define el árbol sintáctico abstracto en EcParseTree, y la generación del árbol +anotado con tipos es responsabilidad de módulos especializados en su ámbito. En +nuestro caso la transformación semántica la realiza el módulo EcTyping, con las +estructuras de datos anotadas definidas en EcFol, ya que son los módulos +encargado de gestionar fórmulas de primer orden, como veremos con más detalle en +las secciones \ref{sec:modif-al-anal-sin} y \ref{sec:modif-al-anal-sem}. Los +módulos EcLexer y EcParser hacen uso de la biblioteca Menhir mencionada +anteriormente para generar los analizadores. Estos módulos contienen las +definiciones de tokens y las reglas de las gramáticas regular y libre de +contexto usadas para indicar, respectivamente, el comportamiento de los +analizadores léxico y sintáctico. Todo este proceso aparece ilustrado en la +figura \ref{fig:ecparser}. \tikzstyle{line} = [draw] @@ -900,9 +907,9 @@ type pcaxiom = { El axioma de coste es un ``record'' (estructura de datos con varios campos) que almacena su nombre, argumentos (opcionales) y especificación. La especificación -es una fórmula: expresiones que pueden estar cuantificadas existencialmente o -universalmente. Por tanto, también necesitaremos modificar el tipo de datos -fórmula para que pueda contener expresiones de coste: +es una fórmula de primer orden: expresiones que pueden estar cuantificadas +existencial o universalmente. Por tanto, también necesitaremos modificar el +tipo de datos fórmula para que pueda contener expresiones de coste: \begin{code} \begin{minted}{ocaml} @@ -950,13 +957,84 @@ más compleja: modificar el analizador semántico. \section{Modificaciones al analizador semántico} \label{sec:modif-al-anal-sem} -TODO: Modificaciones en EcTyping, EcFol, EcEnv, EcScope, EcTheory, EcPV, -EcCommands... :) +El análisis semántico en EasyCrypt fundamentalmente consiste en la comprobación +de tipos (incluyendo de ámbito y entorno). A continuación se expondrá a muy alto +nivel cómo se ha abordado la implementación, ya que en EasyCrypt el análisis +contextual es muy exhaustivo y complejo. Para más detalles se aconseja al lector +interesado que obtenga el código fuente desde la página web del proyecto. + +El módulo principal encargado de implementar la funcionalidad del analizador +semántico (comprobar los tipos y anotar el árbol sintáctico abstracto) es +<<EcTyping>>. Este módulo exporta funciones que transforman fórmulas definidas +en EcParseTree, sin información semántica, en fórmulas definidas en el módulo +EcFol, obtenidas tras realizar las comprobaciones necesarias y portando +información semántica. + +La función que más nos interesa es trans_form: + +\begin{code} + \begin{minted}{ocaml} +val trans_form : env -> unienv -> pformula -> ty -> EcFol.form + \end{minted} + \caption{Tipo de la función trans_form (ecTyping.mli)} +\end{code} + +Sin entrar en detalles, esta función convierte una fórmula (<<pformula>>) en una +fórmula anotada (<<EcFol.form>>) en función del entorno léxico (<<env>>), el +entorno de unificación (<<unienv>>) y el tipo de datos esperado +(<<ty>>). Necesitamos una variante de esta función que soporte también +fórmulas que contengan expresiones de coste, pero que solo se pueda invocar +cuando la fórmula aparezca dentro de un axioma de coste. + +Para ello, modificaremos la función original para que reciba un argumento +booleano adicional ``cost'' que si esa fórmula puede contener expresiones de +coste o no, y para no romper la compatibilidad, la convertiremos en una función +auxiliar <<_trans_form>> y crearemos dos funciones <<trans_form>> y +<<trans_cform>> que la invoquen con el valor correcto de ``cost'': + +\tikzstyle{block} = [rectangle, draw, fill=blue!20, + text width=8em, text centered, rounded corners, minimum height=4em] +\begin{figure}[H] + \centering + \begin{tikzpicture}[node distance = 3cm, auto] + \node [block] (form) {trans_form(args)}; + \node [invisbl, right of=form] (dummy) {}; + \node [block, right of=dummy] (cform) {trans_cform(args)}; + \node [block, below of=dummy, text width=12em] (aux) {_trans_form(cost, args)}; + \path [line, -latex'] + (form) edge node[left] {\textbf{cost = false}} (aux) + (cform) edge node {\textbf{cost = true}} (aux); + \end{tikzpicture} +\end{figure} + +\newpage +Además, habrá que añadir el caso en que <<_trans_form>> sea invocado con una +expresión de coste: + +\begin{code}[H] + \begin{minted}{ocaml} + | PFcost pcexpr -> + if cost + then f_cost (transcexp env ue pcexpr) + else tyerror f.pl_loc env NotInCostEnv + \end{minted} + \caption{Transformación de cformula para expresiones de coste (ecTyping.ml)} +\end{code} -% \section{Modificaciones al pretty-printer} -% \label{sec:modif-al-pretty} +Como podemos ver, lanza un error en caso de incluirse una expresión de coste +fuera de un entorno válido (axioma de coste). El valor de retorno lo delega a la +función transcexp, que busca el operador objetivo en el entorno, aplica +recursivamente la transformación semántica sobre sus argumentos y unifica sus +tipos (para que sea ilegal, por ejemplo, escribir \rawec{cost[sum, true, + 2]}). Aquà concluye la transformación semántica de la expresión de coste. -% TODO: Modificaciones en EcPrinting +La otra parte, el axioma de coste, es más sencilla de implementar. La función +que lleva a cabo su transformación semántica ha de definirse en el módulo +EcCommands, ya que el axioma de coste es una sentencia básica del lenguaje (es +uno de los pasos que puede ejecutar el evaluador). Su trabajo es crear un nuevo +entorno para las variables cuantificadas universalmente, transformar +recursivamente su especificación bajo ese entorno ampliado y añadirlo al ámbito +global para su posterior referencia. \emptypage @@ -1083,7 +1161,6 @@ minimum height=2em] \path [line,dashed] (django) -- (wserver); \path [line,dashed] (django) -- (crispy); - \path [line,dashed] (easycrypt) -- (ecserver); \path [line,dashed] (tornado) -- (ecserver); \path [line] @@ -1199,6 +1276,7 @@ con una captura de pantalla de su resultado una vez servidas: etc. No se usa directamente, sino que se importa desde otras plantillas usando la directiva \textbf{extends} de Django. +\newpage \item \textbf{login.html}, servida cuando se accede a la página de inicio de sesión. Un ejemplo de su resultado final: @@ -1219,6 +1297,7 @@ con una captura de pantalla de su resultado una vez servidas: \label{fig:register} \end{figure} +\newpage \item \textbf{index.html}, la plantilla que sirve la pantalla principal. Cuando no hay ninguna sesión iniciada, se muestra un mensaje de bienvenida: @@ -1296,6 +1375,7 @@ views.file_mrg(request, file_id=13) (``/files'', ``/projects'', etc) y devuelven información en formato JSON. \end{itemize} +\newpage \section{Implementación: cliente} \label{sec:impl-cliente} @@ -1346,14 +1426,8 @@ ws = new Workspace(); Cabe destacar la presencia del atributo <<Workspace.ui>>, que contiene referencias a los nodos DOM con los que se modifica la parte visible del editor. -A continuación veremos los pasos que se han realizado para abordar la -implementación del cliente, partiendo del diseño de la figura -\ref{fig:prototype}. - -\subsection{Colocación de elementos} %TODO quitar (Ãndice) -\label{sec:coloc-de-elem} - -A la hora de distribuir los elementos de la página principal se ha usado una +A la hora de distribuir los elementos de la página principal (de acuerdo al +diseño de la figura \ref{fig:prototype}) se ha usado una caracterÃstica concreta de Twitter Bootstrap: su sistema de rejillas\footnote{\url{http://getbootstrap.com/css/\#grid}}. Bootstrap define dos elementos para trabajar con rejillas: \textbf{filas} y \textbf{columnas}. Se @@ -1438,9 +1512,7 @@ pestañas y editor de código se muestra en la figura \ref{fig:editor}. \end{figure} El coloreado sintáctico se ha tenido que definir a mano, ya que evidentemente -Ace no incluye por defecto soporte para el coloreado de EasyCrypt. % TODO anexo? - -% TODO Ace soporta ... (guardar, ejecutar, colorear) +Ace no incluye por defecto soporte para el coloreado de EasyCrypt. \subsection{Presentación de resultados} \label{sec:pres-de-result} @@ -1485,7 +1557,12 @@ extremo (WebSocket o entrada de EasyCrypt, respectivamente). \chapter{CONTRIBUCIONES} \label{cha:contribuciones} -TODO coste +En la primera parte del documento se ha implementado la definición del coste en +el lenguaje de expresiones de EasyCrypt modificando su analizador del +lenguaje. Como se indica en la sección de objetivos (\ref{sec:objetivos}), el +siguiente paso natural es implementar tácticas y juicios que permitan usar estas +definiciones para extraer conclusiones reales, ampliando considerablemente el +abanico de teoremas que se puedan extraer del uso de EasyCrypt. En cuanto a la interfaz web, se ha conseguido implementar exitosamente un sistema multiusuario capaz de gestionar, editar y ejecutar proyectos de @@ -1498,11 +1575,9 @@ métodos formales que tanto podrÃan aportar al mundo de la seguridad. \begin{figure}[h] \centering - \includegraphics[width=1\textwidth]{img/web-finished.png} + \includegraphics[width=0.9\textwidth]{img/web-finished.png} \end{figure} -% TODO se adjunta el código aparte por si acaso - \chapter{CONCLUSIONES} \label{cha:result-y-concl} @@ -1510,8 +1585,6 @@ A lo largo de este documento hemos abordado la mejora de dos aspectos relativamente independientes de EasyCrypt: una principalmente técnica (coste) y otra de usabilidad (interfaz web). -% TODO qué he aprendido - EasyCrypt es un marco orientado a un usuario muy concreto: profesionales de la criptografÃa. Si bien es cierto que en el propio Instituto IMDEA Software se usa y desarrolla activamente, el objetivo último serÃa crear comunidad. La @@ -1533,10 +1606,10 @@ conclusión más general, serÃa que incluso los sistemas más complejos y de á puramente académico necesitan usuarios, y a todo usuario le gusta que se lo pongan un poco más fácil. El tiempo dirá si ha valido la pena el esfuerzo. -\chapter{ANEXOS} % TODO quitar? +\chapter{ANEXOS} \label{cha:anexos} -Todo el código desarrollado en el presente trabajo, una vez superados los +Todo el código desarrollado en el presente trabajo, una vez pasados los protocolos de integración, se incorporará a la versión estable de EasyCrypt y podrá obtenerse desde el sitio web (\url{https://www.easycrypt.info}). |