Commit f14b2cb1 authored by Benoit Viguier's avatar Benoit Viguier
Browse files

more rewrite

parent a22a9b1f
......@@ -46,41 +46,30 @@ support Montgomery curves (and in particular Curve25519).
This extension may be of independent interest.
\subheading{Related work.}
\todo{Fix this subsection}
There are two methodologies to get formal guarantees a software meets its
specifications.
The first one is by synthesizing a formal specification and then generating machine
code by refinement.
% in order to get a software correct by construction.
This approach is being used in e.g. the B-method~\cite{Abrial:1996:BAP:236705},
F*~\cite{DBLP:journals/corr/BhargavanDFHPRR17}, or with Coq~\cite{CpdtJFR}.
However this first method cannot be applied to an existing piece of software.
Two methodologies exist to get formal guarantees a software meets its specifications.
This can be done either by synthesizing a formal specification and then generating
machine code by refinement, or by writing a specification and verifying that the
implementation satisfies it.
The second approach consists of writing the specifications and then verifying
the correctness of the implementation.
Because we verify the TweetNaCl cryptographic library, we use this second method.
\todo{Separate verification of existing code from generating proof-carrying code.}
Similar approaches have been used to prove the correctness of OpenSSL
HMAC~\cite{Beringer2015VerifiedCA} and . Compared to
% 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 an 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 does 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, 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 mathematical definition of the group theory behind elliptic curves.
Using the synthesis approach, Zinzindohou{\'{e}} et al. wrote an verified extensible
library of elliptic curves~\cite{Zinzindohoue2016AVE}. This served as ground work for the
cryptographic library HACL*~\cite{zinzindohoue2017hacl} used in the NSS suite from Mozilla.
Coq does not only allows verification but also synthesis.
Using correct-by-construction finite field arithmetic~\cite{Philipoom2018CorrectbyconstructionFF}
one can synthesize~\cite{Erbsen2016SystematicSO} certified elliptic curve
implementations~\cite{Erbsen2017CraftingCE}. These implementation are now being used in BoringSSL~\cite{fiat-crypto}.
Curve25519 implementations has already been under the 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.
Synthesis approaches forces the user to depend on generated code which may not
be optimal (speed, compactness...), they require to tweak the compiler in order
to achieve the desired properties. On the other hand a carefully handcrafted
......@@ -88,14 +77,20 @@ optimized code will force the verifier to consider all the possible special case
and write a complex low level specification in order to prove the correctness of
the algorithm.
It has to be noted that Curve25519 implementations has already been under the 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.
\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. They are available at XXXXXXX
with instructions of how to compile and verify our proof.
A description of the content of the archive is provided in
Appendix~\ref{appendix:proof-folders}.
\subheading{Organization of this paper.}
Section~\ref{preliminaries} give the necessary background on Curve25519
implementation and a rough understand of how formal verification works.
implementation and a rough understanding of how formal verification works.
Section~\ref{C-Coq} provides the specification of X25519 in addition to proofs
techniques used to show the correctness.
Section~\ref{sec3-maths} describes our extension of the formal library by Bartzia
......
......@@ -69,24 +69,22 @@ conditional swap between $Q$ and $R$ in the TweetNaCl implementation.
\subsection{The X25519 key exchange}
\label{preliminaries:A}
\todo{Rephrase, use byte arrays, define clamping, state where things live.}
Inputs are two 32-bytes arrays, one is $n$ the other one represent
the $x$-coordinate of $P$.
To ensure security and avoid low order subgroups, values of $n$ are forced
into the shape of $2^{254} + 8\{0,1,\ldots,2^{251-1}\}$.
This is done by setting bit 255 to \texttt{0}; bit 254 to \texttt{1} and the lower
3 bits to \texttt{0}, making it a multiple of 8.
For any value $x \in \F{p}$, for the elliptic curve $E$ over $\F{p^2}$
defined by $y^2 = x^3 + 486662 x^2 + x$, there exist a point $P$ over $E(\F{p^2})$
such that $x$ is the $x$-coordinate of $P$.
Remark that $x$ is also the $x$-coordinate of $-P$.
Given a natural number $n$ and $x$, X25519 returns the $x$-coordinate of the
scalar multiplication of $P$ by $n$, thus $n \cdot P$. Note that the result is the
same with $n \cdot (-P) = -(n \cdot P)$.
Given $n \in \N$ and $x \in \F{\p}$, such that $x$ is the $x$-coordinate of
a point $P$ of $E(\F{\p})$, X25519 returns the $x$-coordinate of the
scalar multiplication of $P$ by $n$, thus $n \cdot P$.
% Note that the result is the same with $n \cdot (-P) = -(n \cdot P)$.
X25519 makes use of the little endian bijection for its arguements of 32-bytes:
\texttt{n} the secret key and \texttt{p} the public key.
Curve25519 has a cofactor of 8. In order to avoid attacks where an attacker
could discover some bits of the private key, values of $n$ are forced into the
shape of $2^{254} + 8\{0,1,\ldots,2^{251-1}\}$. This is done by setting bit 255
to \texttt{0}; bit 254 to \texttt{1} and the lower 3 bits to \texttt{0},
making it effectively a multiple of 8. This operation is known as the clamping.
RFC~7748~\cite{rfc7748} formalized the X25519 Diffie–Hellman key-exchange algorithm.
Given the base point $B$ where $B.x=9$, each party generate a secret random number
......@@ -186,8 +184,8 @@ sv car25519(gf o)
}
}
\end{lstlisting}
% In order to simplify the verification of this function,
% we extract the last step of the loop $i = 15$.
In order to simplify the verification of this function,
we extract the last step of the loop $i = 15$.
% \begin{lstlisting}[language=Ctweetnacl]
% sv car25519(gf o)
% {
......@@ -271,7 +269,8 @@ the \TNaCle{crypto_scalarmult} API function of TweetNaCl.
In order to compute the scalar multiplication,
X25519 uses the Montgomery ladder~\cite{Mon85}.
\todo{explain, projective coordinates, etc}
$x$-coordinates are represented as fractions, the computation of the actual
value is differed to the end of the ladder with \TNaCle{inv25519}.
First extract and clamp the value of $n$. Then unpack the value of $p$.
As per RFC~7748~\cite{rfc7748}, set its most significant bit to 0.
......
\subsection{Organization of the proof files}
\label{appendix:proof-folders}
\subheading{Requirements}
Our proofs requires the use of \emph{Coq.8.8.2} for the proofs and
......
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