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

more test

parent e15af18b
...@@ -78,13 +78,13 @@ match m with ...@@ -78,13 +78,13 @@ match m with
end. end.
\end{lstlisting} \end{lstlisting}
RFC~7748 states \emph{``All calculations are performed in GF(p), i.e., they are performed modulo p.''}. RFC~7748 states \emph{``All calculations are performed in GF(p), i.e., they are performed modulo p.''}
Operations used in the Montgomery ladder of \coqe{RFC} are intentiated over Operations used in the Montgomery ladder of \coqe{RFC} are intentiated over
integers $Z$ (See Appendix~\ref{subsubsec:RFC-Coq}). The modulo reduction by $\p$ integers $Z$ (See Appendix~\ref{subsubsec:RFC-Coq}). The modulo reduction by $\p$
is deferred at the end with the \coqe{ZPack25519} operation. is deferred at the end with the \coqe{ZPack25519} operation.
We define $\Zfield$ as the field of integers where the modulo reduction by $\p$ is We define $\Zfield$ as the field of integers where the modulo reduction by $\p$ is
deferred at the end of the computations. deferred at the end of the computations.
This aims to formalize its difference with $\Ffield$ where the We use this notation to emphasis its difference with $\Ffield$ where the
modulo by $\p$ is applied in each operations. modulo by $\p$ is applied in each operations.
We first present a generic description of the Montgomery ladder (\ref{subsec:spec-ladder}). We first present a generic description of the Montgomery ladder (\ref{subsec:spec-ladder}).
...@@ -111,7 +111,7 @@ the definition of RFC~7748 are provided in Appendix~\ref{subsubsec:coq-ladder}. ...@@ -111,7 +111,7 @@ the definition of RFC~7748 are provided in Appendix~\ref{subsubsec:coq-ladder}.
Our formalization differs slightly from the RFC. Indeed in order to optimize the Our formalization differs slightly from the RFC. Indeed in order to optimize the
number of calls to \texttt{CSWAP} the RFC uses an additional variable to decide number of calls to \texttt{CSWAP} the RFC uses an additional variable to decide
whether a conditionnal swap is required or not. Our description of the ladder whether a conditional swap is required or not. Our description of the ladder
follows strictly the shape of the exponent as described in \aref{alg:montgomery-ladder}. follows strictly the shape of the exponent as described in \aref{alg:montgomery-ladder}.
This divergence is allowed by the RFC: This divergence is allowed by the RFC:
\emph{``Note that these formulas are slightly different from Montgomery's \emph{``Note that these formulas are slightly different from Montgomery's
......
...@@ -16,11 +16,11 @@ Theorem body_crypto_scalarmult: ...@@ -16,11 +16,11 @@ Theorem body_crypto_scalarmult:
semax_body semax_body
(* Clight translation of TweetNaCl. *) (* Clight translation of TweetNaCl. *)
Vprog Vprog
(* Hoare tripples for fct calls. *) (* Hoare triples for fct calls. *)
Gprog Gprog
(* fct we verify. *) (* fct we verify. *)
f_crypto_scalarmult_curve25519_tweet f_crypto_scalarmult_curve25519_tweet
(* Our Hoare tripple, see below. *) (* Our Hoare triple, see below. *)
crypto_scalarmult_spec. crypto_scalarmult_spec.
\end{lstlisting} \end{lstlisting}
...@@ -186,7 +186,7 @@ As Post-condition we have: ...@@ -186,7 +186,7 @@ As Post-condition we have:
\item[] \VSTe{SEP}: \VSTe{sh [{ v_q $\!\!\}\!\!]\!\!\!$ <<(uch32)-- mVI (RFC n p)}\\ \item[] \VSTe{SEP}: \VSTe{sh [{ v_q $\!\!\}\!\!]\!\!\!$ <<(uch32)-- mVI (RFC n p)}\\
In the memory share \texttt{sh}, the address \VSTe{v_q} points In the memory share \texttt{sh}, the address \VSTe{v_q} points
to a list of integer values \VSTe{mVI (RFC n p)} where \VSTe{RFC n p} is the to a list of integer values \VSTe{mVI (RFC n p)} where \VSTe{RFC n p} is the
result of the \VSTe{crypto_scalarmult} of \VSTe{n} and \VSTe{p}. result of the \TNaCle{crypto_scalarmult} of \VSTe{n} and \VSTe{p}.
\item[] \VSTe{PROP}: \VSTe{Forall (fun x => 0 <= x < 2^8) (RFC n p)}\\ \item[] \VSTe{PROP}: \VSTe{Forall (fun x => 0 <= x < 2^8) (RFC n p)}\\
\VSTe{PROP}: \VSTe{Zlength (RFC n p) = 32}\\ \VSTe{PROP}: \VSTe{Zlength (RFC n p) = 32}\\
We show that the computation for \VSTe{RFC} fits in \TNaCle{u8[32]}. We show that the computation for \VSTe{RFC} fits in \TNaCle{u8[32]}.
...@@ -196,6 +196,9 @@ This specification (proven with VST) shows that \TNaCle{crypto_scalarmult} in C ...@@ -196,6 +196,9 @@ This specification (proven with VST) shows that \TNaCle{crypto_scalarmult} in C
computes the same result as \VSTe{RFC} in Coq provided that inputs are within computes the same result as \VSTe{RFC} in Coq provided that inputs are within
their respective bounds: arrays of 32 bytes. their respective bounds: arrays of 32 bytes.
The correctness of this specification is formally proven in Coq with
\coqe{Theorem body_crypto_scalarmult}.
% \begin{theorem} % \begin{theorem}
% \label{thm:crypto-vst} % \label{thm:crypto-vst}
% \TNaCle{crypto_scalarmult} in TweetNaCl has the same behavior as \coqe{RFC} in Coq. % \TNaCle{crypto_scalarmult} in TweetNaCl has the same behavior as \coqe{RFC} in Coq.
...@@ -312,8 +315,8 @@ To facilitate working in $\Zfield$, we define the \coqe{:GF} notation. ...@@ -312,8 +315,8 @@ To facilitate working in $\Zfield$, we define the \coqe{:GF} notation.
\begin{lstlisting}[language=Coq] \begin{lstlisting}[language=Coq]
Notation "A :GF" := (A mod (2^255-19)). Notation "A :GF" := (A mod (2^255-19)).
\end{lstlisting} \end{lstlisting}
Later in \sref{sec:maths}, we formally define $\Ffield$. Later in \sref{subsec:Zmodp}, we formally define $\Ffield$.
Equivalence between operations 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} replicate the computations and steps done in C.
...@@ -641,31 +644,22 @@ Lemma Pack25519_mod_25519 : ...@@ -641,31 +644,22 @@ Lemma Pack25519_mod_25519 :
(Z16.lst l) mod (2^255-19). (Z16.lst l) mod (2^255-19).
\end{lstlisting} \end{lstlisting}
\todo{FINALIZE CONCLUSION HERE} By using each functions \coqe{Low.M}; \coqe{Low.A}; \coqe{Low.Sq}; \coqe{Low.Zub};
\coqe{Unpack25519}; \coqe{clamp}; \coqe{Pack25519}; \coqe{Inv25519}; \coqe{car25519}; \coqe{montgomery_rec},
we defined a Coq definition \coqe{Crypto_Scalarmult} mimicking the exact behavior of X25519 in TweetNaCl.
By proving that each functions \coqe{Low.M}; \coqe{Low.A}; \coqe{Low.Sq}; \coqe{Low.Zub}; 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} \coqe{Unpack25519}; \coqe{clamp}; \coqe{Pack25519}; \coqe{Inv25519}; \coqe{car25519} are behaving over \coqe{list Z}
as their equivalent over \coqe{Z} in \coqe{:GF} (in \Zfield), we prove the as their equivalent over \coqe{Z} in \coqe{:GF} (in \Zfield), we prove that given the same inputs \coqe{Crypto_Scalarmult} applies the same computation as \coqe{RFC}.
correctness of
% \begin{theorem}
% \label{thm:crypto-rfc}
% \coqe{Crypto_Scalarmult} matches the specification of RFC~7748.
% \end{theorem}
% This is formalized as follows in Coq: % This is formalized as follows in Coq:
% \begin{lstlisting}[language=Coq] \begin{lstlisting}[language=Coq]
% Theorem Crypto_Scalarmult_Eq : Lemma Crypto_Scalarmult_RFC_eq :
% forall (n p:list Z), forall (n: list Z) (p: list Z),
% Zlength n = 32 -> Zlength n = 32 ->
% Zlength p = 32 -> Zlength p = 32 ->
% Forall (fun x : Z, 0 <= x /\ x < 2 ^ 8) n -> Forall (fun x => 0 <= x /\ x < 2 ^ 8) n ->
% Forall (fun x : Z, 0 <= x /\ x < 2 ^ 8) p -> Forall (fun x => 0 <= x /\ x < 2 ^ 8) p ->
% ZofList 8 (Crypto_Scalarmult n p) = Crypto_Scalarmult n p = RFC n p.
% ZCrypto_Scalarmult (ZofList 8 n) (ZofList 8 p). \end{lstlisting}
% \end{lstlisting}
This proves that TweetNaCl's X25519 implementation respect RFC~7748.
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}).
...@@ -353,6 +353,7 @@ We first study Curve25519 and one of the quadratic twist Twist25519, both define ...@@ -353,6 +353,7 @@ We first study Curve25519 and one of the quadratic twist Twist25519, both define
over \F{p}. over \F{p}.
\subsubsection{Curves and Twists} \subsubsection{Curves and Twists}
\label{subsec:Zmodp}
We define $\F{p}$ as the numbers between $0$ and $p = \p$. We define $\F{p}$ as the numbers between $0$ and $p = \p$.
We create a \coqe{Zmodp} module to encapsulate those definitions. We create a \coqe{Zmodp} module to encapsulate those definitions.
...@@ -558,11 +559,8 @@ Theorem curve25519_Fp2_ladder_ok: ...@@ -558,11 +559,8 @@ Theorem curve25519_Fp2_ladder_ok:
curve25519_Fp_ladder n x = (p *+ n)#x0 /p. curve25519_Fp_ladder n x = (p *+ n)#x0 /p.
\end{lstlisting} \end{lstlisting}
\todo{FINALIZE / CONCLUDE HERE} We then prove the equivalence between of operations in $\Ffield$ and $\Zfield$,
in other words between \coqe{Zmodp} and \coqe{:GF}.
We then prove the equivalence between of operations over \coqe{Zmodp} and \coqe{:GF} (seen as \Zfield).
This allows us to show that given a clamped value $n$ and normalized $x$-coordinate of $P$, This allows us to show that given a clamped value $n$ and normalized $x$-coordinate of $P$,
$Curve25519\_Fp$ is equivalent to RFC~7748~\cite{rfc7748}. \coqe{RFC} gives the same results as $Curve25519\_Fp$.
This proves the correctness of TweetNaCl's X25519 and RFC~7748.
From \tref{thm:RFC} and \tref{thm:general-scalarmult}, we prove the correctness
of \TNaCle{crypto_scalarmult} (\tref{thm:Elliptic-RFC}).
...@@ -76,11 +76,11 @@ does not impact the trust of our proof. ...@@ -76,11 +76,11 @@ does not impact the trust of our proof.
\subheading{A complete proof.} \subheading{A complete proof.}
\todo{REWRITE} We provide a mechanized formal proof of the correctness of the X25519
implementation in TweetNaCl.
We provide a mechanized formal proof of the correctness of the X25519 implementation in TweetNaCl. We first formalized X25519 from RFC~7748~\cite{rfc7748} in Coq. Then we proved
We first proved that TweetNaCl's implementation of X25519 matches RFC~7748 (\tref{thm:VST-RFC}). that TweetNaCl's implementation of X25519 matches our formalization.
In a second step we extended the Coq library for elliptic curves \cite{BartziaS14} In a second step we extended the Coq library for elliptic curves \cite{BartziaS14}
by Bartzia and Strub to support Montgomery curves. Using this extension we by Bartzia and Strub to support Montgomery curves. Using this extension we
proved that the X25519 implementation in TweetNaCl matches the mathematical proved that the X25519 from the RFC and its implementation in TweetNaCl matches
definitions as given in~\cite[Sec.~2]{Ber06} (\tref{thm:Elliptic-CSM}). the mathematical definitions as given in~\cite[Sec.~2]{Ber06} (\tref{thm:Elliptic-CSM}).
...@@ -94,7 +94,7 @@ We provide below the location of the most important definitions and lemmas of ou ...@@ -94,7 +94,7 @@ We provide below the location of the most important definitions and lemmas of ou
\multicolumn{3}{c}{Instanciations of \texttt{Ops}}\\ \multicolumn{3}{c}{Instanciations of \texttt{Ops}}\\
\hline \hline
\texttt{Z25519\_Ops} & \texttt{Mid/Instances.v} & Instanciations over \F{p} with $p = \p$\\ \texttt{Z25519\_Ops} & \texttt{Mid/Instances.v} & Instanciations over \F{p} with $p = \p$\\
\texttt{Z\_Ops} & \texttt{Mid/Instances.v} & Instanciations over \Z \\ \texttt{Z\_Ops} & \texttt{Mid/Instances.v} & Instanciations over $\Zfield$ \\
\texttt{List\_Z\_Ops} & \texttt{Mid/Instances.v} & Instanciations lists of \Z \\ \texttt{List\_Z\_Ops} & \texttt{Mid/Instances.v} & Instanciations lists of \Z \\
\hline \hline
\multicolumn{3}{c}{X25519 over \Z and list of \Z}\\ \multicolumn{3}{c}{X25519 over \Z and list of \Z}\\
......
...@@ -168,7 +168,7 @@ morekeywords=[5]{by, done, exact, reflexivity, tauto, romega, omega, ...@@ -168,7 +168,7 @@ morekeywords=[5]{by, done, exact, reflexivity, tauto, romega, omega,
morekeywords=[6]{do, last, first, try, idtac, repeat}, morekeywords=[6]{do, last, first, try, idtac, repeat},
% %
% Control % Control
% morekeywords=[7]{Forall, ZofList, Zlength, length, ListofZ32}, morekeywords=[7]{Forall, ZofList, Zlength, length, ListofZ32},
% %
% Comments delimiters, we do turn this off for the manual % Comments delimiters, we do turn this off for the manual
morecomment=[s]{(*}{*)}, morecomment=[s]{(*}{*)},
......
Markdown is supported
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