Commit 29ec42c5 authored by Freek Wiedijk's avatar Freek Wiedijk
Browse files

Merge branch 'master' of gitlab.science.ru.nl:benoit/tweetnacl

parents 105031fa 64002ca6
...@@ -107,7 +107,7 @@ Note that $n' \in 2^{254} + 8\{0,1,\ldots,2^{251}-1\}$. ...@@ -107,7 +107,7 @@ Note that $n' \in 2^{254} + 8\{0,1,\ldots,2^{251}-1\}$.
X25519 then computes the \xcoord of $n'\cdot P$. X25519 then computes the \xcoord of $n'\cdot P$.
RFC~7748~\cite{rfc7748} standardized the X25519 Diffie–Hellman key-exchange algorithm. RFC~7748~\cite{rfc7748} standardized the X25519 Diffie–Hellman key-exchange algorithm.
Given the base point $B$ where $X_B=9$, each party generate a secret random number Given the base point $B$ where $X_B=9$, each party generates a secret random number
$s_a$ (respectively $s_b$), and computes $X_{P_a}$ (respectively $X_{P_b}$), the $s_a$ (respectively $s_b$), and computes $X_{P_a}$ (respectively $X_{P_b}$), the
\xcoord of $P_A = s_a \cdot B$ (respectively $P_B = s_b \cdot B$). \xcoord of $P_A = s_a \cdot B$ (respectively $P_B = s_b \cdot B$).
The parties exchange $X_{P_a}$ and $X_{P_b}$ and compute their shared secret with The parties exchange $X_{P_a}$ and $X_{P_b}$ and compute their shared secret with
...@@ -118,7 +118,7 @@ X25519 on $s_a$ and $X_{P_b}$ (respectively $s_b$ and $X_{P_a}$). ...@@ -118,7 +118,7 @@ X25519 on $s_a$ and $X_{P_b}$ (respectively $s_b$ and $X_{P_a}$).
As its name suggests, TweetNaCl aims for code compactness (\emph{``a crypto library in 100 tweets''}). As its name suggests, TweetNaCl aims for code compactness (\emph{``a crypto library in 100 tweets''}).
As a result it uses a few defines and typedefs to gain precious bytes while As a result it uses a few defines and typedefs to gain precious bytes while
still remaining readable. still remaining human-readable.
\begin{lstlisting}[language=Ctweetnacl] \begin{lstlisting}[language=Ctweetnacl]
#define FOR(i,n) for (i = 0;i < n;++i) #define FOR(i,n) for (i = 0;i < n;++i)
#define sv static void #define sv static void
...@@ -129,7 +129,7 @@ typedef long long i64; ...@@ -129,7 +129,7 @@ typedef long long i64;
TweetNaCl functions take pointers as arguments. By convention the first one TweetNaCl functions take pointers as arguments. By convention the first one
points to the output array. It is then followed by the input arguments. 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 Due to some limitations of the 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 of type \TNaCle{int} instead of \TNaCle{i64}. We change the code to allow our
proofs to carry through. We believe this does not affect the correctness of the 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 original code. A complete diff of our modifications to TweetNaCl can be found in
...@@ -341,7 +341,7 @@ int crypto_scalarmult(u8 *q, ...@@ -341,7 +341,7 @@ int crypto_scalarmult(u8 *q,
% the pseudocode description % the pseudocode description
\subsection{Coq, separation logic, and VST} \subsection{Coq, separation logic, and the VST}
\label{subsec:Coq-VST} \label{subsec:Coq-VST}
Coq~\cite{coq-faq} is an interactive theorem prover based on type theory. It Coq~\cite{coq-faq} is an interactive theorem prover based on type theory. It
...@@ -382,6 +382,6 @@ The first step consists of translating the source code into Clight, ...@@ -382,6 +382,6 @@ The first step consists of translating the source code into Clight,
an intermediate representation used by CompCert. an intermediate representation used by CompCert.
For such purpose one uses the parser of CompCert called \texttt{clightgen}. For such purpose one uses the parser of CompCert called \texttt{clightgen}.
In a second step one defines the Hoare triple representing the specification of 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 the piece of software one wants to prove. Then using the VST, one uses a strongest
postcondition approach to prove the correctness of the triple. postcondition approach to prove the correctness of the triple.
This approach can be seen as a forward symbolic execution of the program. This approach can be seen as a forward symbolic execution of the program.
...@@ -26,7 +26,7 @@ Theorem body_crypto_scalarmult: ...@@ -26,7 +26,7 @@ Theorem body_crypto_scalarmult:
% We first describe the global structure of our proof (\ref{subsec:proof-structure}). % We first describe the global structure of our proof (\ref{subsec:proof-structure}).
Using our formalization of RFC~7748 (\sref{sec:Coq-RFC}) we specify the Hoare Using our formalization of RFC~7748 (\sref{sec:Coq-RFC}) we specify the Hoare
triple before proving its correctness with VST (\ref{subsec:with-VST}). triple before proving its correctness with the VST (\ref{subsec:with-VST}).
We provide an example of equivalence of operations over different number We provide an example of equivalence of operations over different number
representations (\ref{subsec:num-repr-rfc}). Then, we describe efficient techniques representations (\ref{subsec:num-repr-rfc}). Then, we describe efficient techniques
used in some of our more complex proofs (\ref{subsec:inversions-reflections}). used in some of our more complex proofs (\ref{subsec:inversions-reflections}).
...@@ -153,7 +153,7 @@ point to non-overlapping space in memory. ...@@ -153,7 +153,7 @@ point to non-overlapping space in memory.
When called with three memory fragments (\texttt{o, a, b}), When called with three memory fragments (\texttt{o, a, b}),
the three of them will be consumed. However assuming this naive specification 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 areas (\texttt{o, a}) when \texttt{M(o,a,a)} is called (squaring), the first two memory areas (\texttt{o, a})
are consumed and VST will expect a third memory section (\texttt{a}) which does not \emph{exist} anymore. are consumed and the VST will expect a third memory section (\texttt{a}) which does not \emph{exist} anymore.
Examples of such cases are illustrated in \fref{tikz:MemSame}. Examples of such cases are illustrated in \fref{tikz:MemSame}.
\begin{figure}[h]% \begin{figure}[h]%
\centering% \centering%
...@@ -246,7 +246,7 @@ Later in \sref{subsec:Zmodp}, we formally define $\Ffield$. ...@@ -246,7 +246,7 @@ Later in \sref{subsec:Zmodp}, we formally define $\Ffield$.
Equivalence between operations in $\Zfield$ (\ie under \coqe{:GF}) and in $\Ffield$ are easily proven. Equivalence between operations in $\Zfield$ (\ie under \coqe{:GF}) and in $\Ffield$ are easily proven.
Using these two definitions, we prove intermediate lemmas such as the correctness of the 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. multiplication \Coqe{Low.M} where \Coqe{Low.M} replicates the computations and steps done in C.
\begin{lemma} \begin{lemma}
\label{lemma:mult_correct} \label{lemma:mult_correct}
\Coqe{Low.M} correctly implements the multiplication over $\Zfield$. \Coqe{Low.M} correctly implements the multiplication over $\Zfield$.
...@@ -392,7 +392,7 @@ The idea is to \emph{reflect} the goal into a decidable environment. ...@@ -392,7 +392,7 @@ 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 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. $P_{bool}$ such that if $P_{bool}$ is \Coqe{true} then $P$ holds.
$$\text{\textit{reify\_P}} : P_{bool} = \text{\textit{true}} \implies P$$ $$\text{\textit{reify\_P}} : P_{bool} = \text{\textit{true}} \implies P$$
By applying \textit{reify\_P} on $P$ our goal become $P_{bool} = true$. By applying \textit{reify\_P} on $P$ our goal becomes $P_{bool} = true$.
We then compute the result of $P_{bool}$. If the decision goes well we are We then compute the result of $P_{bool}$. If the decision goes well we are
left with the tautology $\text{\textit{true}} = \text{\textit{true}}$. left with the tautology $\text{\textit{true}} = \text{\textit{true}}$.
......
...@@ -41,27 +41,28 @@ an elliptic curve $E$ ...@@ -41,27 +41,28 @@ an elliptic curve $E$
is a plane cubic algebraic curve defined by an equation $E(x,y)$ of the form: is a plane cubic algebraic curve defined by an equation $E(x,y)$ of the form:
$$E : y^2 + a_1 xy + a_3 y = x^3 + a_2 x^2 + a_4 x + a_6$$ $$E : y^2 + a_1 xy + a_3 y = x^3 + a_2 x^2 + a_4 x + a_6$$
where the $a_i$'s are in \K\ and the curve has no singular point (\ie no cusps where the $a_i$'s are in \K\ and the curve has no singular point (\ie no cusps
or self-intersections). The set of points, written $E(\K)$, is formed by the or self-intersections). The set of points defined over \K, written $E(\K)$, is formed by the
solutions $(x,y)$ of $E$ augmented by a distinguished point $\Oinf$ (called point at infinity): solutions $(x,y)$ of $E$ together with a distinguished point $\Oinf$ called point at infinity:
$$E(\K) = \{(x,y) \in \K \times \K | E(x,y)\} \cup \{\Oinf\}$$ $$E(\K) = \{ E(x,y)~|~(x,y) \in \K \times \K\} \cup \{\Oinf\}$$
\end{dfn} \end{dfn}
\subsubsection{Weierstra{\ss} curves} \subsubsection{Short Weierstra{\ss} curves}
\label{subsec:ECC-Weierstrass} \label{subsec:ECC-Weierstrass}
This equation $E(x,y)$ can be reduced into its short Weierstra{\ss} form. This equation $E(x,y)$ can be reduced into its short Weierstra{\ss} form.
\begin{dfn} \begin{dfn}
Let $a \in \K$, and $b \in \K$ such that $$\Delta(a,b) = -16(4a^3 + 27b^2) \neq 0.$$ Let $a \in \K$ and $b \in \K$ such that $$\Delta(a,b) = -16(4a^3 + 27b^2) \neq 0.$$
The \textit{elliptic curve} $E_{a,b}(\K)$ is the set of all points $(x,y) \in \K^2$ satisfying the equation: The \textit{elliptic curve} $E_{a,b}$ is defined by the equation:
$$y^2 = x^3 + ax + b,$$ $$y^2 = x^3 + ax + b.$$
$E_{a,b}(\K)$ is the set of all points $(x,y) \in \K^2$ satisfying the $E_{a,b}$
along with an additional formal point $\Oinf$, ``at infinity''. Such a curve does not have any singularity. along with an additional formal point $\Oinf$, ``at infinity''. Such a curve does not have any singularity.
\end{dfn} \end{dfn}
In this setting, Bartzia and Strub defined the parametric type \texttt{ec} which In this setting, Bartzia and Strub defined the parametric type \texttt{ec} which
represent the points on a specific curve. It is parameterized by represent the points on a specific curve. It is parameterized by
a \texttt{K : ecuFieldType} -- the type of fields which characteristic is not 2 or 3 -- a \texttt{K : ecuFieldType} --- the type of fields which characteristic is not 2 or 3 ---
and \texttt{E : ecuType} -- a record that packs the curve parameters $a$ and $b$ and \texttt{E : ecuType} --- a record that packs the curve parameters $a$ and $b$
along with the proof that $\Delta(a,b) \neq 0$. along with the proof that $\Delta(a,b) \neq 0$.
\begin{lstlisting}[language=Coq] \begin{lstlisting}[language=Coq]
Inductive point := EC_Inf | EC_In of K * K. Inductive point := EC_Inf | EC_In of K * K.
...@@ -77,11 +78,11 @@ Definition oncurve (p : point) := ...@@ -77,11 +78,11 @@ Definition oncurve (p : point) :=
Inductive ec : Type := EC p of oncurve p. Inductive ec : Type := EC p of oncurve p.
\end{lstlisting} \end{lstlisting}
Points of an elliptic curve are equipped with the structure of an abelian group. Points on an elliptic curve are equipped with the structure of an abelian group.
\begin{itemize} \begin{itemize}
\item The negation of a point $P = (x,y)$ is defined by reflecting in the $x$ axis $-P = (x, -y)$. \item The negation of a point $P = (x,y)$ is defined by reflection over the $x$ axis $-P = (x, -y)$.
\item The addition of two points $P$ and $Q$ is defined as the negation of the third intersection point \item The addition of two points $P$ and $Q$ is defined as the negation of the third intersection point
of the line passing through $P$ and $Q$ or tangent to $P$ if $P = Q$. of the line passing through $P$ and $Q$, or tangent to $P$ if $P = Q$.
\item $\Oinf$ is the neutral element under this law: if 3 points are collinear, their sum is equal to $\Oinf$. \item $\Oinf$ is the neutral element under this law: if 3 points are collinear, their sum is equal to $\Oinf$.
\end{itemize} \end{itemize}
These operations are defined in Coq as follows (where we omit the code for the tangent case): These operations are defined in Coq as follows (where we omit the code for the tangent case):
...@@ -124,9 +125,9 @@ than the Weierstra{\ss} form. We consider the Montgomery form \cite{MontgomerySp ...@@ -124,9 +125,9 @@ than the Weierstra{\ss} form. We consider the Montgomery form \cite{MontgomerySp
Similar to the definition of \texttt{ec}, we defined the parametric type \texttt{mc} which Similar to the definition of \texttt{ec}, we defined the parametric type \texttt{mc} which
represents the points on a specific Montgomery curve. represents the points on a specific Montgomery curve.
It is parameterized by It is parameterized by
a \texttt{K : ecuFieldType} -- the type of fields which characteristic is not 2 or 3 -- a \texttt{K : ecuFieldType} --- the type of fields which characteristic is not
and \texttt{M : mcuType} -- a record that packs the curve parameters $a$ and $b$ 2 or 3 --- and \texttt{M : mcuType} --- a record that packs the curve
along with the proofs that $b \neq 0$ and $a^2 \neq 4$. parameters $a$ and $b$ along with the proofs that $b \neq 0$ and $a^2 \neq 4$.
\begin{lstlisting}[language=Coq] \begin{lstlisting}[language=Coq]
Record mcuType := Record mcuType :=
{ cA : K; cB : K; _ : cB != 0; _ : cA^2 != 4}. { cA : K; cB : K; _ : cB != 0; _ : cA^2 != 4}.
...@@ -139,7 +140,6 @@ Inductive mc : Type := MC p of oncurve p. ...@@ -139,7 +140,6 @@ Inductive mc : Type := MC p of oncurve p.
Lemma oncurve_mc: forall p : mc, oncurve p. Lemma oncurve_mc: forall p : mc, oncurve p.
\end{lstlisting} \end{lstlisting}
We define the addition on Montgomery curves in the similar way as in the Weierstra{\ss} form. We define the addition on Montgomery curves in the similar way as in the Weierstra{\ss} form.
%, however the actual computations will be slightly different.
\begin{lstlisting}[language=Coq] \begin{lstlisting}[language=Coq]
Definition add (p1 p2 : point K) := Definition add (p1 p2 : point K) :=
match p1, p2 with match p1, p2 with
...@@ -162,7 +162,7 @@ Definition addmc (p1 p2 : mc) : mc := ...@@ -162,7 +162,7 @@ Definition addmc (p1 p2 : mc) : mc :=
MC p1 p2 (addO p1 p2) MC p1 p2 (addO p1 p2)
\end{lstlisting} \end{lstlisting}
We then define a bijection between a Montgomery curve and its Weierstra{\ss} form. We then define a bijection between a Montgomery curve and its short Weierstra{\ss} form.
In this way we get associativity of addition on Montgomery curves from the In this way we get associativity of addition on Montgomery curves from the
corresponding property for Weierstra{\ss} curves. corresponding property for Weierstra{\ss} curves.
\begin{lemma} \begin{lemma}
...@@ -172,9 +172,9 @@ corresponding property for Weierstra{\ss} curves. ...@@ -172,9 +172,9 @@ corresponding property for Weierstra{\ss} curves.
$\varphi : M_{a,b}(\K) \mapsto E_{a',b'}(\K)$ defined as: $\varphi : M_{a,b}(\K) \mapsto E_{a',b'}(\K)$ defined as:
\begin{align*} \begin{align*}
\varphi(\Oinf_M) &= \Oinf_E\\ \varphi(\Oinf_M) &= \Oinf_E\\
\varphi( (x , y) ) &= ( \frac{x}{b} + \frac{a}{3b} , \frac{y}{b} ) \varphi( (x , y) ) &= \left( \frac{x}{b} + \frac{a}{3b} , \frac{y}{b} \right)
\end{align*} \end{align*}
is an isomorphism between groups. is an isomorphism between elliptic curves.
\end{lemma} \end{lemma}
\begin{lstlisting}[language=Coq] \begin{lstlisting}[language=Coq]
Definition ec_of_mc_point p := Definition ec_of_mc_point p :=
...@@ -192,8 +192,6 @@ Definition ec_of_mc p := ...@@ -192,8 +192,6 @@ Definition ec_of_mc p :=
Lemma ec_of_mc_bij : bijective ec_of_mc. Lemma ec_of_mc_bij : bijective ec_of_mc.
\end{lstlisting} \end{lstlisting}
% We use this isomorphism to derive that $(M_{a,b}(\K), + )$ is a group.
\subsubsection{Projective coordinates} \subsubsection{Projective coordinates}
\label{subsec:ECC-projective} \label{subsec:ECC-projective}
...@@ -203,8 +201,8 @@ Scalar multiples are representing the same point, \ie ...@@ -203,8 +201,8 @@ Scalar multiples are representing the same point, \ie
for all $\lambda \neq 0$, the triples $(X:Y:Z)$ and $(\lambda X:\lambda Y:\lambda Z)$ represent for all $\lambda \neq 0$, the triples $(X:Y:Z)$ and $(\lambda X:\lambda Y:\lambda Z)$ represent
the same point. the same point.
For $Z\neq 0$, the projective point $(X:Y:Z)$ corresponds to the For $Z\neq 0$, the projective point $(X:Y:Z)$ corresponds to the
point $(X/Z,Y/Z)$ on the Euclidean plane. Likewise the point $(X,Y)$ on the point $(X/Z,Y/Z)$ on the affine plane. Likewise the point $(X,Y)$ on the
Euclidean plane corresponds to $(X:Y:1)$ on the projective plane. affine plane corresponds to $(X:Y:1)$ on the projective plane.
Using fractions as coordinates, the equation for a Montgomery curve $M_{a,b}(\K)$ Using fractions as coordinates, the equation for a Montgomery curve $M_{a,b}(\K)$
becomes: becomes:
...@@ -212,7 +210,7 @@ $$b \bigg(\frac{Y}{Z}\bigg)^2 = \bigg(\frac{X}{Z}\bigg)^3 + a \bigg(\frac{X}{Z}\ ...@@ -212,7 +210,7 @@ $$b \bigg(\frac{Y}{Z}\bigg)^2 = \bigg(\frac{X}{Z}\bigg)^3 + a \bigg(\frac{X}{Z}\
Multiplying both sides by $Z^3$ yields: Multiplying both sides by $Z^3$ yields:
$$b Y^2Z = X^3 + a X^2Z + XZ^2$$ $$b Y^2Z = X^3 + a X^2Z + XZ^2$$
With this equation we can additionally represent the ``point at infinity''. By With this equation we can additionally represent the ``point at infinity''. By
setting $Z=0$, we derive $X=0$, giving us the ``infinite points'' $(0:Y:0)$ with $Y\neq 0$. setting $Z=0$, we derive $X=0$, giving us the ``infinite point'' $(0:1:0)$.
By restricting the parameter $a$ of $M_{a,b}(\K)$ such that $a^2-4$ is not a By restricting the parameter $a$ of $M_{a,b}(\K)$ such that $a^2-4$ is not a
square in \K, we ensure that $(0,0)$ is the only point with a $y$-coordinate of $0$. square in \K, we ensure that $(0,0)$ is the only point with a $y$-coordinate of $0$.
...@@ -280,7 +278,7 @@ in the definition of \coqe{RFC}, and is easily proved to correspond to it. ...@@ -280,7 +278,7 @@ in the definition of \coqe{RFC}, and is easily proved to correspond to it.
In Coq this correspondence proof is hidden in the proof of \coqe{RFC_Correct} shown above.) In Coq this correspondence proof is hidden in the proof of \coqe{RFC_Correct} shown above.)
%\ref to the def of montgomery_rec? relevant lemma(s) that show(s) these are "the same"? %\ref to the def of montgomery_rec? relevant lemma(s) that show(s) these are "the same"?
We prove its correctness for any points which \xcoord is not 0. We prove its correctness for any point whose \xcoord is not 0.
% By taking \aref{alg:montgomery-ladder} and replacing \texttt{xDBL} and \texttt{xADD} % By taking \aref{alg:montgomery-ladder} and replacing \texttt{xDBL} and \texttt{xADD}
...@@ -371,7 +369,7 @@ Theorem opt_montgomery_ok (n m: nat) (x : K) : ...@@ -371,7 +369,7 @@ Theorem opt_montgomery_ok (n m: nat) (x : K) :
To be able to use the above theorem we need to satisfy hypothesis To be able to use the above theorem we need to satisfy hypothesis
\ref{hyp:a_minus_4_not_square}: $a^2-4$ is not a square in \K: \ref{hyp:a_minus_4_not_square}: $a^2-4$ is not a square in \K:
$$\forall x \in \K,\ x^2 \neq a^2-4$$ $$\forall x \in \K,\ x^2 \neq a^2-4.$$
If we consider the quadratic extension field $\F{p^2}$, If we consider the quadratic extension field $\F{p^2}$,
there exists $x$ such that $x^2 = a^2-4$, preventing use \tref{thm:montgomery-ladder-correct} there exists $x$ such that $x^2 = a^2-4$, preventing use \tref{thm:montgomery-ladder-correct}
with $\K = \F{p^2}$. with $\K = \F{p^2}$.
......
...@@ -59,7 +59,7 @@ Indeed indexes 17 to 79 of the \TNaCle{i64 x[80]} intermediate variable of ...@@ -59,7 +59,7 @@ Indeed indexes 17 to 79 of the \TNaCle{i64 x[80]} intermediate variable of
we removed them. we removed them.
Peter Wu and Jason A. Donenfeld brought to our attention that the original Peter Wu and Jason A. Donenfeld brought to our attention that the original
\TNaCle{car25519} function presented risk of undefined behavior if \texttt{c} \TNaCle{car25519} function carried a risk of undefined behavior if \texttt{c}
is a negative number. is a negative number.
\begin{lstlisting}[language=Ctweetnacl] \begin{lstlisting}[language=Ctweetnacl]
c=o[i]>>16; c=o[i]>>16;
......
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