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

fix a few typos + more text

parent f6981a9b
......@@ -22,3 +22,13 @@ clean:
@rm *.log 2> /dev/null || true
@rm *.out 2> /dev/null || true
@rm */*.aux 2> /dev/null || true
spell:
aspell -t -c tweetverif.tex
aspell -t -c intro.tex
aspell -t -c preliminaries.tex
aspell -t -c lowlevel.tex
aspell -t -c highlevel.tex
aspell -t -c conclusion.tex
aspell -t -c tweetnacl.tex
......@@ -376,7 +376,10 @@ note = {\url{https://books.google.nl/books?id=T_ShHENlqBAC&lpg=PR4&pg=PP1#v=o
note = {\url{https://eprint.iacr.org/2017/536.pdf}}
}
@misc{zmq,
title = {ZeroMQ},
note = {\url{http://zeromq.org/}}
@misc{cryptoeprint:2017:212,
author = {Craig Costello and Benjamin Smith},
title = {Montgomery curves and their arithmetic: The case of large characteristic fields},
howpublished = {Cryptology ePrint Archive, Report 2017/212},
year = {2017},
note = {\url{https://eprint.iacr.org/2017/212}},
}
......@@ -23,17 +23,17 @@ Lemma f_ext: forall (A B:Type),
(forall x, f(x) = g(x)) -> f = g.
\end{lstlisting}
\item \textbf{Verifiable Software Toolchain}. This framework developped at
\item \textbf{Verifiable Software Toolchain}. This framework developed at
Princeton allows a user to prove that a \texttt{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 begining of
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.
\item \textbf{CompCert}. The formally proven compiler. We trust that the Clight
model captures correctly the C standard.
\todo{VERIFY THIS, WHICH STANDARD ?}.
Our proof also assumes that the TweetNaCl code will behave as expected if
compiled under CompCert. We do not provide garantees for other C compilers
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
......@@ -48,7 +48,7 @@ o[i] = aux1 + aux2;
The trust of the proof relied on the trust of a correct translation from the
initial version of \textit{TweetNaCl} to \textit{TweetNaclVerificable}.
While this problem is still present, the Compcert developpers provided us with
While this problem is still present, the CompCert developers provided us with
the \texttt{-normalize} option for \texttt{clightgen} which takes care of
generating auxiliary variables in order to automatically derive these steps.
The changes required for a C-code to make it Verifiable are now minimal.
......
......@@ -4,7 +4,7 @@
In this section we first present the work of Bartzia and Strub \cite{DBLP:conf/itp/BartziaS14} (\ref{Weierstrass}).
We extend it to support Montgomery curves (\ref{montgomery}) with homogeneous coordinates (\ref{projective}) and prove the correctness of the ladder (\ref{ladder}).
We then prove the montgomery ladder computes
We then prove the Montgomery ladder computes
the x-coordinate of scalar multiplication over $\F{p^2}$
(Theorem 2.1 by Bernstein \cite{Ber06}) where $p$ is the prime $\p$.
......@@ -35,7 +35,7 @@ along with an additional formal point $\Oinf$, ``at infinity''. Such curve does
\end{definition}
In this setting, Bartzia and Strub defined the parametric type \texttt{ec} which
represent the points on a specific curve. It is parametrized 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 --
and \texttt{E : ecuType} -- a record that packs the curve parameters $a$ and $b$
along with the proof that $\Delta(a,b) \neq 0$.
......@@ -53,15 +53,15 @@ Definition oncurve (p : point) :=
Inductive ec : Type := EC p of oncurve p.
\end{lstlisting}
Points of an elliptic curve can be equiped with a structure of an abelian group.
Points of an elliptic curve can be equipped with a structure of an abelian group.
\begin{itemize}
\item The negation of a point $P = (x,y)$ by taking the symetric with respect to the x axis $-P = (x, -y)$.
\item The negation of a point $P = (x,y)$ by taking the symmetric with respect to the x axis $-P = (x, -y)$.
\item The addition of two points $P$ and $Q$ is defined by the negation of third intersection
of the line passing by $P$ and $Q$ or tangent to $P$ if $P = Q$.
\item $\Oinf$ is the neutral element under this law: if 3 points are colinear, 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}
This operaction are defined in Coq as follow:
This operation are defined in Coq as follow:
\begin{lstlisting}[language=Coq]
Definition neg (p : point) :=
if p is (| x, y |) then (| x, -y |) else EC_Inf.
......@@ -99,9 +99,9 @@ the Montgomery form \cite{MontgomerySpeeding}.
along with an additional formal point $\Oinf$, ``at infinity''.
\end{definition}
Using a similar representation, we defined the parametric type \texttt{mc} which
represent the points on a specific montgomery curve. It is parametrized by
represent the points on a specific Montgomery curve. It is parameterized by
a \texttt{K : ecuFieldType} -- the type of fields which characteristic is not 2 or 3 --
and \texttt{M : mcuType} -- a record that packs the curve paramaters $a$ and $b$
and \texttt{M : mcuType} -- a record that packs the curve parameters $a$ and $b$
along with the proofs that $b \neq 0$ and $a^2 \neq 4$.
\begin{lstlisting}[language=Coq]
Record mcuType :=
......@@ -170,7 +170,7 @@ Points on a projective plane are represented with a triple $(X:Y:Z)$. Any points
except $(0:0:0)$ defines a point on a projective plane. A scalar multiple of a point defines the same point, \ie
for all $\alpha \neq 0$, $(X:Y:Z)$ and $(\alpha X:\alpha Y:\alpha Z)$ defines
the same point. For $Z\neq 0$, the projective point $(X:Y:Z)$ corresponds to the
point $(X/Z,Y/Z)$ on the Euclidian plane, likewise the point $(X,Y)$ on the Euclidian plane corresponds to $(X:Y:1)$ on the projective plane.
point $(X/Z,Y/Z)$ on the Euclidean plane, likewise the point $(X,Y)$ on the Euclidean plane corresponds to $(X:Y:1)$ on the projective plane.
We write the equation for a Montgomery curve $M_{a,b}(\K)$ as such:
\begin{equation}
......@@ -183,7 +183,7 @@ b Y^2Z = X^3 + a X^2Z + XZ^2
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$.
By restristing 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$.
\begin{lstlisting}[language=Coq]
Hypothesis mcu_no_square : forall x : K, x^+2 != (M#a)^+2 - 4%:R.
......@@ -475,7 +475,7 @@ We consider $M_{486662,1}(\F{p})$ and $M_{486662,2}(\F{p})$, one of its quadrati
% $M_{486662,1}(\F{p})$ has the same equation as $M_{486662,1}(\F{p^2})$ while $M_{486662,2}(\F{p})$ is one of its quadratic twist.
By instanciating theorem \ref{montgomery-ladder-correct} we derive the following two lemmas:
By instantiating theorem \ref{montgomery-ladder-correct} we derive the following two lemmas:
\begin{lemma} For all $x \in \F{p},\ n \in \N,\ P \in \F{p} \times \F{p}$,\\
such that $P \in M_{486662,1}(\F{p})$ and $\chi_0(P) = x$.
Given $n$ and $x$, $Curve25519\_Fp(n,x) = \chi_0(n \cdot P)$.
......@@ -540,11 +540,11 @@ Additionally we verify that for each element of in $\F{p^2}\backslash\{0\}$, the
\begin{lemma} For all $x \in \F{p^2}\backslash\{0\}$ and $a,b \in \F{p}$ such that $x = (a,b)$,
$$x^{-1} = \Big(\frac{a}{a^2-2b^2}\ , \frac{-b}{a^2-2b^2}\Big)$$
\end{lemma}
Similarily as in $\F{p}$, we define $0^{-1} = 0$.
Similarly as in $\F{p}$, we define $0^{-1} = 0$.
\begin{lemma}
$\F{p^2}$ is a commutative ring.
\end{lemma}
We can then specialize the basic operations in order to speed up the verifications of formulas by using rewrite rules:
We can then specialize the basic operations in order to speed up the verification of formulas by using rewrite rules:
\begin{align*}
(a,0) + (b,0) &= (a+b, 0)\\
(a,0) \cdot (b,0) &= (a \cdot b, 0)\\
......@@ -556,7 +556,7 @@ We can then specialize the basic operations in order to speed up the verificatio
\end{align*}
The injection $a \mapsto (a,0)$ from $\F{p}$ to $\F{p^2}$ preserves $0, 1, +, -, \times$. Thus $(a,0)$ can be abbreviated as $a$ without confusions.
We define $M_{486662,1}(\F{p^2})$. With the rewrite rule above, it is straightforward to prove that any point on the curve $M_{486662,1}(\F{p})$ is also on the curve $M_{486662,1}(\F{p^2})$. Similarily, any point on the quadratic twist $M_{486662,2}(\F{p})$ is also on the curve $M_{486662,1}(\F{p^2})$.
We define $M_{486662,1}(\F{p^2})$. With the rewrite rule above, it is straightforward to prove that any point on the curve $M_{486662,1}(\F{p})$ is also on the curve $M_{486662,1}(\F{p^2})$. Similarly, any point on the quadratic twist $M_{486662,2}(\F{p})$ is also on the curve $M_{486662,1}(\F{p^2})$.
As direct consequence, using lemma \ref{curve-or-twist}, we prove that for all $x \in \F{p}$, there exists a point $P \in \F{p^2}\times\F{p^2}$ on $M_{486662,2}(\F{p})$ such that $\chi_0(P)$ is $(x,0)$
\begin{lstlisting}[language=Coq]
......
\section{Introduction}
\label{sec:intro}
The Networking and Cryptography library (NaCl)~\cite{BLS12}
is an easy-to-use, high-security, high-speed cryptographic library.
The Networking and Cryptography library (NaCl)~\cite{BLS12}
is an easy-to-use, high-security, high-speed cryptography library.
It uses specialized code for different platform, which makes it rather complex and hard to audit.
TweetNaCl~\cite{BGJ+15} is a compact reimplementation in C
of the core functionalities of NaCl and is claimed to be
TweetNaCl~\cite{BGJ+15} is a compact re-implementation in C
of the core functionalities of NaCl and is claimed to be
\emph{``the first cryptographic library that allows correct functionality
to be verified by auditors with reasonable effort''}~\cite{BGJ+15}.
The original paper presenting TweetNaCl describes some effort to support
......@@ -16,9 +16,9 @@ One core component of TweetNaCl (and NaCl) is the key-exchange protocol X25519~\
This protocol is being 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
an insecure channel.
The X25519 key exchange protocol is a an $x$-coordinate only
The X25519 key exchange protocol is a an $x$-coordinate only
elliptic-curve Diffie-Hellman key-exchange using the Montgomery
curve $E: y^2 = x^3 + 486662 x^2 + x$ over the field $\F{2^{255}-19}$.
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}.
......@@ -26,12 +26,12 @@ We make use of this updated notation in this paper.
\subheading{Contribution of this paper}
We provide a mechanized formal proof of the correctness of the X25519
implementation in TweetNaCl.
This proof is done in two steps:
We first prove equivalence of the C implementation of X25519
implementation in TweetNaCl.
This proof is done in two steps:
We first prove equivalence of the C implementation of X25519
to an implementation in Coq~\cite{coq-faq}.
This part of the proof uses the Verifiable Software Toolchain (VST)~\cite{2012-Appel}
to establish a link between C and Coq.
to establish a link between C and Coq.
VST uses Separation logic~\cite{1969-Hoare,Reynolds02separationlogic}
to show that the semantics of the program satisfy a functional specification in Coq.
To the best of our knowledge, this is the first time that
......@@ -42,7 +42,7 @@ In a second step we prove that the Coq implementation matches
the mathematical definition of X25519 as given in~\cite[Sec.~2]{Ber06}.
We accomplish this step of the proof by extending the Coq library
for elliptic curves~\cite{DBLP:conf/itp/BartziaS14} by Bartzia and Strub to
support Mongomery curves (and in particular Curve25519).
support Montgomery curves (and in particular Curve25519).
This extension may be of independent interest.
\subheading{Related work.}
......
\section{Proving equivalence of X25519 in C and Coq}
\label{C-Coq}
In this section we prove the following theorem:
%\begin{lstlisting}[language=Coq]
%Lemma body_crypto_scalarmult: semax_body Vprog Gprog f_crypto_scalarmult_curve25519_tweet crypto_scalarmult_spec.
%\end{lstlisting}
\begin{theorem}
The implementation in TweetNaCl matches the Coq definition of \TNaCle{crypto_scalarmult}
\end{theorem}
In this section we first describe the global structure of our proof.
Then we discuss techniques used to prove the equivalence between the
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 \texttt{crypto\_scalarmult}
(abreviated as CSM) in Coq. Then, we prove that our specification of the scalar
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
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
......@@ -40,7 +49,7 @@ are equivalent to operations ($+,-,\times,x^2$) in \Zfield.
number and a point.
\end{itemize}
In order to prove the soundness and correctness of \texttt{crypto\_scalarmult},
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...
A high level specification (over a generic field $\K$) allows us to prove the
......@@ -56,7 +65,7 @@ By showing that operations over instances ($\K = \Zfield$, $\Z$, list of $\Z$) a
equivalent, we bridge the gap between the low level and the high level specification
with Curve25519 parameters.
As such, we prove all specifications to equivalent (Fig.\ref{tk:ProofStructure}).
This garantees us the correctness of the implementation.
This guarantees us the correctness of the implementation.
\begin{figure}[h]
\include{tikz/specifications}
......@@ -173,7 +182,7 @@ 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 as a full integer.
\begin{definition}
Let \Coqe{ZofList} : $\Z \rightarrow \texttt{list} \Z \rightarrow \Z$, a parametrized map by $n$ betwen a list $l$ and its
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$.
\end{definition}
We define it in Coq as:
......@@ -248,13 +257,13 @@ Function pow_fn_rev (a:Z) (b:Z) (c g: list Z)
\end{lstlisting}
This \Coqe{Function} requires a proof of termination. It is done by proving the
well-foundness of the decreasing argument: \Coqe{measure Z.to_nat a}. Calling
well-foundedness of the decreasing argument: \Coqe{measure Z.to_nat a}. Calling
\Coqe{pow_fn_rev} 254 times allows us to reproduce the same behavior as the \texttt{Clight} definition.
\begin{lstlisting}[language=Coq]
Definition Inv25519 (x:list Z) : list Z :=
pow_fn_rev 254 254 x x.
\end{lstlisting}
Similarily we define the same function over $\Z$.
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
......@@ -303,7 +312,7 @@ It provides us with flexibility, for example, we don't need to know the number o
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.
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.
$$reify\_P : P_{bool} = true \implies P$$
By applying $reify\_P$ on $P$ our goal become $P_{bool} = true$.
......@@ -358,7 +367,7 @@ f_inv_denote
\end{lstlisting}
On the right side, \Coqe{(x * x^2 = x^3)} depends on $x$. On the left side,
\texttt{(Eq\_inv (M\_inv R\_inv (S\_inv R\_inv)) (P\_inv R\_inv 3))} does not depend on $x$.
This allows us to use computations in our decision precedure.
This allows us to use computations in our decision procedure.
We define \Coqe{step_inv} and \Coqe{pow_inv} to mirror the behavior of
\Coqe{step_pow_Z} and respectively \Coqe{pow_fn_rev_Z} over our DSL and
......@@ -437,7 +446,7 @@ Theorem Inv25519_Z_correct :
\end{Coq}
From \Coqe{Inv25519_Z_GF} and \Coqe{Inv25519_Z_correct}, we conclude the
functionnal correctness of the inversion over \Zfield.
functional correctness of the inversion over \Zfield.
\begin{corollary}
\Coqe{Inv25519} computes an inverse in \Zfield.
\end{corollary}
......@@ -461,7 +470,7 @@ for(i=1;i<15;i++) {
m[i-1]&=0xffff;
}
\end{lstlisting}
The first loop is computing the substraction while the second is applying the carrying.
The first loop is computing the subtraction while the second is applying the carrying.
\begin{lstlisting}[language=Ctweetnacl]
for(i=1;i<15;i++) {
m[i]=t[i]-0xffff
......@@ -471,7 +480,7 @@ for(i=1;i<15;i++) {
m[i-1]&=0xffff;
}
\end{lstlisting}
This loop separation allows simpler proofs. The first loop is seen as the substraction of a number in \Zfield.
This loop separation allows simpler proofs. The first loop is seen as the subtraction of a number in \Zfield.
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$.
......@@ -488,8 +497,8 @@ ZofList 8 (Pack25519 l) = (Z16.lst l) mod (2^255-19).
The Verifiable Software Toolchain uses a strongest postcondition strategy.
The user must first write a formal specification of the function he wants to verify in Coq.
This should be as close as possible to the C implementation behavior.
This will simplify the proof and help with stepping throught the CLight version of the software.
With the range of inputes defined, VST steps mechanically through each instruction
This will simplify the proof and help with stepping through the CLight version of the software.
With the range of inputs defined, VST steps mechanically through each instruction
and ask the user to verify auxiliary goals such as array bound access, or absence of overflows/underflows.
We call this specification a low level specification. A user will then have an easier
time to prove that his low level specification matches a simpler higher level one.
......@@ -528,7 +537,7 @@ $\{0,1,2,3\}$:
\end{itemize}
This solution allows us to make cases analysis over possible aliasing.
\subsection{Verifiying \texttt{for} loops}
\subsection{Verifying \texttt{for} loops}
Final state of \texttt{for} loops are usually computed by simple recursive functions.
However we must define invariants which are true for each iteration.
......@@ -580,4 +589,4 @@ Lemma Tail_Head_equiv :
forall (n:nat) (s:T),
rec_fn n s = rec_fn_rev n s.
\end{Coq}
Using this formalization, we prove that the 255 steps of the montgomery ladder in C provide the same computations are the one defined in Algorithm \ref{montgomery-double-add}.
Using this formalization, we prove that the 255 steps of the Montgomery ladder in C provide the same computations are the one defined in Algorithm \ref{montgomery-double-add}.
......@@ -41,6 +41,8 @@
\newcommand{\Z}{\ensuremath{\mathbb{Z}}}
\newcommand{\K}{\ensuremath{\mathbb{K}}}
% \renewcommand\L{\mathcal{L}}
\renewcommand{\L}{\ensuremath{\mathbb{L}}}
\newcommand{\ZZ}{\ensuremath{\mathbb{Z}}}
\newcommand{\corr}{\,\hat{=}\,}
\newcommand{\B}{\ensuremath{\mathbb{B}}}
......
......@@ -7,9 +7,55 @@ Finally, we provide a brief description of the formal tools we use in our proofs
\subsection{Arithmetic on Montgomery curves}
\label{subsec:montgomery}
\todo{Write; move some text from later parts of the paper to here}
\todo{High-level view of Montgomery ladder, similar to Alg. 1, but with differential addition}
\begin{definition}
Let $a,b \in \K$, $M_{a,b}$ is a Montgomery curve defined over a field $\K$ with equation:
$$M_{a,b}: by^2 = x^3 + ax^2 + x$$
where $a^2 \neq 4$ and $b \neq 0$.
\end{definition}
\begin{definition}
For any algebraic extension $\L$ of $\K$, $\K \subseteq \L$,
$M_{a,b}(\L)$ is the set of $\L$-rational points which satisfy the equation with
addition to the point at infinity $\Oinf$.
$$M_{a,b}(\L) = \{\Oinf\} \cup \{(x,y) \in \L \times \L~|~by^2 = x^3 + ax^2 + x\}$$
\end{definition}
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}$:
isomorphic over $\F{p^2}$~\cite{cryptoeprint:2017:212}.
Points over $M_{a,b}(\K)$ can be equipped with a structure of an abelian group
with the addition operation $\oplus$ and with neutral element the point at infinity $\Oinf$.
Using this law, we have the scalar multiplication over $M_{a,b}(\K)$ defined by:
$$n\cdot P = \underbrace{P \oplus \cdots \oplus P}_{n\text{ times}}$$
\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})\\
\end{align*}
\begin{algorithm}
\caption{Montgomery ladder for scalar mult.}
\label{montgomery-ladder}
\begin{algorithmic}
\REQUIRE{x-coordinate of $P$ : $P.x$, scalars $n$ and $m$, $n < 2^m$}
\ENSURE{$Q = n \cdot P$}
\STATE $Q \leftarrow (X_P, Z_P)$
\STATE $R \leftarrow \Oinf$
\FOR{$k$ := $m$ down to $1$}
\IF{$k^{\text{th}}$ bit of $n$ is $0$}
\STATE $R \leftarrow \texttt{xADD}(Q,R,X_P,Z_P)$
\STATE $Q \leftarrow \texttt{xDBL}(X_P, Z_P)$
\ELSE
\STATE $Q \leftarrow \texttt{xADD}(Q,R,X_P,Z_P)$
\STATE $R \leftarrow \texttt{xDBL}(X_P, Z_P)$
\ENDIF
\ENDFOR
\end{algorithmic}
\end{algorithm}
\subsection{The X25519 key exchange}
\label{preliminaries:A}
......@@ -53,8 +99,8 @@ typedef long long i64;
\subheading{Arithmetic in \Ffield.}
In X25519, all computations are performed in $\F{p}$.
Throughout the computation, elements of that field
are represented in radix $2^{16}$,
Throughout the computation, elements of that field
are represented in radix $2^{16}$,
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
......@@ -66,17 +112,22 @@ typedef i64 gf[16];
Conversion from the input byte array to this representation is done
as follows:
\todo{unpack}
\begin{lstlisting}[language=Ctweetnacl]
sv unpack25519(gf o, const u8 *n)
{
int i;
FOR(i,16) o[i]=n[2*i]+((i64)n[2*i+1]<<8);
o[15]&=0x7fff;
}
\end{lstlisting}
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})
For example, it is used to avoid carry handling in
the implementations of addition (\TNaCle{A})
and subtraction (\TNaCle{Z}) in $\F{\p}$:
% and squaring (\texttt{S}).
\begin{lstlisting}[language=Ctweetnacl]
sv A(gf o,const gf a,const gf b) {
int i;
......@@ -134,12 +185,25 @@ sv car25519(gf o)
% }
% \end{lstlisting}
Inverse in $\Zfield$ are computed with \texttt{inv25519}.
Inverse 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$.
\todo{sel25519}
\TNaCle{sel25519} implements a constant-time conditional swap by applying a mask between
two fields elements.
% \begin{lstlisting}[language=Ctweetnacl]
% sv sel25519(gf p,gf q,i64 b)
% {
% int i;
% i64 t,c=~(b-1);
% FOR(i,16) {
% t= c&(p[i]^q[i]);
% p[i]^=t;
% q[i]^=t;
% }
% }
% \end{lstlisting}
% It takes advantage of the shape of the number by not doing the multiplications only twice.
......@@ -179,15 +243,15 @@ sv pack25519(u8 *o,const gf n)
\end{lstlisting}
As we can see, this function is considerably more complex than the
unpacking function. The reason is that it needs to convert
unpacking function. The reason is that it needs to convert
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
turn our attention to the core of the X25519 computation:
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,
In order to compute the scalar multiplication,
X25519 uses the Montgomery ladder~\cite{Mon85}.
\todo{explain, projective coordinates, etc}
of .
......@@ -248,12 +312,11 @@ int crypto_scalarmult(u8 *q,
\subsection{Coq and VST}
\label{preliminaries:C}
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. 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.
It uses its type system to verify the applications of hypotheses,
Coq does not rely on an SMT solver in its trusted code base.
It uses its type system to verify the applications of hypotheses,
lemmas, and theorems~\cite{Howard1995-HOWTFN}.
Hoare logic is a formal system which allows reasoning about programs.
......@@ -261,8 +324,8 @@ 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}}$
are assertions and \texttt{Prog} is a piece of code.
It is read as
``when the precondition ${\color{doc@lstnumbers}\textbf{Pre}}$ is met,
It is read as
``when the precondition ${\color{doc@lstnumbers}\textbf{Pre}}$ is met,
executing \texttt{Prog} will yield postcondition ${\color{doc@lstdirective}\textbf{Post}}$''.
We use compositional rules to prove the truth value of a Hoare triple.
For example, here is the rule for sequential composition:
......
......@@ -192,6 +192,6 @@ int crypto_scalarmult(u8 *q,const u8 *n,const u8 *p)
}
\end{lstlisting}
\subheading{Diff from Tweetnacl} We provide below the diff between the original code of TweetNaCl and the code we verified.
\subheading{Diff from TweetNaCl} We provide below the diff between the original code of TweetNaCl and the code we verified.
\lstinputlisting[language=diff]{tweetnacl.diff}
......@@ -20,7 +20,7 @@
\date{}
%make title bold and 14 pt font (Latex default is non-bold, 16 pt)
\title{\Large \bf A Coq proof of Tweetnacl's X25519 correctness}
\title{\Large \bf A Coq proof of TweetNaCl's X25519 correctness}
%for single author (just remove % characters)
\ifpublic
......
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