1_Introduction.tex

\section{Introduction}

Implementing cryptographic primitives without any bugs is hard.
While tests provides a code coverage and are used in the limits,
they still don't cover 100\% of the possible input values.

In order to get formal guaranties a software meets its specifications,
two methodologies exist. The first one is by synthesizing a formal specification and
generating machine code by refinment. This approach is being used in the
B-method\cite{Abrial:1996:BAP:236705}, F* \cite{DBLP:journals/corr/BhargavanDFHPRR17} with Kremlin, or in Coq \cite{CpdtJFR}.
This gives you a software correct by construction. However it cannot be applied
to an existing piece of software. In such case we need to write the specifications
and then verify the correctness of the implementation.

Verifying an existing cryptographic library, we use the second approach.
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.
Similar approaches have been used to prove the correctness of OpenSSL HMAC
\cite{Beringer2015VerifiedCA} and SHA-256 \cite{Appel2015VerificationOA}.

TweetNaCl\cite{BGJ+15} is a compact reimplementation of the
NaCl\cite{BLS12} library. It does not aim for high speed
application and has been optimized for source code compactness.
It maintains some degree of readability in order to be easily auditable.

This library makes use of Curve25519\cite{Ber06}, a function over a \F{p}-restricted
$x$-coordinate computing a scalar multiplication on $E(\F{p^2})$, where $p$ is
the prime number \p and $E$ is the elliptic curve $y^2 = x^3 + 486662 x^2 + x$.

Coq is a formal system that allows to machine-check our proofs.
A famous example of its use is the proof of the Four Color Theorem.
The Compcert\cite{Leroy-backend} compiler and the Verifiable Software Toolchain
(VST)\cite{2012-Appel} are build on top of it.

Our approach is as follow, we use the \textit{clightgen} tool from Compcert to
generate the \textit{semantic version} (Clight\cite{Blazy-Leroy-Clight-09}) of
the TweetNaCl C code.
Using the Separation logic\cite{1969-Hoare,Reynolds02separationlogic}
with with the Verifiable Software Toolchain we show that the semantics of the
program satisfies a functionnal specification in Coq.
We extend the work of Bartzia and Strub \cite{DBLP:conf/itp/BartziaS14} to
support Montgomery curves.
With this formalization, we prove the correctness of a generic Montgomery ladder
and show that our specification can be seen as an instance of it.

% Five years ago:
% \url{https://www.imperialviolet.org/2014/09/11/moveprovers.html}
% \url{https://www.imperialviolet.org/2014/09/07/provers.html}

% \section{Related Works}
%
% \begin{itemize}
%   \item HACL*
%   \item Proving SHA-256 and HMAC
%   \item \url{http://www.iis.sinica.edu.tw/~bywang/papers/ccs17.pdf}
%   \item \url{http://www.iis.sinica.edu.tw/~bywang/papers/ccs14.pdf}
%   \item \url{https://cryptojedi.org/crypto/#gfverif}
%   \item \url{https://cryptojedi.org/crypto/#verify25519}
%   \item Fiat Crypto : synthesis
% \end{itemize}
%
% Add comparison with Fiat-crypto