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

more writting

parent 6534d52c
......@@ -136,7 +136,7 @@ Lemma Inv25519_bound_Zlength : forall g,
Proof. intros; rewrite /Inv25519; apply pow_fn_rev_bound_Zlength => //. Qed.
Lemma Inv25519_Zlength : forall g,
Zlength g = 16 ->
Zlength g = 16 ->
Zlength (Inv25519 g) = 16.
Proof. intros; rewrite /Inv25519; apply pow_fn_rev_Zlength => //. Qed.
......@@ -145,7 +145,7 @@ Lemma Inv25519_Z_GF : forall g,
ZofList 16 (Inv25519 g) :𝓖𝓕 = (Inv25519_Z (ZofList 16 g)) :𝓖𝓕 .
Proof. intros; rewrite /Inv25519 /Inv25519_Z; apply pow_fn_rev_Z_GF => //. Qed.
Lemma Inv25519_Zpow_GF : forall g,
Corollary Inv25519_Zpow_GF : forall g,
Zlength g = 16 ->
ZofList 16 (Inv25519 g) :𝓖𝓕 = (Z.pow (ZofList 16 g) (Z.pow 2 255 - 21)) :𝓖𝓕 .
Proof. intros. rewrite Inv25519_Z_GF //.
......
......@@ -2,3 +2,4 @@
By using the Coq formal proof assistant with the VST library, we prove the
soundness and correctness of TweetNaCl's Curve25519 implementation.
\todo[inline]{more text here, too short}
\section{Introduction}
Implementing cryptographic primitives without any bugs is hard.
While tests provides a some code coverage, they don't cover
100\% of the possible input values. Using Coq, we prove the
correctness of the scalar multiplication in Tweetnacl.
While tests provides a some code coverage and are used in the limits,
they still don't cover 100\% of the possible input values.
Using Coq, we prove the correctness of the scalar multiplication in Tweetnacl.
TweetNaCl\cite{BGJ+15} is a compact reimplementation of the
NaCl\cite{BLS12} library. It does not aim for high speed
......@@ -12,7 +12,7 @@ It maintains some degree of readability in order to be
easily auditable.
This library makes use of Curve25519\cite{Ber06}, an elliptic
curve defined over the field $\mathbb{Z}_{2^{255}-19}$.
curve defined over the field \Zfield.
It defines the function \texttt{crypto\_scalarmult} which
takes as input a scalar $n$ and the $x$ coordinate of a
point $P$ and returns the $x$ coordinate of the
......
\section{Curve25519 implementation}
In order to prove the correctness of \texttt{crypto\_scalarmult},
\todo[inline]{This part does not really make sens here. Needs to be rewritten.}
To prove the correctness of \texttt{crypto\_scalarmult},
we also need to do the same with all the functions subsequently called:
\texttt{unpack25519}; \texttt{A}; \texttt{Z}; \texttt{M}; \texttt{S};
\texttt{car25519}; \texttt{inv25519}; \texttt{set25519}; \texttt{sel25519};
......@@ -8,7 +9,7 @@ In order to prove the correctness of \texttt{crypto\_scalarmult},
\subsection{Implementation} \label{sec:impl}
Curve25519 is defined over $\mathbb{Z}_{2^{255}-19}$. Number in that field can
Curve25519 is defined over \Zfield. Number in that field can
be represented by a 256-bits number. Each of them represented in base $2^{16}$.
they are cut into 16 limbs of at least 16 bits placed into 64-bits signed
container.
......@@ -168,23 +169,22 @@ We prove that the implementation of Curve25519 is \textbf{sound} \ie
\item absence of overflows/underflow on the arithmetic.
\end{itemize}
\noindent
We also prove that TweetNaCl's code is \textbf{correct}:
\begin{itemize}
\item Curve25519 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 $\mathbb{Z}_{2^{255}-19}$
are equivalent to operations ($+,-,\times,x^2$) in \Zfield.
\end{itemize}
% \subsection{Meet-in-the-middle Approach}
In order to prove the soundness and correctness of \texttt{crypto\_scalarmult},
we defined multiples levels of specifications.
A high level specification (over a generic field $\mathbb{F}$) looking only at
the structure of the Montgomery ladder provided us with the correcntess.
A low level specification close to the \texttt{C} code (over lists of $\mathbb{Z}$)
gave us the soundness assurance.
We defined a third specification over $\mathbb{Z}_{2^{255}-19}$ (mid level) and
We defined a third specification over \Zfield (mid level) and
we proved to be an instance of the high level one.
We also proved its equivalence with the low level one.
As such we proved all specifications to equivalent (Fig.\ref{tk:ProofStructure}).
......@@ -204,7 +204,7 @@ We show the soundness of TweetNaCl by proving the {\red{equivalence}} of the fol
specification. This defines the equivalence between the Clight representation
and a Coq definition of the ladder.
\begin{lstlisting}[language=CoqVST]
\begin{CoqVST}
Definition crypto_scalarmult_spec :=
DECLARE _crypto_scalarmult_curve25519_tweet
WITH
......@@ -235,7 +235,7 @@ SEP (sh [{ v_q }] <<(uch32)-- mVI (CSM n p);
sh [{ v_n }] <<(uch32)-- mVI n;
sh [{ v_p }] <<(uch32)-- mVI p;
Ews [{ c121665 }] <<(lg16)-- mVI64 c_121665
\end{lstlisting}
\end{CoqVST}
In this specification we state as preconditions:
\begin{itemize}
......
\section{Mathematical Model}
\textbf{ASK TIMMY}
\todo[inline]{Timmy needs to write here}
......@@ -6,26 +6,26 @@ Clight description of TweetNaCl and Coq functions producing similar behaviors.
\subsection{Number representation and C implementation}
As described in Section \ref{sec:impl}, numbers in \TNaCle{gf} are represented
in base $2^16$ and we can use a direct mapping to represent that array as a list
in base $2^{16}$ and we can 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. For this reason We define
we need to convert this number as a full integer. For this reason we define
\coqDe{ZofList : Z -> list Z -> Z}:
\begin{lstlisting}[language=CoqD]
\begin{coqD}
Fixpoint ZofList {n:Z} (a:list Z) : Z :=
match a with
| [] => 0
| h :: q => h + 2^n * ZofList q
| h :: q => h + (pow 2 n) * ZofList q
end.
Notation "Z16.lst A" := (ZofList 16 A).
\end{lstlisting}
It convert any list of integer from a base $2^n$ to an single integer. In our
\end{coqD}
It converts any list of integer from a base $2^n$ to an single integer. In our
case we define a notation where $n$ is $16$.
The following Coq notation is defined to convert any integer to its representant
in $\mathbb{Z}_{2^{255}-19}$.
\begin{lstlisting}[language=CoqD]
in \Zfield.
\begin{coqD}
Notation "A :GF" := (A mod (2^255-19)).
\end{lstlisting}
\end{coqD}
Using these two definitions, we proved lemmas such as the correctness of the
multiplication \coqDe{M}:
......@@ -38,72 +38,132 @@ Lemma mult_GF_Zlength :
(Z16.lst a * Z16.lst b) :GF.
\end{coqD}
\subsection{Inversions and Reflections}
For all list of integers \texttt{a} and \texttt{b} of length 16 representing
$A$ and $B$ in \Zfield, the number represented in \Zfield by the list \coqDe{(M a b)}
is equal to $A \times B \bmod 2^{255}-19$.
To prove that the \coqDe{Inv25519_Z} is computing $\mathbb{Z}_{2^{255}-19}$,
In TweetNaCl, \TNaCle{inv25519} computes an inverse in $\mathbb{Z}_{2^{255}-19}$
In a similar fashion we can define a Coq version of the inversion mimicking
the behavior of \TNaCle{inv25519} over \coqDe{list Z}. \coqDe{step_pow} contains
the body of the for loop.
\coqDe{Inv25519} the inverse is computed using ht
{\red TODO: SAY WHY WE WANT TO USE REFLECTION}
\begin{coqD}
Definition step_pow (a:Z) (c g:list Z) : list Z :=
let c := Sq c in
if a <>? 1 && a <>? 3
then M c g
else c.
\end{coqD}
Reflection proofs relies on the decidability of an expression. In our case,
we show that for a property $P$, we can define a decidable
boolean property $P_{bool}$ such that $$P_{bool} = true \implies P$$
\coqDe{pow_fn_rev} is responsible of the iteration of the loop by making
recursive calls.
\begin{coqD}
Function pow_fn_rev (a:Z) (b:Z) (c g: list Z)
{measure Z.to_nat a} : (list Z) :=
if a <=? 0
then c
else
let prev := pow_fn_rev (a - 1) b c g in
step_pow (b - 1 - a) prev g.
\end{coqD}
With VST we proved that \TNaCle{inv25519} is equivalent to its Coq functional
definition \coqDe{Inv25519}.
% This \coqDe{Function} requires a proof of termination. It is done by proving the
% Well-foundness of the decreasing argument: \coqDe{measure Z.to_nat a}.
Calling \coqDe{pow_fn_rev} 254 times allows us to reproduce the same behavior as
the Clight definition.
\begin{coqD}
Definition Inv25519 (x:list Z) : (list Z) :=
Definition Inv25519 (x:list Z) : list Z :=
pow_fn_rev 254 254 x x.
\end{coqD}
We proved that \coqDe{pow_fn_rev} over \coqDe{list Z} is equivalent to applying
\coqDe{pow_fn_rev_Z} over \coqDe{Z}
\subsection{Inversions and Reflections}
In TweetNaCl, \TNaCle{inv25519} computes an inverse in \Zfield. It uses the
Fermat's little theorem by the exponentiation to $2^{255}-21$. To prove the
correctness of the result we can use multiple strategy such as:
\begin{itemize}
\item Proving it is special case of square-and-multiply algorithm applied to
a specific number and then show that this number is indeed $2^{255}-21$.
\item Unrolling the for loop step-by-step and applying the equalities
$x^a \times x^b = x^{(a+b)}$ and $(x^a)^2 = x^{(2 \times a)}$. We can prove that
the resulting exponent is $2^{255}-21$.
\end{itemize}
We choose the second method. The only drawback is that it requires to apply the
unrolling and exponentiation lemmas 255 times. This can be automated in Coq with
tacticals such as \coqDe{repeat}, but it generates a big proof object which
will take a long time to verify.
\subsubsection{Speeding up with Reflections}
In order to speed up the verification, we use a technique called reflection.
It provides us with flexibility such as we don't need to know the number of
times the lemmas needs to be applied.
The idea is to \textit{reflect} the goal into a decidable environment.
In our case, we show that for a property $P$, we can define a decidable
boolean property $P_{bool}$ such that if $P_{bool}$ is \coqDe{true} then $P$ holds.
$$P_{bool} = true \implies P$$
With VST we proved that \TNaCle{inv25519} in \texttt{Clight} is equivalent to its Coq
functional definition \coqDe{Inv25519}. We also proved that \coqDe{Inv25519}
over \coqDe{list Z} is equivalent to applying
\coqDe{Inv25519_Z} over \coqDe{Z}
% With VST we proved that \TNaCle{inv25519} in \texttt{Clight} is equivalent to its Coq
% functional definition \coqDe{Inv25519}. We also proved that \coqDe{pow_fn_rev}
% over \coqDe{list Z} is equivalent to applying
% \coqDe{pow_fn_rev_Z} over \coqDe{Z}
\begin{coqD}
Lemma pow_fn_rev_Z_GF :
forall (a:Z) (b:Z) (c:list Z) (g:list Z),
Zlength c = 16 ->
Zlength g = 16 ->
(Z16.lst (pow_fn_rev a b c g)) :GF =
(pow_fn_rev_Z a b (Z16.lst c) (Z16.lst g)) :GF .
Lemma Inv25519_Z_GF :
forall (g:list Z),
length g = 16 ->
(Z16.lst (Inv25519 g)) :GF =
(Inv25519_Z (Z16.lst g)) :GF.
\end{coqD}
where \coqDe{pow_fn_rev_Z} is defined in two parts: the application
(body of the for loop) and the loop itself.
% \begin{coqD}
% Lemma pow_fn_rev_Z_GF :
% forall (a:Z) (b:Z) (c:list Z) (g:list Z),
% Zlength c = 16 ->
% Zlength g = 16 ->
% (Z16.lst (pow_fn_rev a b c g)) :GF =
% (pow_fn_rev_Z a b (Z16.lst c) (Z16.lst g)) :GF .
% \end{coqD}
where \coqDe{Inv25519_Z} reproduces the same pattern as \coqDe{Inv25519}.
\begin{coqD}
Definition step_pow_Z (a:Z) (c:Z) (g:Z) :=
let c0 := c*c in
if a <>? 1 && a <>? 3
then c0*g
else c0.
Definition Inv25519_Z (x:Z) : Z :=
pow_fn_rev_Z 254 254 x x.
\end{coqD}
\coqDe{pow_fn_rev_Z} mimicks \coqDe{pow_fn_rev} over \coqDe{Z} instead of
\coqDe{list Z}. The structure is the same:
the application \coqDe{step_pow_Z} and the loop itself \coqDe{pow_fn_rev_Z}
\begin{coqD}
Definition step_pow_Z (a:Z) (c:Z) (g:Z) : Z :=
let c := c * c in
if a <>? 1 && a <>? 3
then c * g
else c.
Function pow_fn_rev_Z (a:Z) (b:Z) (c:Z) (g: Z)
{measure Z.to_nat a} : (Z) :=
{measure Z.to_nat a} : Z :=
if (a <=? 0)
then c
else
let prev := pow_fn_rev_Z (a - 1) b c g in
step_pow_Z (b - 1 - a) prev g.
\end{coqD}
We define the inversion modulo $2^{255}-19$ as an instance of \coqDe{pow_fn_rev_Z} where \coqDe{a} and \coqDe{b} are 254.
\begin{coqD}
Definition Inv25519_Z (x:Z) : Z :=
pow_fn_rev_Z 254 254 x x.
\end{coqD}
%
% In line with the definition of \coqDe{Inv25519}, we define the inversion modulo
% $2^{255}-19$ as an instance of \coqDe{pow_fn_rev_Z} where \coqDe{a} and \coqDe{b} are 254.
\subsubsection{A Simple Domain Specific Language}
{\red TODO: WHY $2^{255}-21$ ???}
To prove that the \coqDe{Inv25519_Z} is computing $x^{2^{255}-21}$,
we define a Domain Specific Language:
\begin{coqD}
......@@ -129,8 +189,8 @@ Fixpoint e_inv_denote (m:expr_inv) : Z :=
end.
\end{coqD}
We then defined \coqDe{step_inv} and \coqDe{pow_inv} to mirror the behavior of
\coqDe{step_pow_Z} and respectively \coqDe{pow_fn_rev_Z} over our new language.
We defined \coqDe{step_inv} and \coqDe{pow_inv} to mirror the behavior of
\coqDe{step_pow_Z} and respectively \coqDe{pow_fn_rev_Z} over our new domain.
\begin{coqD}
Lemma step_inv_step_pow_eq :
......@@ -167,11 +227,12 @@ f_inv_denote
\subsubsection{Deciding formulas}
In order to prove formulas, we define a decidable procedure.
In order to prove formulas in \coqDe{formula_inv},
we define a decidable procedure.
We first compute the power of each side of the formula and then check their
equality.
\begin{coqD}
Fixpoint pow_expr_inv (t : expr_inv) : Z :=
Fixpoint pow_expr_inv (t:expr_inv) : Z :=
match t with
| R_inv => 1
| M_inv x y =>
......@@ -182,15 +243,15 @@ Fixpoint pow_expr_inv (t : expr_inv) : Z :=
(Z.pos p) * (pow_expr_inv x)
end.
Definition decide_e_inv (l1 l2 : expr_inv) : bool :=
Definition decide_e_inv (l1 l2:expr_inv) : bool :=
(pow_expr_inv l1) ==? (pow_expr_inv l2).
Definition decide_f_inv (f : formula_inv) : bool :=
Definition decide_f_inv (f:formula_inv) : bool :=
match f with
| Eq_inv x y => decide_e_inv x y
end.
\end{coqD}
We proved that our procedure is correct: for all formulas, if
We proved that our procedure is correct: for all formulas in \coqDe{formula_inv}, if
\coqDe{decide_f_inv} returns \coqDe{true}, then the denoted equality is correct.
\begin{coqD}
Lemma decide_formula_inv_impl :
......@@ -203,10 +264,58 @@ By reification to our Domain Specific Language and then by applying
\texttt{decide\_formula\_inv\_impl} and computing \texttt{decide\_f\_inv},
we proved that \coqDe{Inv25519} is indeed computing an inverse in
modulo $2^{255}-19$.
\begin{coqD}
Theorem Inv25519_Z_correct :
forall (x:Z),
Inv25519_Z x = pow x (2^255-21).
\end{coqD}
{\red TODO: GIVE OTHER EXAMPLES WHERE REFLECTION IS APPLIED : e.g. PACK25519}
From \coqDe{Inv25519_Z_correct} and \coqDe{Inv25519_Z_GF}, we conclude the
functionnal correctness of the inversion over \Zfield.
\begin{coqD}
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{coqD}
\subsubsection{Packing and other applications}
Reflection can also be used where proofs requires computing.
\todo[inline]{give other examples where Reflection was applied, e.g. pack25519}
Pack25519 :
prove that the substraction and the carry can be seen as two separate loops instead of a single for.
This simplifies the proof as you just the carrying does not change the value in \Zfield.
Proving equalitives of the form:
\begin{coqD}
[x * y + z * t, x , y * r] =
[t * z + y * x, x , r * y].
\end{coqD}
This is usually solved with the repetition of the \coqDe{f_equal} lemma.
\begin{coqD}
Lemma f_equal :
forall (A B C:Type) (x y:A) (z t:B) (f:A->B->C),
x = y -> z = t ->
f x z = f y t.
\end{coqD}
In this example case it will create two subgoals:
\begin{coqD}
(* 1 *)
x * y + z * t = t * z + y * x
(* 2 *)
[x , y * r] = [x , r * y]
\end{coqD}
The first one will be proven by the \coqDe{ring} tactic which solve simple non-linear goals.
The second one will be proven by the application of \coqDe{f_equal}
followed by \coqDe{ring}. This iteration and call for tactics makes the proofs slow.
Instead of repeating this over the 16 or more elements of the lists, we used a reflection.
We created a decidable procedure over the elements of the list and iterated on them.
\section{Related Works}
\todo[inline]{Write write write}
\begin{itemize}
\item HACL*
\item Proving SHA-256 and HMAC
......
......@@ -79,4 +79,6 @@ Date: somewhen in 2018.}
\begin{appendix}
\end{appendix}
\listoftodos
\end{document}
......@@ -202,3 +202,4 @@
\newcommand{\PowMul}{{\text{\sf PowMul}}}
\newcommand{\PowMulPsi}{{\text{\sf PowMul}_{\psi}}}
\newcommand{\ie}{{\it i.e.}}
\newcommand{\Zfield}{\ensuremath{\mathbb{Z}_{2^{255}-19}}}
......@@ -38,7 +38,7 @@
\usepackage{xspace}
\usepackage{subfig}
\usepackage{float}
\usepackage{todonotes}
\usepackage[capitalise,nameinlink]{cleveref}
\floatstyle{ruled}
......@@ -49,6 +49,12 @@
\newcounter{subListing@save}
\renewcommand{\thesubListing}{\alph{subListing}}
\usepackage[framemethod=tikz]{mdframed}
\mdfsetup{leftmargin=0cm,skipabove=0.1cm,hidealllines=true,%
innerleftmargin=0.05cm,innerrightmargin=0.05cm,
innertopmargin=-0.10cm,innerbottommargin=-0.20cm,
skipbelow=-0.2cm}
\renewcommand{\tabcolsep}{4pt}
\def\subheading#1{\medskip\noindent{\boldmath\textbf{#1}}~\ignorespaces}
......@@ -111,6 +117,7 @@ width=0.8\columnwidth
morecomment=[l]{//},
identifierstyle=\color[rgb]{0,0,0},
delim=[s][\color{doc@lstdirective}]{(*}{*)},
backgroundcolor=\color{doc@lstbackground}, % set the background color
literate=
{=>}{{$\mapsto$}}1
{<}{{$\!<\!$}}1
......@@ -125,6 +132,12 @@ width=0.8\columnwidth
\def\VSTe{\lstinline[language=CoqVST, basicstyle=\ttfamily\normalsize]}
\def\VSTes{\lstinline[language=CoqVST, basicstyle=\scriptsize]}
\lstnewenvironment{CoqVST}{
\mdframed[backgroundcolor=doc@lstbackground]%
\lstset{language=CoqVST}}{
\endmdframed
}
%
% DEFINITION OF COQ PERSONNAL SYNTAX COLORING
......@@ -136,10 +149,11 @@ mathescape=true,
% Comments may or not include Latex commands
texcl=false,
% Vernacular commands
morekeywords=[1]{Definition, Fixpoint, Theorem, Qed, Function, Lemma, Notation,
Inductive, Variable},
morekeywords=[1]{Definition, Fixpoint, Theorem, Corollary, Qed, Function, Lemma,
Notation, Inductive, Variable},
morekeywords=[2]{list, Z, expr_inv, positive, formula_inv, bool, Prop, nat, T, Type},
morekeywords=[3]{forall, fun, match, end, with, measure, if, then, else, let, in},
morekeywords=[3]{forall, fun, match, end, with, measure, if, then, else, let, in,
ring},
morekeywords=[4]{Forall, ZofList, Zlength},
morekeywords=[5]{ 0, 1, 2, 3, 16, 32, 254, true},
sensitive=true,
......@@ -164,6 +178,7 @@ breaklines=false,
% basicstyle=\small,
% Position of captions is bottom
captionpos=b,
backgroundcolor=\color{doc@lstbackground}, % set the background color
% flexible columns
columns=[l]flexible,
literate=
......@@ -199,7 +214,11 @@ literate=
%
}[keywords,comments,strings]
\lstnewenvironment{coqD}{\lstset{language=CoqD}}{}
\lstnewenvironment{coqD}{
\mdframed[backgroundcolor=doc@lstbackground]%
\lstset{language=CoqD}}{
\endmdframed
}
% pour inliner dans le texte
\def\coqDe{\lstinline[language=CoqD, basicstyle=\ttfamily\normalsize]}
......@@ -363,7 +382,6 @@ literate=
%
identifierstyle=\color[rgb]{0,0,0},
delim=[l][\color{doc@lstdirective}]{\#},
backgroundcolor=\color{white}, % set the background color
literate=
}
......@@ -402,14 +420,14 @@ literate=
%
captionpos=b, % set the caption position to `bottom'
%
xleftmargin=0.4em, % text to the right
xrightmargin=0.4em, % text to the left
xleftmargin=0.2em, % text to the right
xrightmargin=0.2em, % text to the left
breaklines=false, % don't break long lines of code
%
frame=single, % add a frame around the code
framexleftmargin=0pt, % frame back to the left
framexrightmargin=0pt, % frame back to the right
backgroundcolor=\color{doc@lstbackground}, % set the background color
backgroundcolor=\color{white}, % set the background color
rulecolor=\color{doc@lstframe}, % frame color
%
columns=flexible, % try not to ruin the spacing intended by the font designer
......
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