Commit 1e83eaa3 authored by Benoit Viguier's avatar Benoit Viguier
Browse files

simplify inversion: no off by one

parent a8dff6b1
......@@ -7,7 +7,8 @@ In this section we prove the following theorem:
%\end{lstlisting}
\begin{theorem}
The implementation in TweetNaCl matches the Coq definition of \TNaCle{crypto_scalarmult}
The implementation X25519 in TweetNaCl (\TNaCle{crypto_scalarmult}) matches our
functional specification in Coq.
\end{theorem}
We first describe the global structure of our proof.
......@@ -16,7 +17,7 @@ Clight description of TweetNaCl and Coq functions producing similar behaviors.
In order to prove the correctness of X25519 in TweetNaCl code, we use VST to prove
that the code matches our functional specification of \TNaCle{crypto_scalarmult}
(abbreviated as CSM) in Coq. Then, we prove that our specification of the scalar
(abbreviated as \texttt{CSM}) in Coq. 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}. Figure~\ref{tk:ProofOverview} shows a graph of dependencies
of the proofs considered. The mathematical proof of our specification is presented
......@@ -30,19 +31,19 @@ in Section~\ref{sec3-maths}.
\end{figure}
Verifying \texttt{crypto\_scalarmult} also implies to verify all the functions
subsequently called: \texttt{unpack25519}; \texttt{A}; \texttt{Z}; \texttt{M};
\texttt{S}; \texttt{car25519}; \texttt{inv25519}; \texttt{set25519}; \texttt{sel25519};
\texttt{pack25519}.
Verifying \TNaCle{crypto_scalarmult} also implies to verify all the functions
subsequently called: \TNaCle{unpack25519}; \TNaCle{A}; \TNaCle{Z}; \TNaCle{M};
\TNaCle{S}; \TNaCle{car25519}; \TNaCle{inv25519}; \TNaCle{set25519}; \TNaCle{sel25519};
\TNaCle{pack25519}.
We prove the implementation of Curve25519 is \textbf{sound}, \ie:
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.
\end{itemize}
We also prove that TweetNaCl's code is \textbf{correct}:
\begin{itemize}
\item Curve25519 is correctly implemented (we get what we expect).
\item X25519 is correctly implemented (we get what we expect).
\item Operations on \texttt{gf} (\texttt{A}, \texttt{Z}, \texttt{M}, \texttt{S})
are equivalent to operations ($+,-,\times,x^2$) in \Zfield.
\item The Montgomery ladder computes a scalar multiplication between a natural
......@@ -73,11 +74,10 @@ This guarantees us the correctness of the implementation.
\label{tk:ProofStructure}
\end{figure}
\subsection{Correctness Specification}
We show the soundness of TweetNaCl by proving the following specification matches a pure Coq function.
We show the soundness of TweetNaCl by proving the following specification matches a pure Coq function. % why "pure" ?
This defines the equivalence between the Clight representation and a Coq definition of the ladder.
\begin{CoqVST}
......@@ -116,7 +116,7 @@ SEP (sh [{ v_q }] <<(uch32)-- mVI (CSM n p);
In this specification we state as preconditions:
\begin{itemize}
\item[] \VSTe{PRE}: \VSTe{_p OF (tptr tuchar)}\\
The function \texttt{crypto\_scalarmult} takes as input three pointers to
The function \TNaCle{crypto_scalarmult} takes as input three pointers to
arrays of unsigned bytes (\VSTe{tptr tuchar}) \VSTe{_p}, \VSTe{_q} and \VSTe{_n}.
\item[] \VSTe{LOCAL}: \VSTe{temp _p v_p}\\
Each pointer represent an address \VSTe{v_p},
......@@ -136,7 +136,7 @@ In this specification we state as preconditions:
As Post-condition we have:
\begin{itemize}
\item[] \VSTe{POST}: \VSTe{tint}\\
The function \texttt{crypto\_scalarmult} returns an integer.
The function \TNaCle{crypto_scalarmult} returns an integer.
\item[] \VSTe{LOCAL}: \VSTe{temp ret_temp (Vint Int.zero)}\\
The returned integer has value $0$.
\item[] \VSTe{SEP}: \VSTe{sh [{ v_q $\!\!\}\!\!]\!\!\!$ <<(uch32)-- mVI (CSM n p)}\\
......@@ -148,11 +148,13 @@ As Post-condition we have:
We show that the computation for \VSTe{CSM} fits in \TNaCle{u8[32]}.
\end{itemize}
This specification shows that \VSTe{crypto_scalarmult} in C computes the same
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.
\todo{TO MOVE TO THE NEXT SECTION}
By converting those array of 32 bytes into their respective little-endian value
we prove the correctness of \VSTe{crypto_scalarmult} (Theorem \ref{CSM-correct})
we prove the correctness of \TNaCle{crypto_scalarmult} (Theorem \ref{CSM-correct})
in Coq (for the sake of simplicity we do not display the conversion in the theorem).
\begin{theorem}
\label{CSM-correct}
......@@ -183,7 +185,7 @@ integers in Coq. However in order to show the correctness of the basic operation
we need to convert this number as a full integer.
\begin{definition}
Let \Coqe{ZofList} : $\Z \rightarrow \texttt{list} \Z \rightarrow \Z$, a parameterized map by $n$ between a list $l$ and its
it's little endian representation with a base $2^n$.
it's little endian representation with a radix $2^n$.
\end{definition}
We define it in Coq as:
\begin{lstlisting}[language=Coq]
......@@ -224,7 +226,7 @@ Lemma mult_GF_Zlength :
\subsection{Inversions in \Zfield}
We define a Coq version of the inversion mimicking
the behavior of \TNaCle{inv25519} over \Coqe{list Z}.
the behavior of \TNaCle{inv25519} (see below) over \Coqe{list Z}.
\begin{lstlisting}[language=Ctweetnacl]
sv inv25519(gf o,const gf a)
{
......@@ -239,11 +241,11 @@ sv inv25519(gf o,const gf a)
}
\end{lstlisting}
We specify this with 2 functions: a recursive \Coqe{pow_fn_rev} to to simulate the for loop and a simple
\Coqe{step_pow} containing the body. Note the off by one for the loop.
\Coqe{step_pow} containing the body.
\begin{lstlisting}[language=Coq]
Definition step_pow (a:Z) (c g:list Z) : list Z :=
let c := Sq c in
if a <>? 1 && a <>? 3
if a <>? 2 && a <>? 4
then M c g
else c.
......@@ -253,7 +255,7 @@ Function pow_fn_rev (a:Z) (b:Z) (c g: list Z)
then c
else
let prev := pow_fn_rev (a - 1) b c g in
step_pow (b - 1 - a) prev g.
step_pow (b - a) prev g.
\end{lstlisting}
This \Coqe{Function} requires a proof of termination. It is done by proving the
......@@ -267,7 +269,7 @@ Similarly we define the same function over $\Z$.
\begin{lstlisting}[language=Coq]
Definition step_pow_Z (a:Z) (c:Z) (g:Z) : Z :=
let c := c * c in
if a <>? 1 && a <>? 3
if a <>? 2 && a <>? 4
then c * g
else c.
......@@ -277,7 +279,7 @@ Function pow_fn_rev_Z (a:Z) (b:Z) (c:Z) (g: Z)
then c
else
let prev := pow_fn_rev_Z (a - 1) b c g in
step_pow_Z (b - 1 - a) prev g.
step_pow_Z (b - a) prev g.
Definition Inv25519_Z (x:Z) : Z :=
pow_fn_rev_Z 254 254 x x.
......@@ -394,7 +396,7 @@ In order to prove formulas in \Coqe{formula_inv},
we have the following a decidable procedure.
We define \Coqe{pow_expr_inv}, a function which returns the power of an expression.
We then compare the two values and decide over their equality.
\begin{Coq}
\begin{lstlisting}[language=Coq]
Fixpoint pow_expr_inv (t:expr_inv) : Z :=
match t with
| R_inv => 1
......@@ -420,7 +422,7 @@ Definition decide_f_inv (f:formula_inv) : bool :=
match f with
| Eq_inv x y => decide_e_inv x y
end.
\end{Coq}
\end{lstlisting}
We prove our decision procedure correct.
\begin{lemma}
\label{decide}
......@@ -428,35 +430,35 @@ For all formulas $f$, if the decision over $f$ returns \Coqe{true},
then the denoted equality by $f$ is true.
\end{lemma}
Which is formalized as:
\begin{Coq}
\begin{lstlisting}[language=Coq]
Lemma decide_formula_inv_impl :
forall (f:formula_inv),
decide_f_inv f = true ->
f_inv_denote f.
\end{Coq}
\end{lstlisting}
By reification to over DSL (lemma \ref{reify}) and by applying our decision (lemma \ref{decide}).
we proved the following theorem.
\begin{theorem}
\Coqe{Inv25519_Z} computes an inverse in \Zfield.
\end{theorem}
\begin{Coq}
\begin{lstlisting}[language=Coq]
Theorem Inv25519_Z_correct :
forall (x:Z),
Inv25519_Z x = pow x (2^255-21).
\end{Coq}
\end{lstlisting}
From \Coqe{Inv25519_Z_GF} and \Coqe{Inv25519_Z_correct}, we conclude the
functional correctness of the inversion over \Zfield.
\begin{corollary}
\Coqe{Inv25519} computes an inverse in \Zfield.
\end{corollary}
\begin{Coq}
\begin{lstlisting}[language=Coq]
Corollary Inv25519_Zpow_GF :
forall (g:list Z),
length g = 16 ->
Z16.lst (Inv25519 g) :GF =
(pow (Z16.lst g) (2^255-21)) :GF.
\end{Coq}
\end{lstlisting}
\subsection{Packing and other Applications of Reflection}
......@@ -484,13 +486,13 @@ This loop separation allows simpler proofs. The first loop is seen as the subtra
We then prove that with the iteration of the second loop, the number represented in $\Zfield$ stays the same.
This leads to the proof that \TNaCle{pack25519} is effectively reducing mod $\p$ and returning a number in base $2^8$.
\begin{Coq}
\begin{lstlisting}[language=Coq]
Lemma Pack25519_mod_25519 :
forall (l:list Z),
Zlength l = 16 ->
Forall (fun x => -2^62 < x < 2^62) l ->
ZofList 8 (Pack25519 l) = (Z16.lst l) mod (2^255-19).
\end{Coq}
\end{lstlisting}
\subsection{Using the Verifiable Software Toolchain}
\label{using-VST}
......
......@@ -49,9 +49,9 @@ To remove secret-dependent if-statements we use a constant-time conditional swap
\begin{algorithmic}
\REQUIRE{$b \in \{0, 1\}$ and a pair $(X_0, X_1)$ of objects encoded as $n$-bit strings}
\ENSURE{$(X_b, X_{1-b})$}
\STATE $b \leftarrow (b, \ldots, b)_n$
\STATE $mask \leftarrow b\texttt{ AND } (X_0\texttt{ XOR } X_1)$
\RETURN $(x_0 \texttt{ XOR } mask, x_1 \texttt{ XOR } mask)$
\STATE $B \leftarrow (b, \ldots, b)_n$
\STATE $Mask \leftarrow B \texttt{ AND } (X_0\texttt{ XOR } X_1)$
\RETURN $(X_0 \texttt{ XOR } Mask, X_1 \texttt{ XOR } Mask)$
\end{algorithmic}
\end{algorithm}
......@@ -104,6 +104,7 @@ over $s_a$ and $P_b$ (respectively $s_b$ and $P_a$).
\subsection{TweetNaCl specifics}
\label{preliminaries:B}
As it names stands for, 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.
......@@ -113,8 +114,21 @@ still remaining readable.
typedef unsigned char u8;
typedef long long i64;
\end{lstlisting}
Any TweetNaCl functions takes pointers as arguments.
The first one defines the output. It is then followed by the inputs arguments.
TweetNaCl functions takes pointers as arguments. By convention the first one
defines the output. It is then followed by the inputs 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 beleive the original code is fine as is.
A complete diff of our modifications to TweetNaCl can be found in
Appendix~\ref{verified-C-and-diff}.
\todo{MOVE this:}
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.
\todo{Metion Peter Wu and Jason A. Donenfeld change to car25519}
\subsection{X25519 in TweetNaCl}
\label{preliminaries:B}
......@@ -129,7 +143,6 @@ i.e., an element $A$ is represented as $(a_0,\dots,a_{15}$,
with $A = \sum_{i=0}^{15}a_i2^{16i}$.
The individual ``limbs'' $a_i$ are represented as
64-bit \TNaCle{long long} variables:
\begin{lstlisting}[language=Ctweetnacl]
typedef i64 gf[16];
\end{lstlisting}
......@@ -151,7 +164,6 @@ 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}$:
\begin{lstlisting}[language=Ctweetnacl]
sv A(gf o,const gf a,const gf b) {
int i;
......@@ -166,7 +178,6 @@ sv Z(gf o,const gf a,const gf b) {
Also multiplication (\TNaCle{M}) is heavily exploiting the redundancy
of the representation to delay carry handling.
\begin{lstlisting}[language=Ctweetnacl]
sv M(gf o,const gf a,const gf b) {
i64 i,j,t[31];
......@@ -182,7 +193,6 @@ sv M(gf o,const gf a,const gf b) {
After the actual multiplication, the limbs of the result \texttt{o} are
too large to be used again as input, which is why the two calls to
\TNaCle{car25519} at the end of \TNaCle{M} propagate the carries through the limbs:
\begin{lstlisting}[language=Ctweetnacl]
sv car25519(gf o)
{
......@@ -193,29 +203,17 @@ 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$.
% \begin{lstlisting}[language=Ctweetnacl]
% sv car25519(gf o)
% {
% int i;
% i64 c;
% FOR(i,15) {
% o[(i+1)]+=o[i]>>16;
% o[i]&=0xffff;
% }
% o[0]+=38*(o[15]>>16);
% o[15]&=0xffff;
% }
% \end{lstlisting}
Inverse in $\Zfield$ are computed with \TNaCle{inv25519}.
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.
Notice that in this case the inverse of $0$ is defined as $0$.
\TNaCle{sel25519} implements a constant-time conditional swap by applying a mask between
two fields elements.
\TNaCle{sel25519} implements a constant-time conditional \texttt{SWAP} (Algorithm~\ref{c-swap})
by applying a mask between two fields elements.
% \begin{lstlisting}[language=Ctweetnacl]
% sv sel25519(gf p,gf q,i64 b)
% {
......@@ -229,15 +227,9 @@ two fields elements.
% }
% \end{lstlisting}
% It takes advantage of the shape of the number by not doing the multiplications only twice.
% \todo{Ladder algorithm C code}
% \todo{Ladderstep algorithm C code}
Finally, we require the \TNaCle{pack25519} function,
which converts from the internal redundant radix-$2^{16}$
representation to a unique byte array:
\begin{lstlisting}[language=Ctweetnacl]
sv pack25519(u8 *o,const gf n)
{
......
......@@ -62,7 +62,7 @@
\draw (0,0) -- (0.4, 0.4) -- (2,0.4) -- (2,0) -- cycle;
\draw (0,0) -- (2,0) -- (2,-1) -- (0, -1) -- cycle;
\draw (0.3,-0.05) node[textstyle] {Definition};
\draw (1,-0.5) node[textstyle, anchor=center] {$[n]P$};
\draw (1,-0.5) node[textstyle, anchor=center] {$n \cdot P$};
\end{scope}
% Correctness Theorem
......@@ -71,7 +71,7 @@
\draw (0,0) -- (2.5,0) -- (2.5,-1.5) -- (0, -1.5) -- cycle;
\draw (0.3,-0.05) node[textstyle] {Proof};
\draw (2.5,-1.5) node[textstyle, anchor = south east] {\color{doc@lstfunctions}{\checkmark}};
\draw (1.25,-0.75) node[textstyle, anchor=center] {{\color{doc@lstnumbers}\textbf{Pre}} $\implies$\\$\text{\texttt{CSM}}(n,P) = [n]P$};
\draw (1.25,-0.75) node[textstyle, anchor=center] {{\color{doc@lstnumbers}\textbf{Pre}} $\implies$\\$\text{\texttt{CSM}}(n,P) = n \cdot P$};
\end{scope}
\path [thick, double, ->] (1.25,-0.5) edge (2.5, -0.5);
......
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