Commit d7017e68 authored by Peter Schwabe's avatar Peter Schwabe
Browse files

Complete restructuring, messing with pretty much every file.

parent d668f985
% \subsection*{Abstract}
\begin{abstract}
By using the Coq formal proof assistant, we first extend
the formalization of elliptic curves of Bartzia and Strub to support
Montgomery curves. Then with the Verified Software Toolchain
we prove the soundness and correctness of TweetNaCl's Curve25519 implementation.
\end{abstract}
...@@ -169,7 +169,7 @@ int crypto_scalarmult(u8 *q, ...@@ -169,7 +169,7 @@ int crypto_scalarmult(u8 *q,
} }
\end{lstlisting} \end{lstlisting}
\subsection{What need to be proven?} \subsection{What needs to be proven?}
Verifying \texttt{crypto\_scalarmult} also implies to verify all the functions Verifying \texttt{crypto\_scalarmult} also implies to verify all the functions
subsequently called: \texttt{unpack25519}; \texttt{A}; \texttt{Z}; \texttt{M}; subsequently called: \texttt{unpack25519}; \texttt{A}; \texttt{Z}; \texttt{M};
......
FILES := $(wildcard *.tex) $(wildcard tikz/*.tex) $(wildcard *.sty) FILES := $(wildcard *.tex) $(wildcard tikz/*.tex) $(wildcard *.sty)
curve25519.pdf: FORCE $(FILES) collection.bib tweetverif.pdf: FORCE $(FILES) collection.bib
./latexrun.py curve25519.tex ./latexrun.py tweetverif.tex
depend: depend:
@echo $(FILES) @echo $(FILES)
......
% \subsection*{Abstract}
\begin{abstract}
In this paper we formally prove that the C implementation of
X25519 key exchange in the TweetNaCl library matches
the mathematical definition of X25519 from Bernstein's 2006 paper.
The proof is computer-verified using the Coq theorem prover.
To establish the link between C and Coq we use the
Verified Software Toolchain (VST).
\end{abstract}
\section{Conclusion}
\subsection{TCB of the proof}
\todo{Explain and compare to, e.g., F*}
\subsection{Proof toolchain}
\section{Proving that X25519 in Coq matches the mathematical model}
\section{Introduction} XXX: NaCl
XXX: TweetNaCl (find real-world use of TweetNaCl?)
XXX:
``TweetNaCl is the
first cryptographic library that allows correct functionality to be verified
by auditors with reasonable effort''
XXX: One core component of TweetNaCl (and NaCl) is X25519, mention use
of X25519 in the wild.
TweetNaCl\cite{BGJ+15} is a compact reimplementation of the TweetNaCl\cite{BGJ+15} is a compact reimplementation of the
NaCl\cite{BLS12} high security cryptographic library. NaCl\cite{BLS12} high security cryptographic library.
...@@ -26,8 +37,13 @@ However this first method cannot be applied to an existing piece of software. ...@@ -26,8 +37,13 @@ However this first method cannot be applied to an existing piece of software.
In such case we need to write the specifications and then verify the correctness In such case we need to write the specifications and then verify the correctness
of the implementation. of the implementation.
\subsection{Our Formal Approach} \subheading{Contribution of this paper}
\todo{Proof that TweetNaCl's X25519 code correctly implements math definition from 25519 paper}
\todo{State additional contributions, e.g., extension of EC framework by Bartiza and Strub.}
\subheading{Our Formal Approach.}
Verifying an existing cryptographic library, we use the second approach. Verifying an existing cryptographic library, we use the second approach.
Our method can be seen as a static analysis over the input values coupled Our method can be seen as a static analysis over the input values coupled
with the formal proof that the code of the algorithm matches its specification. with the formal proof that the code of the algorithm matches its specification.
...@@ -49,10 +65,12 @@ Bartzia and Strub wrote a formal library for elliptic curves\cite{DBLP:conf/itp/ ...@@ -49,10 +65,12 @@ Bartzia and Strub wrote a formal library for elliptic curves\cite{DBLP:conf/itp/
We extend it to support Montgomery curves. With this formalization, we prove the We extend it to support Montgomery curves. With this formalization, we prove the
correctness of a generic Montgomery ladder and show that our specification is an instance of it. correctness of a generic Montgomery ladder and show that our specification is an instance of it.
\subsection{Related Works} \subheading{Related work.}
Similar approaches have been used to prove the correctness of OpenSSL HMAC \todo{Separate verification of existing code from generating proof-carrying code.}
\cite{Beringer2015VerifiedCA} and SHA-256 \cite{2015-Appel}. Compared to their work
Similar approaches have been used to prove the correctness of OpenSSL HMAC~\cite{Beringer2015VerifiedCA}
and SHA-256~\cite{2015-Appel}. Compared to their work
our approaches makes a complete link between the C implementation and the formal our approaches makes a complete link between the C implementation and the formal
mathematical definition of the group theory behind elliptic curves. mathematical definition of the group theory behind elliptic curves.
...@@ -69,18 +87,20 @@ Curve25519 implementations has already been under the scrutiny \cite{Chen2014Ver ...@@ -69,18 +87,20 @@ Curve25519 implementations has already been under the scrutiny \cite{Chen2014Ver
However in this paper we provide a proofs of correctness and soundness of a C program up to However in this paper we provide a proofs of correctness and soundness of a C program up to
the theory of elliptic curves. the theory of elliptic curves.
\subsection{Organization of this paper and reproducibility} \todo{Add 1-2 sentences about how this compares? Different limitations etc.}
\subheading{Reproducing the proofs.}
To maximize reusability of our results we placed the code of our formal proofs To maximize reusability of our results we placed the code of our formal proofs
presented in this paper into the public domain. They are available at XXXXXXX presented in this paper into the public domain. They are available at XXXXXXX
with instructions of how to compile and verify our proofs. with instructions of how to compile and verify our proofs.
Section \ref{sec2-implem} gives the necessary background on Curve25519 \subheading{Organization of this paper.}
Section~\ref{sec2-implem} gives the necessary background on Curve25519
implementation in TweetNaCl and provides the specifications we later prove correct. implementation in TweetNaCl and provides the specifications we later prove correct.
Section \ref{sec3-maths} describes our extension of the formal library by Bartzia and Strub. Section~\ref{sec3-maths} describes our extension of the formal library by Bartzia and Strub.
Section \ref{sec4-refl} makes the link between the mathematical model and the C implementation. Section~\ref{sec4-refl} makes the link between the mathematical model and the C implementation.
In this section we also describe some of the techniques we used to speed up some of the proofs. In this section we also describe some of the techniques we used to speed up some of the proofs.
Section \ref{sec5-vst} provides with attention points a VST user should be careful Section~\ref{sec5-vst} provides with attention points a VST user should be careful
of in order to avoid unnecessary work. of in order to avoid unnecessary work.
...@@ -101,3 +121,4 @@ of in order to avoid unnecessary work. ...@@ -101,3 +121,4 @@ of in order to avoid unnecessary work.
% \end{itemize} % \end{itemize}
% %
% Add comparison with Fiat-crypto % Add comparison with Fiat-crypto
\section{Proving equivalence of X25519 in C and Coq}
...@@ -210,3 +210,4 @@ ...@@ -210,3 +210,4 @@
\newcommand{\eg}{{\it e.g.}\;} \newcommand{\eg}{{\it e.g.}\;}
\newcommand{\p}{\ensuremath{2^{255}-19}} \newcommand{\p}{\ensuremath{2^{255}-19}}
\newcommand{\Zfield}{\ensuremath{\mathbb{Z}_{2^{255}-19}}} \newcommand{\Zfield}{\ensuremath{\mathbb{Z}_{2^{255}-19}}}
\newcommand{\Ffield}{\ensuremath{\mathbb{F}_{2^{255}-19}}}
\section{Preliminaries}
\subsection{The X25519 key exchange}
XXX: math definition from Cure25519 paper.
\subsection{X25519 in TweetNaCl}
\subheading{The Montgomery ladder}
\todo{Ladder algorithm C code}
\todo{Ladderstep algorithm C code}
\subheading{Arithmetic in \Ffield}
\todo{C code or just explanation and C code later.}
\subsection{Coq and VST}
...@@ -47,9 +47,12 @@ ...@@ -47,9 +47,12 @@
\usepackage{xspace} \usepackage{xspace}
\usepackage{subfig} \usepackage{subfig}
\usepackage{float} \usepackage{float}
\usepackage{todonotes}
\usepackage[capitalise,nameinlink]{cleveref} \usepackage[capitalise,nameinlink]{cleveref}
\newcommand{\todo}[1]{
{\color{red} \bf TODO: #1}
}
\floatstyle{ruled} \floatstyle{ruled}
\newfloat{Listing}{htb}{lst} \newfloat{Listing}{htb}{lst}
\floatstyle{plain} \floatstyle{plain}
......
\subsection{The complete X25519 code from TweetNaCl}
XXX
% TEMPLATE for Usenix papers, specifically to meet requirements of
% USENIX '05
% originally a template for producing IEEE-format articles using LaTeX.
% written by Matthew Ward, CS Department, Worcester Polytechnic Institute.
% adapted by David Beazley for his excellent SWIG paper in Proceedings,
% Tcl 96
% turned into a smartass generic template by De Clarke, with thanks to
% both the above pioneers
% use at your own risk. Complaints to /dev/null.
% make it two column with no page numbering, default is 10 point
% Munged by Fred Douglis <douglis@research.att.com> 10/97 to separate
% the .sty file from the LaTeX source template, so that people can
% more easily include the .sty file into an existing document. Also
% changed to more closely follow the style guidelines as represented
% by the Word sample file.
% Note that since 2010, USENIX does not require endnotes. If you want
% foot of page notes, don't include the endnotes package in the
% usepackage command, below.
% This version uses the latex2e styles, not the very ancient 2.09 stuff.
% \documentclass[letterpaper,twocolumn,9pt]{article} % \documentclass[letterpaper,twocolumn,9pt]{article}
\documentclass[conference, 9pt]{IEEEtran} \documentclass[conference]{IEEEtran}
% \usepackage{usenix} % \usepackage{usenix}
\usepackage{epsfig} \usepackage{epsfig}
\usepackage{setup} \usepackage{setup}
...@@ -40,10 +18,7 @@ ...@@ -40,10 +18,7 @@
\date{} \date{}
%make title bold and 14 pt font (Latex default is non-bold, 16 pt) %make title bold and 14 pt font (Latex default is non-bold, 16 pt)
\title{\Large \bf A Coq proof of Tweetnacl's Curve25519 correctness.% \title{\Large \bf A Coq proof of Tweetnacl's X25519 correctness.}
\thanks{
Date: somewhen in 2019.}
}
%for single author (just remove % characters) %for single author (just remove % characters)
\ifpublic \ifpublic
...@@ -57,7 +32,7 @@ The Netherlands} ...@@ -57,7 +32,7 @@ The Netherlands}
The Netherlands} The Netherlands}
\and \and
\IEEEauthorblockN{Timmy Weerwag} \IEEEauthorblockN{Timmy Weerwag}
\IEEEauthorblockA{Radboud University,\\ \IEEEauthorblockA{XXX: Affiliation,\\
The Netherlands} The Netherlands}
\and \and
\IEEEauthorblockN{Freek Wiedijk} \IEEEauthorblockN{Freek Wiedijk}
...@@ -66,22 +41,26 @@ The Netherlands} ...@@ -66,22 +41,26 @@ The Netherlands}
} }
\fi \fi
\maketitle \maketitle
\todo{Put in date and thanks, figure out how in IEEEtran with conference mode.}
%\thispagestyle{empty} %\thispagestyle{empty}
\input{0_Abstract.tex} \input{abstract.tex}
\input{1_Introduction.tex} \input{intro.tex}
\input{2_Implementation.tex} \input{preliminaries.tex}
\input{3_Maths.tex} \input{lowlevel.tex}
\input{4_NumberAndImplementation.tex} \input{highlevel.tex}
\input{5_UsingVST.tex} \input{conclusion.tex}
\vspace*{1cm} \vspace*{1cm}
{\footnotesize \bibliographystyle{acm} {\footnotesize \bibliographystyle{acm}
\bibliography{collection}} \bibliography{collection}}
% \begin{appendix} \begin{appendix}
% \end{appendix} \input{tweetnacl.tex}
\end{appendix}
\end{document} \end{document}
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment