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

typos, corrections, conclusions

parent 2d20d0fd
......@@ -62,6 +62,7 @@
@book{Abrial:1996:BAP:236705,
author = {Jean-Raymond Abrial},
editor = {},
title = {The B-book: Assigning Programs to Meanings},
publisher = {Cambridge University Press},
year = {1996},
......@@ -264,6 +265,15 @@
note = {\url{https://www.cs.cmu.edu/~crary/819-f09/Howard80.pdf}},
}
@manual{ISO:C17,
title = {ISO C Standard 2017},
author = {ISO},
month = {Jun},
year = {2018},
note = {\url{https://www.iso.org/standard/74528.html}},
}
@manual{ISO:C99,
title = {ISO C Standard 1999},
......
......@@ -4,12 +4,10 @@
Any formal system relies on a trusted base. In this section we describe our
chain of trust.
\subsection{Trusted Code Base of the proof}
Our proof relies on a trusted base, i.e. a foundation of specifications
and implementations that must stay correct with respect to their specifications.
One should not be able to prove a false statement in that system e.g. by proving
an inconsistency.
\subheading{Trusted Code Base of the proof.}
Our proof relies on a trusted base, i.e. a foundation of definitions that must be
correct. One should not be able to prove a false statement in that system, \eg, by
proving an inconsistency.
In our case we rely on:
\begin{itemize}
......@@ -25,15 +23,13 @@ Lemma f_ext: forall (A B:Type),
\item \textbf{Verifiable Software Toolchain}. This framework developed at
Princeton allows a user to prove that a Clight code matches pure Coq
specification. However one must trust the framework properly captures and
map the Clight behavior to the basic pure Coq functions.
% At the beginning of the project we found inconsistency and reported them to the authors.
specification.
\item \textbf{CompCert}. The formally proven compiler. We trust that the Clight
model captures correctly the C99 standard.
model captures correctly the C17 standard.
Our proof also assumes that the TweetNaCl code will behave as expected if
compiled under CompCert. We do not provide guarantees for other C compilers
such as Clang or GCC.
compiled under CompCert.
% We do not provide guarantees for other C compilers such as Clang or GCC.
\item \textbf{\texttt{clightgen}}. The tool making the translation from \textbf{C} to
\textbf{Clight}. It is the first step of the compilation.
......@@ -45,8 +41,8 @@ aux2 = b[i];
o[i] = aux1 + aux2;
\end{lstlisting}
The trust of the proof relied on the trust of a correct translation from the
initial version of \textit{TweetNaCl} to \textit{TweetNaclVerificable}.
\texttt{clightgen} now comes with \texttt{-normalize} flag which
initial version of \emph{TweetNaCl} to \emph{TweetNaclVerifiableC}.
\texttt{clightgen} comes with \texttt{-normalize} flag which
factors out function calls and assignments from inside subexpressions.
The changes required for a C-code to make it Verifiable are now minimal.
......@@ -56,11 +52,11 @@ o[i] = aux1 + aux2;
done with this architecture \cite{2015-Appel,coq-faq}.
\end{itemize}
\subsection{Corrections in TweetNaCl}
\subheading{Corrections in TweetNaCl.}
As a result of this verification, we removed superfluous code.
Indeed the upper 64 indexes of the \TNaCle{i64 x[80]} intermediate variable of
\TNaCle{crypto_scalarmult} were adding unnecessary complexity to the code, we fixed it.
Indeed indexes 17 to 79 of the \TNaCle{i64 x[80]} intermediate variable of
\TNaCle{crypto_scalarmult} were adding unnecessary complexity to the code,
we removed them.
Peter Wu and Jason A. Donenfeld brought to our attention that the original
\TNaCle{car25519} function presented risk of Undefined Behavior if \texttt{c}
......@@ -69,7 +65,7 @@ is a negative number.
c=o[i]>>16;
o[i]-=c<<16; // c < 0 = UB !
\end{lstlisting}
By replacing statement by a logical \texttt{and} (and proving the correctness)
By replacing this statement by a logical \texttt{and} (and proving the correctness)
we solved this problem.
\begin{lstlisting}[language=Ctweetnacl]
o[i]&=0xffff;
......@@ -78,4 +74,10 @@ o[i]&=0xffff;
We believe that the type change of the loop index (\TNaCle{int} instead of \TNaCle{i64})
does not impact the trust of our proof.
\todo{I don't see what to say more here.}
\subheading{A complete proof.}
We provide a mechanized formal proof of the correctness of the X25519 implementation in TweetNaCl.
We first proved that TweetNaCl's implementation of X25519 matches RFC~7748 (\tref{thm:VST-RFC}).
In a second step we extended the COq library for elliptic cruves \cite{BartziaS14}
by Bartzia and Strub to support Montgomery curves. Using this extension we
proved that the X25519 implementation in TweetNaCl matches the mathematical
definitions as given in~\cite[Sec.~2]{Ber06} (\tref{thm:Elliptic-CSM}).
\todo{I don't think this belongs to the paper but more to the associated materials}
\subsection{Content of the proof files}
\label{appendix:proof-files}
......
......@@ -22,7 +22,7 @@ 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}.
We make use of this updated notation in this paper.
We make use of this updated terminology in this paper.
\subheading{Contribution of this paper}
We provide a mechanized formal proof of the correctness of the X25519
......@@ -46,7 +46,7 @@ support Montgomery curves (and in particular Curve25519).
This extension may be of independent interest.
\subheading{Related work.}
Two methodologies exist to get formal guarantees a software meets its specifications.
Two methodologies exist to get formal guarantees that software meets its specification.
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.
......@@ -67,15 +67,15 @@ 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
their work our approaches makes a complete link between the C implementation and
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 forces the user to depend on generated code which may not
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 will force the verifier to consider all the possible special cases
and write a complex low level specification in order to prove the correctness of
the algorithm.
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
......@@ -89,14 +89,14 @@ 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
implementation and a rough understanding of how formal verification works.
\sref{sec:C-Coq-RFC} provides the specification of X25519 and the in addition to proofs
\sref{sec:preliminaries} give the necessary background on Curve25519 and X25519
implementations and a brief explanation of how formal verification works.
\sref{sec:C-Coq-RFC} provides the specification of X25519 and in addition the proofs
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
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 trust in this proof.
And lastly in \sref{sec:Conclusion} we discuss the trusted code base of this proof.
% Five years ago:
......
\section{Proving equivalence of X25519 in C and Coq}
\label{sec:C-Coq-RFC}
In this section we prove the following theorems:
In this section we prove the following theorem:
% In this section we outline the structure of our proofs of the following theorem:
\begin{theorem}
\label{thm:VST}
The implementation of X25519 in TweetNaCl (\TNaCle{crypto_scalarmult}) matches our
functional specification in Coq.
\end{theorem}
\begin{theorem}
\label{thm:RFC}
Our functional specification in Coq matches the specifications of RFC~7748~\cite{rfc7748}.
\label{thm:VST-RFC}
The implementation of X25519 in TweetNaCl (\TNaCle{crypto_scalarmult}) matches
the specifications of RFC~7748~\cite{rfc7748}
\end{theorem}
We first describe the global structure of our proof (\ref{subsec:proof-structure}).
Then we introduce our specification, we specify the Hoare triple and prove it
correct with VST (\tref{thm:VST}).
Then we discuss techniques used to prove equivalence of operations between
different number representations,
proving the equivalence with the RFC (\tref{thm:RFC}).
We introduce our translation of RFC~7748 (\ref{subsec:spec-rfc}) and specify
the Hoare triple before proving its correctness with VST (\ref{subsec:with-VST}).
We provide an example of equivalence of operations over different number
representations (\ref{subsec:num-repr-rfc}). Then, we describe efficient techniques
used to in some of our more complex proofs (\ref{subsec:inversions-reflections}).
......@@ -29,16 +25,15 @@ proving the equivalence with the RFC (\tref{thm:RFC}).
In order to prove the correctness of X25519 in TweetNaCl code \TNaCle{crypto_scalarmult},
we use VST to prove that the code matches our functional Coq specification of \Coqe{Crypto_Scalarmult}
(sometimes abbreviated as \Coqe{CSM}). Then, we prove that our specification of the scalar
multiplication matches the mathematical definition of elliptic curves and Theorem 2.1 by
Bernstein~\cite{Ber06} (\tref{thm:Elliptic-CSM}).
\fref{tikz:ProofOverview} shows a graph of dependencies of the proofs considered.
The mathematical proof of our specification is presented
in \sref{sec:maths}.
(to save space we sometimes abbreviate this as \Coqe{CSM}). Then, we prove that
our specification of the scalar multiplication matches the mathematical definition
of elliptic curves and Theorem 2.1 by Bernstein~\cite{Ber06} (\tref{thm:Elliptic-CSM}).
\fref{tikz:ProofOverview} shows a graph of dependencies of the proofs.
The mathematical proof of X25519 is presented in \sref{sec:maths}.
\begin{figure}[h]
\centering
\include{tikz/proof}
\caption{Overview of the proof}
\caption{Structure of the proof}
\label{tikz:ProofOverview}
\end{figure}
......@@ -50,28 +45,29 @@ subsequently called: \TNaCle{unpack25519}; \TNaCle{A}; \TNaCle{Z}; \TNaCle{M};
We prove the implementation of X25519 is \textbf{sound}, \ie:
\begin{itemize}
\item absence of access out-of-bounds of arrays (memory safety).
\item absence of overflows/underflow on the arithmetic.
\item absence of overflows/underflow in the arithmetic.
\end{itemize}
We also prove that TweetNaCl's code is \textbf{correct}:
\begin{itemize}
\item X25519 is correctly implemented (we get what we expect) .
\item Operations on \texttt{gf} (\texttt{A}, \texttt{Z}, \texttt{M}, \texttt{S})
\item Operations on \TNaCle{gf} (\TNaCle{A}, \TNaCle{Z}, \TNaCle{M}, \TNaCle{S})
are equivalent to operations ($+,-,\times,x^2$) in \Zfield.
\item The Montgomery ladder computes a scalar multiplication between a natural
number and a point.
\item The Montgomery ladder computes the multiple of a point.
% \item The Montgomery ladder computes a scalar multiplication between a natural
% number and a point.
\end{itemize}
In order to prove the soundness and correctness of \TNaCle{crypto_scalarmult},
we first create a skeleton of the Montgomery ladder with abstract operations which
can be instantiated over lists, integers, field elements...
can be instantiated over \eg lists, integers, field elements.
A high level specification (over a generic field $\K$) allows us to prove the
correctness of the ladder with respect to the curves theory.
correctness of the ladder with respect to the theory of elliptic curves.
This high-level specification does not rely on the parameters of Curve25519.
By instantiating $\K$ with $\Zfield$, and the parameters of Curve25519 ($a = 486662, b = 1$),
we define a mid-level specification.
Additionally we also provide a low-level specification close to the \texttt{C} code
(over lists of $\Z$). We show this specification to be equivalent to the
\textit{semantic version} of C (Clight) with VST.
\emph{semantic version} of C (Clight) using the VST.
This low level specification gives us the soundness assurance.
By showing that operations over instances ($\K = \Zfield$, $\Z$, list of $\Z$) are
equivalent, we bridge the gap between the low level and the high level specification
......@@ -91,16 +87,17 @@ This guarantees us the correctness of the implementation.
\subsection{A Correct Specification}
\label{subsec:spec-rfc}
TweetNaCl implements X25519 with numbers represented as arrays.
RFC~7748 defines X25519 over field elements. In order to simplify our proofs,
we define operations used in the ladder over generic types
\coqe{T} and \coqe{T'}. Those types are later instantiated as natural numbers,
integers, field elements, list of integers...
The generic definition of the ladder (\coqe{montgomery_rec}) and its match with
integers, field elements, list of integers.
The generic definition of the ladder (\coqe{montgomery_rec}) and its parallel with
the definition of RFC~7748 are provided in Appendix~\ref{subsubsec:coq-ladder}.
It has to be noted that the RFC uses an additional variable to optimize the number
of \texttt{CSWAP}:
of \texttt{CSWAP} calls:
\emph{``Note that these formulas are slightly different from Montgomery's
original paper. Implementations are free to use any correct formulas.''}~\cite{rfc7748}.
We later prove our ladder correct in that respect (\sref{sec:maths}).
......@@ -119,10 +116,15 @@ interpreted as the formalization of X25519 in RFC~7748.
In appendix~\ref{subsubsec:CryptoScalarmult}, we show the the formalization of
\TNaCle{crypto_scalarmult} over lists of integers. We define it as
\Coqe{Crypto_Scalarmult} or \Coqe{CSM}. For the sake of space and simplicity we
do not display the definitions of each underlying functions.
The location of the definitions are listed in Appendix~\ref{appendix:proof-files}.
do not display the definitions of each underlying function.
% The location of the definitions are listed in Appendix~\ref{appendix:proof-files}.
\subsection{With the Verifiable Software Toolchain}
\subsection{Applying the Verifiable Software Toolchain}
\label{subsec:with-VST}
We now turn our focus to the specification of the Hoare triple with our
......@@ -183,11 +185,11 @@ In this specification we state as preconditions:
In the memory share \texttt{sh}, the address \VSTe{v_p} points
to a list of integer values \VSTe{mVI p}.
\item[] \VSTe{PROP}: \VSTe{Forall (fun x => 0 <= x < 2^8) p}\\
In order to consider all the possible inputs, we assumed each
In order to consider all the possible inputs, we assume each
elements of the list \texttt{p} to be bounded by $0$ included and $2^8$
excluded.
\item[] \VSTe{PROP}: \VSTe{Zlength p = 32}\\
We also assumed that the length of the list \texttt{p} is 32. This defines the
We also assume that the length of the list \texttt{p} is 32. This defines the
complete representation of \TNaCle{u8[32]}.
\end{itemize}
......@@ -200,7 +202,7 @@ As Post-condition we have:
\item[] \VSTe{SEP}: \VSTe{sh [{ v_q $\!\!\}\!\!]\!\!\!$ <<(uch32)-- mVI (CSM n p)}\\
In the memory share \texttt{sh}, the address \VSTe{v_q} points
to a list of integer values \VSTe{mVI (CSM n p)} where \VSTe{CSM n p} is the
result of the \VSTe{crypto_scalarmult} over \VSTe{n} and \VSTe{p}.
result of the \VSTe{crypto_scalarmult} of \VSTe{n} and \VSTe{p}.
\item[] \VSTe{PROP}: \VSTe{Forall (fun x => 0 <= x < 2^8) (CSM n p)}\\
\VSTe{PROP}: \VSTe{Zlength (CSM n p) = 32}\\
We show that the computation for \VSTe{CSM} fits in \TNaCle{u8[32]}.
......@@ -209,7 +211,16 @@ As Post-condition we have:
This specification shows that \TNaCle{crypto_scalarmult} in C computes the same
result as \VSTe{CSM} in Coq provided that inputs are within their respective
bounds: arrays of 32 bytes.
The location of the proof of this Hoare triple can be found in Appendix~\ref{appendix:proof-files}.
\begin{theorem}
\label{thm:crypto-vst}
\TNaCle{crypto_scalarmult} in TweetNaCl has the same behavior as \coqe{Crypto_Scalarmult} in Coq.
\end{theorem}
% % this does not exists anymore
% The location of the proof of this Hoare triple can be found in Appendix~\ref{appendix:proof-files}.
% We now bring the attention of the reader to details of verifications using the VST.
......@@ -235,7 +246,7 @@ In the VST, a simple specification of \texttt{M(o,a,b)} will assume three
distinct memory share. When called with three memory shares (\texttt{o, a, b}),
the three of them will be consumed. However assuming this naive specification
when \texttt{M(o,a,a)} is called (squaring), the first two memory shares (\texttt{o, a})
are consumed and VST will expect a third memory share (\texttt{a}) which does not \textit{exist} anymore.
are consumed and VST will expect a third memory share (\texttt{a}) which does not \emph{exist} anymore.
Examples of such cases are illustrated in \fref{tikz:MemSame}.
\begin{figure}[h]
\centering
......@@ -260,7 +271,7 @@ This solution does not cover all cases (e.g. all arguments are aliased) but it
is enough for our needs.
\subheading{Verifying \texttt{for} loops.}
Final state of \texttt{for} loops are usually computed by simple recursive functions.
Final states of \texttt{for} loops are usually computed by simple recursive functions.
However we must define invariants which are true for each iteration step.
Assume we want to prove a decreasing loop where indexes go from 3 to 0.
......@@ -299,14 +310,16 @@ in C provide the same computations as in \coqe{CSM}.
\subsection{Number Representation and C Implementation}
\label{subsec:num-repr-rfc}
As described in \sref{subsec:Number-TweetNaCl}, numbers in \TNaCle{gf} are represented
in base $2^{16}$ and we use a direct mapping to represent that array as a list
integers in Coq. However in order to show the correctness of the basic operations,
we need to convert this number to a full integer.
\begin{dfn}
Let \Coqe{ZofList} : $\Z \rightarrow \texttt{list} \Z \rightarrow \Z$,
Let \Coqe{ZofList} : $\Z \rightarrow \texttt{list}~\Z \rightarrow \Z$,
a parameterized map by $n$ between a list $l$ and its little endian representation
with a radix $2^n$.
\end{dfn}
......@@ -329,13 +342,13 @@ Notation "A :GF" := (A mod (2^255-19)).
Later in \sref{sec:maths}, we formally define \F{\p}.
Equivalence between operations under \coqe{:GF} and in \F{\p} are easily proven.
Using these two definitions, we proved intermediates lemmas such as the correctness of the
multiplication \Coqe{Low.MM} where \Coqe{Low.M} replicate the computations and steps done in C.
Using these two definitions, we prove intermediate lemmas such as the correctness of the
multiplication \Coqe{Low.M} where \Coqe{Low.M} replicate the computations and steps done in C.
\begin{lemma}
\label{lemma:mult_correct}
\Coqe{Low.M} implements correctly the multiplication over \Zfield.
\end{lemma}
And seen in Coq as follows:
And specified in Coq as follows:
\begin{lstlisting}[language=Coq]
Lemma mult_GF_Zlength :
forall (a:list Z) (b:list Z),
......@@ -368,12 +381,14 @@ Lemma M_bound_Zlength :
\subsection{Inversions, Reflections and Packing}
\label{subsec:inversions-reflections}
We now turn our attention to the inversion in \Zfield and techniques to
increase the verification speed of complex formulas.
We now turn our attention to the multiplicative inverse in \Zfield and techniques
to improve the verification speed of complex formulas.
\subheading{Inversions in \Zfield.}
\subheading{Inversion in \Zfield.}
We define a Coq version of the inversion mimicking
the behavior of \TNaCle{inv25519} (see below) over \Coqe{list Z}.
\begin{lstlisting}[language=Ctweetnacl]
......@@ -469,7 +484,7 @@ will take a long time to verify.
flexibility, \eg we don't need to know the number of times nor the order
in which the lemmas needs to be applied (chapter 15 in \cite{CpdtJFR}).
The idea is to \textit{reflect} the goal into a decidable environment.
The idea is to \emph{reflect} the goal into a decidable environment.
We show that for a property $P$, we can define a decidable Boolean property
$P_{bool}$ such that if $P_{bool}$ is \Coqe{true} then $P$ holds.
$$reify\_P : P_{bool} = true \implies P$$
......@@ -656,7 +671,13 @@ Lemma Pack25519_mod_25519 :
By proving that each functions \coqe{Low.M}; \coqe{Low.A}; \coqe{Low.Sq}; \coqe{Low.Zub};
\coqe{Unpack25519}; \coqe{clamp}; \coqe{Pack25519}; \coqe{car25519} are behaving over \coqe{list Z}
as their equivalent over \coqe{Z} in \coqe{:GF} (in \Zfield), we prove the correctness of
\tref{thm:RFC}. This is formalized as follows in Coq:
\begin{theorem}
\label{thm:crypto-rfc}
\coqe{Crypto_Scalarmult} matches the specification of RFC~7748.
\end{theorem}
This is formalized as follows in Coq:
\begin{lstlisting}[language=Coq]
Theorem Crypto_Scalarmult_Eq :
forall (n p:list Z),
......@@ -667,3 +688,8 @@ Theorem Crypto_Scalarmult_Eq :
ZofList 8 (Crypto_Scalarmult n p) =
ZCrypto_Scalarmult (ZofList 8 n) (ZofList 8 p).
\end{lstlisting}
We prove that \coqe{Crypto_Scalarmult} matches the specification of RFC~7748 (\tref{thm:crypto-rfc}).
With the VST we also prove that \coqe{Crypto_Scalarmult} matches the Clight translation of Tweetnacl (\tref{thm:crypto-vst}).
We infer that the implementation of X25519 in TweetNaCl (\TNaCle{crypto_scalarmult}) matches
the specifications of RFC~7748 (\tref{thm:VST-RFC}).
......@@ -5,12 +5,16 @@ In this section, we first give a brief summary of the mathematical background
on elliptic curves. We then describe X25519 and its implementation in TweetNaCl.
Finally, we provide a brief description of the formal tools we use in our proofs.
\subsection{Arithmetic on Montgomery curves}
\label{subsec:arithmetic-montgomery}
\begin{dfn}
Let $a,b \in \K$ such that $a^2 \neq 4$ and $b \neq 0$, $M_{a,b}$ is a
Montgomery curve defined over a field $\K$ with equation:
Given a field \K, let $a,b \in \K$ such that $a^2 \neq 4$ and $b \neq 0$,
$M_{a,b}$ is a Montgomery curve defined over $\K$ with equation:
$$M_{a,b}: by^2 = x^3 + ax^2 + x$$
\end{dfn}
......@@ -22,11 +26,12 @@ Finally, we provide a brief description of the formal tools we use in our proofs
\end{dfn}
Details of the formalization can be found in \sref{subsec:ECC-Montgomery}.
For $M_{a,b}$ over $\F{p}$, the parameter $b$ is known as the ``twisting factor'',
for $b'\in \F{p}\backslash\{0\}$ and $b' \neq b$, the curves $M_{a,b}$ and $M_{a,b'}$
are isomorphic via $(x,y) \mapsto (x, \sqrt{b'/b} \cdot y)$.
\begin{dfn}
For $M_{a,b}$ over $\F{p}$, the parameter $b$ is known as the ``twisting factor'',
for $b'\in \F{p}\backslash\{0\}$ and $b' \neq b$, the curves $M_{a,b}$ and $M_{a,b'}$
are isomorphic via $(x,y) \mapsto (x, \sqrt{b'/b} \cdot y)$.
When $b'/b$ is not a square in \F{p}, $M_{a,b'}$ is a quadratic twist of $M_{a,b}$:
When $b'/b$ is not a square in \F{p}, $M_{a,b'}$ is a \emph{quadratic twist} of $M_{a,b}$:
isomorphic over $\F{p^2}$~\cite{cryptoeprint:2017:212}.
\end{dfn}
......@@ -35,13 +40,18 @@ with the addition operation $\boxplus$ and with neutral element the point at inf
Using this law, we have the scalar multiplication over $M_{a,b}(\K)$ defined by:
$$n\cdot P = \underbrace{P \boxplus \cdots \boxplus P}_{n\text{ times}}$$
We now consider x-coordinate-only operations. In order to simplify computations,
In order to efficiently computes the scalar multiplication we use an algorithm
similar to square-and-multiply: the Montgomery ladder where the basic operations
are addition and doubling.
We consider x-coordinate-only operations. In order to simplify computations,
such coordinates are represented as $X/Z$ fractions. We define two operations:
\begin{align*}
\texttt{xADD} &: (X_P, Z_P, X_Q , Z_Q, X_{P-Q}, Z_{P-Q}) \mapsto (X_{P+Q}, Z_{P+Q})\\
\texttt{xDBL} &: (X_P, Z_P) \mapsto (X_{2P}, Z_{2P})
\texttt{xADD} &: (X_P, Z_P, X_Q , Z_Q, X_{P \boxminus Q}, Z_{P \boxminus Q}) \mapsto (X_{P \boxplus Q}, Z_{P \boxplus Q})\\
\texttt{xDBL} &: (X_P, Z_P) \mapsto (X_{2 \cdot P}, Z_{2 \cdot P})
\end{align*}
In the Montgomery ladder, notice that the arguments of \texttt{xADD} and \texttt{xDBL}
In the Montgomery ladder, % notice that
the arguments of \texttt{xADD} and \texttt{xDBL}
are swapped depending of the value of the $k^{th}$ bit. We use a conditional
swap \texttt{CSWAP} to change the arguments of the above function while keeping
the same body of the loop.
......@@ -68,6 +78,10 @@ computing a $x$-coordinate-only scalar multiplication (see \aref{alg:montgomery-
\end{algorithmic}
\end{algorithm}
\subsection{The X25519 key exchange}
\label{subsec:X25519-key-exchange}
......@@ -84,9 +98,9 @@ X25519 makes use of the little endian bijection for its arguments 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
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.
making $n$ 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
......@@ -95,10 +109,14 @@ of the scalar multiplication between $B$ and $s_a$ (respectively $s_b$).
The party exchanges $P_a$ and $P_b$ and computes their shared secret with X25519
over $s_a$ and $P_b$ (respectively $s_b$ and $P_a$).
\subsection{TweetNaCl specifics}
\label{subsec:Number-TweetNaCl}
As it names stands for, TweetNaCl aims for code compactness (in tweets).
As its name suggests, TweetNaCl aims for code compactness (in tweets).
As a result it uses a few defines and typedef to gain precious bytes while
still remaining readable.
\begin{lstlisting}[language=Ctweetnacl]
......@@ -108,15 +126,19 @@ typedef unsigned char u8;
typedef long long i64;
\end{lstlisting}
TweetNaCl functions takes pointers as arguments. By convention the first one
defines the output. It is then followed by the inputs arguments.
TweetNaCl functions take pointers as arguments. By convention the first one
points to the output array. It is then followed by the input arguments.
Due to some limitations of VST, indexes used in \TNaCle{for} loops have to be
of type \TNaCle{int} instead of \TNaCle{i64}. We change the code to allow our
proofs to carry through. We believe the original code is fine as is.
A complete diff of our modifications to TweetNaCl can be found in
proofs to carry through. We believe this does not affect the correctness of the
original code. A complete diff of our modifications to TweetNaCl can be found in
Appendix~\ref{verified-C-and-diff}.
\subsection{X25519 in TweetNaCl}
\label{subsec:X25519-TweetNaCl}
......@@ -148,9 +170,8 @@ sv unpack25519(gf o, const u8 *n)
The radix-$2^{16}$ representation in limbs of $64$ bits is
highly redundant; for any element $A \in \F{\p}$ there are
multiple ways to represent $A$ as $(a_0,\dots,a_{15})$.
For example, it is used to avoid carry handling in
the implementations of addition (\TNaCle{A})
and subtraction (\TNaCle{Z}) in $\F{\p}$:
This is used to avoid carry handling in the implementations of addition
(\TNaCle{A}) and subtraction (\TNaCle{Z}) in $\F{\p}$:
\begin{lstlisting}[language=Ctweetnacl]
sv A(gf o,const gf a,const gf b) {
int i;
......@@ -192,11 +213,11 @@ 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$.
we treat the last iteration of the loop $i = 15$ as a separate step.
Inverses in $\Zfield$ are computed with \TNaCle{inv25519}.
It takes the exponentiation by $2^{255}-21$ with the Square-and-multiply algorithm.
Fermat's little theorem brings the correctness.
It takes the exponentiation by $2^{255}-21$ with the square-and-multiply algorithm.
Fermat's little theorem gives the correctness.
Notice that in this case the inverse of $0$ is defined as $0$.
\TNaCle{sel25519} implements a constant-time conditional swap (\texttt{CSWAP}) by
......@@ -250,14 +271,14 @@ to a \emph{unique} representation before packing into the output
byte array.
\subheading{The Montgomery ladder.}
With these low-level arithmetic and helper function at hand, we can now
With these low-level arithmetic and helper functions at hand, we can now
turn our attention to the core of the X25519 computation:
the \TNaCle{crypto_scalarmult} API function of TweetNaCl.
In order to compute the scalar multiplication,
X25519 uses the Montgomery ladder~\cite{Mon85}.
$x$-coordinates are represented as fractions, the computation of the actual
value is deferred to the end of the ladder with \TNaCle{inv25519}.
$x$-coordinates are represented as not evaluated fractions, the computation of
the quotient is deferred 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.
......@@ -313,15 +334,19 @@ int crypto_scalarmult(u8 *q,
}
\end{lstlisting}
\subsection{Coq and VST}
\label{subsec:Coq-VST}
Coq~\cite{coq-faq} is an interactive theorem prover. It provides an expressive
formal language to write mathematical definitions, algorithms and theorems coupled
with their proofs. It has been used in the proof the four-color theorem~\cite{gonthier2008formal}.
The CompCert C compiler~\cite{Leroy-backend} was implemented with it and provides
the guarantee that the behavior of the machine code is the same as the one
semantically defined in C (ISO C99~\cite{ISO:C99}).
formal language to write mathematical definitions, algorithms and theorems together
with their proofs. It has been used in the proof of the four-color theorem~\cite{gonthier2008formal}.
The CompCert C compiler~\cite{Leroy-backend} was implemented with it.
The Compcert C sematinc is very close to C17~\cite{ISO:C17}, giving us the guarantee
that the intended behavior is preserved through the compilation to the machine code.
As opposed to other systems such as F*~\cite{DBLP:journals/corr/BhargavanDFHPRR17},
Coq does not rely on an SMT solver in its trusted code base.
......@@ -332,7 +357,7 @@ Hoare logic is a formal system which allows reasoning about programs.
It uses triples such as
$$\{{\color{doc@lstnumbers}\textbf{Pre}}\}\texttt{~Prog~}\{{\color{doc@lstdirective}\textbf{Post}}\}$$
where ${\color{doc@lstnumbers}\textbf{Pre}}$ and ${\color{doc@lstdirective}\textbf{Post}}$