Commit 5c5ac275 authored by Peter Schwabe's avatar Peter Schwabe
Browse files

Edits in intro and preliminaries towards the camera-ready version

parent fc994792
......@@ -7,7 +7,7 @@
Bernstein's 2006 paper, as standardized in RFC~7748,
as well as the absence of undefined behavior
like arithmetic overflows
and array out of bounds errors.
and array out-of-bounds errors.
We also formally prove, based on the work of Bartzia and Strub,
that X25519 is mathematically correct, i.e.,
that it correctly computes scalar multiplication on
......
......@@ -15,7 +15,7 @@ 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
such as SSH, the 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
......@@ -25,7 +25,7 @@ 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.}
\subheading{Contributions 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}.
......@@ -113,7 +113,7 @@ In~\cite{Zinzindohoue2016AVE}, Zinzindohou{\'{e}}, Bartzia, and Bhargavan
describe a verified extensible library of elliptic curves~ 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. The approach they use is a combination
of proving and synthesising: A fairly low-level implementation written in
of proving and synthesizing: A fairly low-level implementation written in
Low$^*$ is proven to be equivalent to a high-level specification in F$^*$.
The Low$^*$ code is then compiled to C using an unverified and thus trusted
compiler called Kremlin.
......@@ -148,7 +148,7 @@ structure of finite field and elliptic curves the actual proofs are quite differ
\subheading{Reproducing the proofs.}
To maximize reusability of our results we place the code of our formal proof
presented in this paper into the public domain.
It is available at \url{http://doi.org/10.5281/zenodo.4439686}
It is available at \url{https://doi.org/10.5281/zenodo.4439686}
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}.
......@@ -157,10 +157,10 @@ Appendix~\ref{appendix:proof-folders}.
\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
\sref{sec:C-Coq} details 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
and Strub and the proof of correctness of the 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
......@@ -170,12 +170,12 @@ effort required to extend our work to other elliptic-curve software.
C source files are represented by {\color{doc@lstfunctions}.C} while
{\color{doc@lstfunctions}.V} corresponds to Coq files.
In a nutshell, we formalize X25519 into a Coq function \texttt{RFC},
and we write a specification in Separation logic with VST.
The first step of CompCert compilation (clightgen) is used to translates
and we write a specification in separation logic with VST.
The first step of CompCert compilation (clightgen) is used to translate
the C source code into a DSL in Coq (CLight). By using VST,
we step through the translated instructions and verify that the program satisfies the specifications.
Additionally we formally define the scalar multiplication over elliptic curves and show that,
under the same preconditions as used in the specification, \texttt{RFC} computes the desired results
under the same preconditions as used in the specification, \texttt{RFC} computes the desired results.
\begin{figure}[h]
\centering
......
......@@ -32,7 +32,7 @@ are isomorphic via $(x,y) \mapsto (x, \sqrt{b/b'} \cdot y)$.
a curve that is isomorphic over $\F{p^2}$~\cite{cryptoeprint:2017:212}.
\end{dfn}
Points in $M_{a,b}(\K)$ can be equipped with a structure of an commutative group
Points in $M_{a,b}(\K)$ can be equipped with a structure of a commutative group
with the addition operation $+$ and with neutral element the point at infinity $\Oinf$.
For a point $P \in M_{a,b}(\K)$ and a positive integer $n$ we obtain the scalar product
$$n\cdot P = \underbrace{P + \cdots + P}_{n\text{ times}}.$$
......@@ -51,7 +51,7 @@ We define the operation:
& ((X_{2 \cdot P}:Z_{2 \cdot P}), (X_{P + Q}:Z_{P + Q}))
\end{align*}
A pseudocode description of the Montgomery ladder
A pseudocode description of the Montgomery ladder using this \texttt{xDBL\&ADD} routine
is given in Algorithm~\ref{alg:montgomery-ladder}.
The main loop iterates over the bits of the scalar $n$.
The $k^{\text{th}}$ iteration conditionally swaps
......@@ -62,9 +62,6 @@ function while keeping the same body of the loop. \label{cswap}
Given a pair $(P_0, P_1)$ and a bit $b$, \texttt{CSWAP} returns the pair
$(P_b, P_{1-b})$.
By using the differential addition and doubling operations we define the Montgomery ladder
computing a \xcoord-only scalar multiplication (see \aref{alg:montgomery-ladder}).
% \setlength{\textfloatsep}{1em}
\begin{algorithm}
\caption{Montgomery ladder for scalar mult.}
......@@ -98,13 +95,13 @@ The core of the X25519 key-exchange protocol is a scalar\hyp{}multiplication
function, which we will also refer to as X25519.
This function receives as input two arrays of $32$ bytes each.
One of them is interpreted as the little-endian encoding of a
non-negative 256-bit integer $n$ (see \ref{sec:Coq-RFC}).
non-negative 256-bit integer $n$ (see Section~\ref{sec:Coq-RFC}).
The other is interpreted as the little-endian encoding of
the \xcoord $x_P \in \F{p}$ of a point in $E(\F{p^2})$,
using the standard mapping of integers modulo $p$ to elements in $\F{p}$.
The X25519 function first computes a scalar $n'$ from $n$ by setting
bits at position 0, 1, 2 and 255 to \texttt{0}; and at position 254
bits at positions 0, 1, 2 and 255 to \texttt{0}; and at position 254
to \texttt{1}.
This operation is often called ``clamping'' of the scalar $n$.
Note that $n' \in 2^{254} + 8\{0,1,\ldots,2^{251}-1\}$.
......@@ -171,7 +168,7 @@ and squaring (\TNaCle{S}). After a multiplication, limbs of the result
\texttt{o} are too large to be used again as input. Two calls to
\TNaCle{car25519} at the end of \TNaCle{M} takes care of the carry propagation.
Inverses in $\Ffield$ are computed with \TNaCle{inv25519}.
Inverses in $\Ffield$ are computed in \TNaCle{inv25519}.
This function uses exponentiation by $p - 2 = 2^{255}-21$,
computed with the square-and-multiply algorithm.
......@@ -188,8 +185,8 @@ This function is considerably more complex as it needs to convert
to a \emph{unique} representation, i.e., also fully reduce modulo
$p$ and remove the redundancy of the radix-$2^{16}$ representation.
The C definitions of those functions are available in
Appendix \ref{verified-C-and-diff}.
The C definitions of all these functions are available in
Appendix~\ref{verified-C-and-diff}.
\subheading{The Montgomery ladder.}
With these low-level arithmetic and helper functions defined,
......@@ -247,8 +244,9 @@ int crypto_scalarmult(u8 *q,
}
\end{lstlisting}
Note that lines 10 \& 11 represent the ``clamping'' operation.
Note that lines 10 \& 11 represent the ``clamping'' operation;
the sequence of arithmetic operations in lines 22 through 39 implement the
\texttt{xDBL\&ADD} routine.
\subsection{Coq, separation logic, and VST}
\label{subsec:Coq-VST}
......@@ -280,8 +278,10 @@ For example, here is the rule for sequential composition:
\BinaryInfC{$\{P\}C_1;C_2\{R\}$}
\end{prooftree}
Separation logic is an extension of Hoare logic which allows reasoning about
pointers and memory manipulation. This logic enforces strict conditions on the
memory shared such as being disjoint.
pointers and memory manipulation.
%This logic enforces strict conditions on the memory shared such as being disjoint.
%Separation logic requires memory regions of different function arguments to be disjoint.
Reasoning in separation logic assumes that certain memory regions are non-overlapping
We discuss this limitation further in \sref{subsec:with-VST}.
The Verified Software Toolchain (VST)~\cite{cao2018vst-floyd} is a framework
......@@ -289,8 +289,8 @@ which uses separation logic (proven correct with respect to CompCert semantics)
to prove the functional correctness of C programs.
The first step consists of translating the source code into Clight,
an intermediate representation used by CompCert.
For such purpose one uses the parser of CompCert called \texttt{clightgen}.
For this purpose we use the parser of CompCert called \texttt{clightgen}.
In a second step one defines the Hoare triple representing the specification of
the piece of software one wants to prove. Then using VST, one uses a strongest
postcondition approach to prove the correctness of the triple.
the piece of software one wants to prove. With the help of VST
we then use the strongest-postcondition approach to prove the correctness of the triple.
This can be seen as a forward symbolic execution of the program.
......@@ -23,10 +23,8 @@
\ifpublic
\author{
\IEEEauthorblockN{Peter Schwabe}
\IEEEauthorblockA{Max Planck Institute for Security and Privacy,\\
Germany \&\\
Radboud University\\
The Netherlands}
\IEEEauthorblockA{MPI-SP, Germany \&\\
Radboud University, The Netherlands}
\and
\IEEEauthorblockN{Beno\^it Viguier}
\IEEEauthorblockA{Radboud University,\\
......
Markdown is supported
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