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

One more pass through intro

parent 75c46b28
......@@ -12,16 +12,17 @@ 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~\cite{rfc7748}.
This protocol is being used by a wide variety of applications~\cite{things-that-use-curve25519}
One core component of TweetNaCl (and NaCl) is the key-exchange protocol X25519 presented
by Bernstein in~\cite{rfc7748}.
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 a an \xcoord only
The X25519 key-exchange protocol is a 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 scheme to X25519 and to use the name
X25519 for the protocol and Curve25519 for the underlying elliptic curve~\cite{Ber14}.
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}
......@@ -50,39 +51,48 @@ This extension may be of independent interest.
\subheading{Related work.}
Two methodologies exist to get formal guarantees that software meets its specification.
This can be done either by writing a formal specification and then synthesis
machine code by refinement, or by formalizing a specification and verifying that the
The first is to write a formal specification and then synthesize
machine code by refinement; the second is to formalize
a specification and then verify that some
implementation satisfies it.
% One of the earliest example of this first approach is the
% B-method~\cite{Abrial:1996:BAP:236705} in 1986.
Using the synthesis approach, Zinzindohou{\'{e}} et al. wrote a verified extensible
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}.
Erbsenm; Philipoom; Gross; and Chlipala et al. make use of it to have
correct-by-construction finite field arithmetic~\cite{Philipoom2018CorrectbyconstructionFF}.
In such way, they synthesized~\cite{Erbsen2016SystematicSO} certified elliptic curve
implementations~\cite{Erbsen2017CraftingCE}. These are now being used in
BoringSSL~\cite{fiat-crypto}.
The verification approach has been used to prove the correctness of OpenSSL
HMAC~\cite{Beringer2015VerifiedCA} and SHA-256~\cite{2015-Appel}. Compared to
that work our approach makes a complete link between the C implementation and
the formal mathematical definition of the group theory behind elliptic curves.
Synthesis approaches force the user to depend on generated code which may not
be optimal (speed, compactness) and they require compiler tweaks in order
to achieve the desired properties. On the other hand, carefully handcrafted
optimized code forces the verifier to consider all the possible special cases
and write a low level specification of the details of the code in order to prove
the correctness of the algorithm.
It has to be noted that Curve25519 implementations have already been under scrutiny~\cite{Chen2014VerifyingCS}.
However in this paper we provide a proofs of correctness and soundness of a C program up to
the theory of elliptic curves.
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}.
The verification approach has been used to prove the correctness of OpenSSL's
implementations of HMAC~\cite{Beringer2015VerifiedCA} and SHA-256~\cite{2015-Appel}.
In terms of languages and tooling, this work is closest to what we present here,
but our work considers an asymmetric primitive and provides computer-verified
proofs up to the mathematical definition of the group theory behind elliptic curves.
When considering the target of the verification effort, the closest work
to this paper is presented in~\cite{Chen2014VerifyingCS}, which presents
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 together with SAT solvers;
also, it does not cover the full X25519 functionality and does
not make the link to the mathematical definition from~\cite{Ber06}.
%Synthesis approaches force the user to depend on generated code which may not
%be optimal (speed, compactness) and they require compiler tweaks in order
%to achieve the desired properties. On the other hand, carefully handcrafted
%optimized code forces the verifier to consider all the possible special cases
%and write a low-level specification of the details of the code in order to prove
%the correctness of the algorithm.
%It has to be noted that Curve25519 implementations have already been under scrutiny
%However in this paper we provide a proofs of correctness and soundness of a C program up to
%the theory of elliptic curves.
\subheading{Reproducing the proofs.}
To maximize reusability of our results we placed the code of our formal proof
......@@ -91,22 +101,22 @@ presented in this paper into the public domain.
They are available at XXXXXXX
with instructions of how to compile and verify our proof.
\else
They are available in the associated materials with instructions of how
to compile and verify our proof.
They are available in the associated materials with this submission
and include instructions of how to compile and verify our proof.
\fi
A description of the content of the archive is provided in
Appendix~\ref{appendix:proof-folders}.
\subheading{Organization of this paper.}
\sref{sec:preliminaries} give the necessary background on Curve25519 and X25519
\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 formalization of RFC~7748~\cite{rfc7748}'s X25519.
\sref{sec:C-Coq} provides the specifications of TweetNaCl's X25519 and some of the
proofs techniques used to show the correctness with respect to RFC~7748~\cite{rfc7748}.
\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}.
And lastly in \sref{sec:Conclusion} we discuss the trusted code base of this proof.
Finally in \sref{sec:Conclusion} we discuss the trusted code base of our proofs.
\fref{tikz:ProofOverview} shows a graph of dependencies of the proofs.
\begin{figure}[h]
......
......@@ -236,7 +236,6 @@
}
@misc{Erbsen2016SystematicSO,
author = {Andres Erbsen and
Jason Gross and
Adam Chlipala},
......@@ -330,7 +329,6 @@
title = {Correct-by-construction finite field arithmetic in Coq},
school = {Massachusetts Institute of Technology},
year = {2018},
note = {\url{http://adam.chlipala.net/theses/jadep_meng.pdf}},
}
......
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