1-intro.tex

\section{Introduction}
\label{sec:intro}

The Networking and Cryptography library (NaCl)~\cite{BLS12}
is an easy-to-use, high-security, high-speed cryptography library.
It uses specialized code for different platforms, which makes it rather complex and hard to audit.
TweetNaCl~\cite{BGJ+15} is a compact re-implementation in C
of the core functionalities of NaCl and is claimed to be
\emph{``the first cryptographic library that allows correct functionality
to be verified by auditors with reasonable effort''}~\cite{BGJ+15}.
The original paper presenting TweetNaCl describes some effort to support
this claim, for example, formal verification of memory safety, but does not actually
prove correctness of any of the primitives implemented by the library.

One core component of TweetNaCl (and NaCl) is the key-exchange protocol X25519 presented
by Bernstein in~\cite{Ber06}.
This protocol is standardized in RFC~7748 and used by a wide variety of applications~\cite{things-that-use-curve25519}
such as SSH, Signal Protocol, Tor, Zcash, and TLS to establish a shared secret over
an insecure channel.
The X25519 key-exchange protocol is an \xcoord-only
elliptic-curve Diffie--Hellman key exchange using the Montgomery
curve $E: y^2 = x^3 + 486662 x^2 + x$ over the field $\F{\p}$.
Note that originally, the name ``Curve25519'' referred to the key-exchange protocol,
but Bernstein suggested to rename the protocol to X25519 and to use the name
Curve25519 for the underlying elliptic curve~\cite{Ber14}.
We use this updated terminology in this paper.

\subheading{Contribution of this paper.}
In short, in this paper we provide a computer-verified proof that the
X25519 implementation in TweetNaCl matches the mathematical definition
of the function given in~\cite[Sec.~2]{Ber06}.
This proof is done in three steps:

We first formalize RFC~7748~\cite{rfc7748} in Coq~\cite{coq-faq}.

In the second step we prove equivalence of the C implementation of X25519
to our RFC formalization.
This part of the proof uses the Verifiable Software Toolchain (VST)~\cite{2012-Appel}
to establish a link between C and Coq.
VST uses separation logic~\cite{1969-Hoare,Reynolds02separationlogic}
to show that the semantics of the program satisfy a functional specification in Coq.
To the best of our knowledge, this is the first time that VST 
is used in the formal proof of correctness of an implementation
of an asymmetric cryptographic primitive.

In the last step we prove that the Coq formalization of the RFC matches
the mathematical definition of X25519 as given in~\cite[Sec.~2]{Ber06}.
We do this by extending the Coq library
for elliptic curves~\cite{BartziaS14} by Bartzia and Strub to
support Montgomery curves, and in particular Curve25519.

To our knowledge, this verification effort is the first to not just
connect a low-level implementation to a higher-level implementation (or ``specification''),
but to prove correctness all the way up
to the mathematical definition in terms of scalar multiplication on an elliptic curve.
As a consequence, the result of this paper can readily be used in mechanized proofs of
higher-level protocols that work with the mathematical definition of X25519.
Also, connecting our formalization of the RFC to the mathematical definition
significantly increases trust into the correctness of the formalization and
reduces the effort of manual auditing of that formalization.

\subheading{Related work.}
The field of computer-aided cryptography, i.e., using computer-verified proofs
to strengthen our trust into cryptographic constructions and cryptographic software,
has seen massive progress in the recent past. This progress, the state of the art,
and future challenges have recently been compiled in a SoK paper by Barbosa,
Barthe, Bhargavan, Blanchet, Cremers, Liao, and Parno~\cite{BBB+19}.
This SoK paper, in Section III.C, also gives an overview of verification efforts of 
X25519 software. What all the previous approaches have in common is that they
prove correctness by verifying that some low-level implementation matches a
higher-level specification. This specification is kept in terms of a sequence
of finite-field operations, typically close to the pseudocode in RFC 7748.

There are two general approaches to establish this link 
between low-level code and higher-level specification:
Synthesize low-level code from the specification
or write the low-level code by hand and prove that it
matches the specification.

\todo{Say something about all X25519 implementations from the SoK paper.}


%The synthesis approach was used by Zinzindohou{\'{e}}, Bartzia, and Bhargavan to build a verified extensible
%library of elliptic curves~\cite{Zinzindohoue2016AVE} in F*~\cite{DBLP:journals/corr/BhargavanDFHPRR17}.
%This served as ground work for the cryptographic library HACL*~\cite{zinzindohoue2017hacl}
%used in the NSS suite from Mozilla.
%
%Coq not only allows verification but also synthesis~\cite{CpdtJFR}.
%Erbsen, Philipoom, Gross, and Chlipala make use of it to have
%correct-by-construction finite field arithmetic, which is used
%to synthesize certified elliptic-curve crypto software~\cite{Philipoom2018CorrectbyconstructionFF,Erbsen2017CraftingCE,Erbsen2016SystematicSO}.
%This software suite is now being used in BoringSSL~\cite{fiat-crypto}.


All of these X25519 verification efforts listed in~\cite{BBB+19} use a clean-slate
approach to obtain code and proofs. 
Our effort targets existing software and we are aware of only one earlier 
work in the context of X25519 following a similar approach. 
In~\cite{Chen2014VerifyingCS}, Chen, Hsu, Lin, Schwabe, Tsai, Wang, Yang, and Yang present
a mechanized proof of two assembly-level implementations of the core function of X25519.
The proof in~\cite{Chen2014VerifyingCS} takes a different approach from ours.
It uses heavy annotation of code in order to ``guide'' a SAT solver;
also, it does not cover the full X25519 functionality and does
not make the link to the mathematical definition from~\cite{Ber06}.

Finally, in terms of languages and tooling the work closest to what we present here
is the proof of correctness of OpenSSL's
implementations of HMAC~\cite{Beringer2015VerifiedCA}, 
and mbedTLS' implementations of 
HMAC-DRBG~\cite{2017-Ye} and SHA-256~\cite{2015-Appel}.

\subheading{Reproducing the proofs.}
To maximize reusability of our results we placed the code of our formal proof
presented in this paper into the public domain.
It is available at \todo{FIX ME: https://cdn-09.anonfile.com/6fp8ta70n9/014c4f8c-1569921449/coq-verif-tweetnacl.tar.gz}
with instructions of how to compile and verify our proof.
A description of the content of the code archive is provided in
Appendix~\ref{appendix:proof-folders}.

\subheading{Organization of this paper.}
\sref{sec:preliminaries} gives the necessary background on Curve25519 and X25519
implementations and a brief explanation of how formal verification works.
\sref{sec:Coq-RFC} provides our Coq formalization of X25519 as specified in RFC~7748~\cite{rfc7748}.
\sref{sec:C-Coq} provides the specifications of X25519 in TweetNaCl and some of the
proof techniques used to show the correctness with respect to RFC~7748~\cite{rfc7748}.
\sref{sec:maths} describes our extension of the formal library by Bartzia
and Strub and the correctness of X25519 implementation with respect to Bernstein's
specifications~\cite{Ber14}.
Finally in \sref{sec:Conclusion} we discuss the trusted code base of our proofs
and conclude with some lessons learned about TweetNaCl and with sketching the 
effort required to extend our work to other elliptic-curve software.

\fref{tikz:ProofOverview} shows a graph of dependencies of the proofs.
C source files are represented by {\color{doc@lstfunctions}.C} while
{\color{doc@lstfunctions}.V} corresponds to Coq files.

\begin{figure}[h]
  \centering
  \include{tikz/proof}
  \caption{Structure of the proof.}
  \label{tikz:ProofOverview}
\end{figure}

% 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