Commit cbf1658b by Benoit Viguier

### more text

parent 5c754263
 ... ... @@ -4,26 +4,29 @@ In this section we present our formalization of RFC~7748~\cite{rfc7748}. \begin{informaltheorem} The specification of X25519 in RFC~7748 is formalized by \Coqe{ZCrypto_Scalarmult}. The specification of X25519 in RFC~7748 is formalized by \Coqe{RFC}. \end{informaltheorem} More precisely, we formalized X25519 with the following definition. \begin{coq} Definition ZCrypto_Scalarmult n p := \begin{lstlisting}[language=Coq] Definition RFC (n: list Z) (p: list Z) : list Z := let k := decodeScalar25519 n in let u := decodeUCoordinate p in let t := montgomery_rec 255 (* iterate 255 times *) (Zclamp n) (* clamped n *) k (* clamped n *) 1 (* x_2 *) (ZUnpack25519 p) (* x_3 *) u (* x_3 *) 0 (* z_2 *) 1 (* z_3 *) 0 (* dummy *) 0 (* dummy *) (ZUnpack25519 p) (* x_1 *) in u (* x_1 *) in let a := get_a t in let c := get_c t in ZPack25519 (Z.mul a (ZInv25519 c)). \end{coq} let o := ZPack25519 (Z.mul a (ZInv25519 c)) in encodeUCoordinate o. \end{lstlisting} We first present a generic description of the Montgomery ladder (\ref{subsec:spec-ladder}). Then we turn our attention to the different steps of the computation (\ref{subsec:spec-unpack-clamp-inv-pack}). ... ... @@ -64,6 +67,18 @@ We later prove our ladder correct in that respect (\sref{sec:maths}). \subsection{Unpacking, clamping, Inversion and Packing} \label{subsec:spec-unpack-clamp-inv-pack} \begin{lstlisting}[language=Coq] Definition decodeScalar25519 (l: list Z) : Z := ZofList 8 (clamp l). Definition decodeUCoordinate (l: list Z) : Z := ZofList 16 (Unpack25519 l). Definition encodeUCoordinate (x: Z) : list Z := ListofZ32 8 x. \end{lstlisting} Inputs of X25519 % \emph{To implement the X25519(k, u) and X448(k, u) functions (where k is % the scalar and u is the u-coordinate), first decode k and u and then ... ...
 ... ... @@ -3,10 +3,11 @@ In this section we prove the following theorem: % In this section we outline the structure of our proofs of the following theorem: \begin{informaltheorem} \label{thm:VST-RFC} The implementation of X25519 in TweetNaCl (\TNaCle{crypto_scalarmult}) matches the specifications of RFC~7748~\cite{rfc7748} (\Coqe{ZCrypto_Scalarmult}) the specifications of RFC~7748~\cite{rfc7748} (\Coqe{RFC}) \end{informaltheorem} More formally. ... ... @@ -27,10 +28,9 @@ used to in some of our more complex proofs (\ref{subsec:inversions-reflections}) \label{subsec:proof-structure} In order to prove the correctness of X25519 in TweetNaCl code \TNaCle{crypto_scalarmult}, we use VST to prove that the code matches our functional Coq specification of \Coqe{Crypto_Scalarmult} (to save space we sometimes abbreviate this as \Coqe{CSM}). 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} (\tref{thm:Elliptic-CSM}). we use VST to prove that the code matches our functional Coq specification of \Coqe{RFC}. 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} (\tref{thm:Elliptic-RFC}). \fref{tikz:ProofOverview} shows a graph of dependencies of the proofs. The mathematical proof of X25519 is presented in \sref{sec:maths}. \begin{figure}[h] ... ... @@ -111,7 +111,7 @@ a pure Coq function. % A pure function is a function where the return value is only determined by its % input values, without observable side effects (Side effect are e.g. printing) This defines the equivalence between the Clight representation and our Coq definition of the ladder (\coqe{CSM}). definition of the ladder (\coqe{RFC}). \begin{lstlisting}[language=CoqVST] Definition crypto_scalarmult_spec := ... ... @@ -137,10 +137,10 @@ SEP (sh [{ v_q }] <<(uch32)-- q; Ews [{ c121665 }] <<(lg16)-- mVI64 c_121665) (*------------------------------------------*) POST [ tint ] PROP (Forall (fun x => 0 <= x < 2^8) (CSM n p); Zlength (CSM n p) = 32) PROP (Forall (fun x => 0 <= x < 2^8) (RFC n p); Zlength (RFC n p) = 32) LOCAL(temp ret_temp (Vint Int.zero)) SEP (sh [{ v_q }] <<(uch32)-- mVI (CSM n p); SEP (sh [{ v_q }] <<(uch32)-- mVI (RFC n p); sh [{ v_n }] <<(uch32)-- mVI n; sh [{ v_p }] <<(uch32)-- mVI p; Ews [{ c121665 }] <<(lg16)-- mVI64 c_121665 ... ... @@ -172,22 +172,22 @@ As Post-condition we have: 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)}\\ \item[] \VSTe{SEP}: \VSTe{sh [{ v_q $\!\!\}\!\!]\!\!\!$ <<(uch32)-- mVI (RFC n p)}\\ In the memory share \texttt{sh}, the address \VSTe{v_q} points to a list of integer values \VSTe{mVI (CSM n p)} where \VSTe{CSM 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}. \item[] \VSTe{PROP}: \VSTe{Forall (fun x => 0 <= x < 2^8) (CSM n p)}\\ \VSTe{PROP}: \VSTe{Zlength (CSM n p) = 32}\\ We show that the computation for \VSTe{CSM} fits in \TNaCle{u8[32]}. \item[] \VSTe{PROP}: \VSTe{Forall (fun x => 0 <= x < 2^8) (RFC n p)}\\ \VSTe{PROP}: \VSTe{Zlength (RFC n p) = 32}\\ We show that the computation for \VSTe{RFC} fits in \TNaCle{u8[32]}. \end{itemize} 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 result as \VSTe{RFC} in Coq provided that inputs are within their respective bounds: arrays of 32 bytes. \begin{theorem} \label{thm:crypto-vst} \TNaCle{crypto_scalarmult} in TweetNaCl has the same behavior as \coqe{Crypto_Scalarmult} in Coq. \TNaCle{crypto_scalarmult} in TweetNaCl has the same behavior as \coqe{RFC} in Coq. \end{theorem} ... ... @@ -278,7 +278,7 @@ and without returns the same result. We formalized this result in a generic way in Appendix~\ref{subsubsec:for}. Using this formalization, we prove that the 255 steps of the Montgomery ladder in C provide the same computations as in \coqe{CSM}. in C provide the same computations as in \coqe{RFC}. ... ... @@ -645,22 +645,22 @@ By proving that each functions \coqe{Low.M}; \coqe{Low.A}; \coqe{Low.Sq}; \coqe{ \coqe{Unpack25519}; \coqe{clamp}; \coqe{Pack25519}; \coqe{car25519} are behaving over \coqe{list Z} as their equivalent over \coqe{Z} in \coqe{:GF} (in \Zfield), we prove the 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: \begin{lstlisting}[language=Coq] Theorem Crypto_Scalarmult_Eq : forall (n p:list Z), Zlength n = 32 -> Zlength p = 32 -> Forall (fun x : Z, 0 <= x /\ x < 2 ^ 8) n -> Forall (fun x : Z, 0 <= x /\ x < 2 ^ 8) p -> ZofList 8 (Crypto_Scalarmult n p) = ZCrypto_Scalarmult (ZofList 8 n) (ZofList 8 p). \end{lstlisting} % \begin{theorem} % \label{thm:crypto-rfc} % \coqe{Crypto_Scalarmult} matches the specification of RFC~7748. % \end{theorem} % This is formalized as follows in Coq: % \begin{lstlisting}[language=Coq] % Theorem Crypto_Scalarmult_Eq : % forall (n p:list Z), % Zlength n = 32 -> % Zlength p = 32 -> % Forall (fun x : Z, 0 <= x /\ x < 2 ^ 8) n -> % Forall (fun x : Z, 0 <= x /\ x < 2 ^ 8) p -> % ZofList 8 (Crypto_Scalarmult n p) = % ZCrypto_Scalarmult (ZofList 8 n) (ZofList 8 p). % \end{lstlisting} 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}). ... ...
 ... ... @@ -2,12 +2,26 @@ \label{sec:maths} In this section we prove the following theorem: \begin{theorem} \label{thm:Elliptic-CSM} \begin{informaltheorem} \label{thm:Elliptic-RFC} The implementation of X25519 in TweetNaCl (\TNaCle{crypto_scalarmult}) computes the $\F{p}$-restricted $x$-coordinate scalar multiplication on $E(\F{p^2})$ where $p$ is $\p$ and $E$ is the elliptic curve $y^2 = x^3 + 486662 x^2 + x$. \end{theorem} \end{informaltheorem} More formally: \begin{lstlisting}[language=Coq] Theorem RFC_Correct: forall (n p : list Z) (P:mc curve25519_Fp2_mcuType), Zlength n = 32 -> Zlength p = 32 -> Forall (fun x => 0 <= x /\ x < 2 ^ 8) n -> Forall (fun x => 0 <= x /\ x < 2 ^ 8) p -> Fp2_x (decodeUCoordinate p) = P#x0 -> RFC n p = encodeUCoordinate ((P *+ (Z.to_nat (decodeScalar25519 n))) _x0). \end{lstlisting} We first review the work of Bartzia and Strub \cite{BartziaS14} (\ref{subsec:ECC-Weierstrass}). We extend it to support Montgomery curves (\ref{subsec:ECC-Montgomery}) ... ... @@ -414,7 +428,8 @@ we can find a $y$ such that $(x,y)$ is either on the curve or on the quadratic t over $M_{486662,2}(\F{p})$ such that the $x$-coordinate of $P$ is $x$. \end{lemma} \begin{lstlisting}[language=Coq] Theorem x_is_on_curve_or_twist: forall x : Zmodp.type, Theorem x_is_on_curve_or_twist: forall x : Zmodp.type, (exists (p : mc curve25519_mcuType), p#x0 = x) \/ (exists (p' : mc twist25519_mcuType), p'#x0 = x). \end{lstlisting} ... ... @@ -430,22 +445,22 @@ Module Zmodp2. Inductive type := Zmodp2 (x: Zmodp.type) (y:Zmodp.type). Definition pi (x : Zmodp.type * Zmodp.type) : type := Definition pi (x: Zmodp.type * Zmodp.type) : type := Zmodp2 x.1 x.2. Coercion repr (x : type) : Zmodp.type*Zmodp.type := Coercion repr (x: type) : Zmodp.type*Zmodp.type := let: Zmodp2 u v := x in (u, v). Definition zero : type := pi ( 0%:R, 0%:R ). Definition one : type := pi ( 1, 0%:R ). Definition opp (x : type) : type := Definition opp (x: type) : type := pi (- x.1 , - x.2). Definition add (x y : type) : type := Definition add (x y: type) : type := pi (x.1 + y.1, x.2 + y.2). Definition sub (x y : type) : type := Definition sub (x y: type) : type := pi (x.1 - y.1, x.2 - y.2). Definition mul (x y : type) : type := Definition mul (x y: type) : type := pi ((x.1 * y.1) + (2%:R * (x.2 * y.2)), (x.1 * y.2) + (x.2 * y.1)). \end{lstlisting} ... ... @@ -556,16 +571,4 @@ Lemma ZCrypto_Scalarmult_curve25519_ladder: \end{lstlisting} From \tref{thm:RFC} and \tref{thm:general-scalarmult}, we prove the correctness of \TNaCle{crypto_scalarmult} (\tref{thm:Elliptic-CSM}). \begin{lstlisting}[language=Coq] Theorem Crypto_Scalarmult_Correct: forall (n:list Z) (p:list Z) (P:mc curve25519_Fp2_mcuType), Zlength n = 32 -> Zlength p = 32 -> Forall (fun x => 0 <= x /\ x < 2^8) n -> Forall (fun x => 0 <= x /\ x < 2^8) p -> Fp2_x (ZUnpack25519 (ZofList 8 p)) = P#x0 -> ZofList 8 (Crypto_Scalarmult n p) = (P *+ (Z.to_nat (Zclamp (ZofList 8 n)))) _x0. \end{lstlisting} of \TNaCle{crypto_scalarmult} (\tref{thm:Elliptic-RFC}).
 ... ... @@ -77,8 +77,8 @@ match t with end. \end{lstlisting} \subsubsection{ZCrypto\_Scalarmult} \label{subsubsec:ZCryptoScalarmult} \subsubsection{RFC in Coq} \label{subsubsec:RFC-Coq} ~ Instantiation of the Class \Coqe{Ops} with operations over \Z and modulo \p. \begin{lstlisting}[language=Coq] ... ... @@ -152,21 +152,33 @@ Proof. apply Mid.getbit. (* instantiate ith bit *) Defined. Definition decodeScalar25519 (l: list Z) : Z := ZofList 8 (clamp l). Definition decodeUCoordinate (l: list Z) : Z := ZofList 16 (Unpack25519 l). Definition encodeUCoordinate (x: Z) : list Z := ListofZ32 8 x. (* instantiate montgomery_rec with Z_Ops *) Definition ZCrypto_Scalarmult n p := Definition RFC (n: list Z) (p: list Z) : list Z := let k := decodeScalar25519 n in let u := decodeUCoordinate p in let t := montgomery_rec 255 (* iterate 255 times *) (Zclamp n) (* clamped n *) k (* clamped n *) 1 (* x_2 *) (ZUnpack25519 p) (* x_3 *) u (* x_3 *) 0 (* z_2 *) 1 (* z_3 *) 0 (* dummy *) 0 (* dummy *) (ZUnpack25519 p) (* x_1 *) in u (* x_1 *) in let a := get_a t in let c := get_c t in ZPack25519 (Z.mul a (ZInv25519 c)). let o := ZPack25519 (Z.mul a (ZInv25519 c)) in encodeUCoordinate o. \end{lstlisting} \subsubsection{CSM} ... ...
 ... ... @@ -8,8 +8,27 @@ preaction = {decorate}, postaction = {draw,line width=1.4pt, white,shorten >= 4.5pt}] \path [thick, dashed] (2.5,1) edge +(0,-6.75); \draw (2.5,1) node[anchor=north east] {\sref{sec:Coq-RFC}}; \draw (2.5,1) node[anchor=north west] {\sref{sec:C-Coq}}; \path [thick, dashed] (0,-5.75) edge +(8.5,0); \draw (8.5,-5.75) node[anchor=north east] {\sref{sec:maths}}; % SECTION III % Definition of RFC \begin{scope}[yshift=-3 cm,xshift=0 cm] \draw (0,0) -- (0.4, 0.4) -- (1.75,0.4) -- (1.75,0) -- cycle; \draw (0,0) -- (1.75,0) -- (1.75,-1) -- (0, -1) -- cycle; \draw (0.3,-0.05) node[textstyle] {Definition}; \draw (0.875,-0.5) node[textstyle, anchor=center] {\texttt{RFC}}; \draw (1.75,-1) node[textstyle, anchor = south east] {\color{doc@lstfunctions}{.V}}; \end{scope} % SECTION IV % C code \begin{scope}[yshift=0 cm,xshift=0 cm] \begin{scope}[yshift=-0.25 cm,xshift=3 cm] \draw (0,0) -- (0.4, 0.4) -- (1.25,0.4) -- (1.25,0) -- cycle; \draw (0,0) -- (1.25,0) -- (1.25,-1.25) -- (0, -1.25) -- cycle; \draw (0.3,-0.05) node[textstyle] {code}; ... ... @@ -17,9 +36,8 @@ \draw (1.25,-1.25) node[textstyle, anchor = south east] {\color{doc@lstfunctions}{.C}}; \end{scope} % V code \begin{scope}[yshift=0 cm,xshift=2.5 cm] \begin{scope}[yshift=-0.25 cm,xshift=5 cm] \draw (0,0) -- (0.4, 0.4) -- (1.25,0.4) -- (1.25,0) -- cycle; \draw (0,0) -- (1.25,0) -- (1.25,-1.25) -- (0, -1.25) -- cycle; \draw (0.3,-0.05) node[textstyle] {code}; ... ... @@ -28,61 +46,63 @@ % \draw (1.25,0) node[anchor=south east, inner sep=0pt] {\includegraphics[width=.0125\textwidth]{img/coq_logo.png}}; \end{scope} % VST Theorem \begin{scope}[yshift=0 cm,xshift=6 cm] \draw (0,0) -- (0.4, 0.4) -- (2.5,0.4) -- (2.5,0) -- cycle; \draw (0,0) -- (2.5,0) -- (2.5,-1.25) -- (0, -1.25) -- cycle; \draw (0.3,-0.05) node[textstyle] {Proof}; \draw (1.25,-0.5) node[textstyle, anchor=center] {\{{\color{doc@lstnumbers}\textbf{Pre}}\} \texttt{Prog} \{{\color{doc@lstdirective}\textbf{Post}}\}}; \draw (2.5,-1.25) node[textstyle, anchor = south east] {\color{doc@lstfunctions}{\checkmark}}; \end{scope} \path [thick, double, ->] (4.25,-0.75) edge (5, -0.75); % VST Spec \begin{scope}[yshift=-2.5 cm,xshift=3 cm] \begin{scope}[yshift=-3 cm,xshift=3 cm] \draw (0,0) -- (0.4, 0.4) -- (2,0.4) -- (2,0) -- cycle; \draw (0,0) -- (2,0) -- (2,-2) -- (0, -2) -- cycle; \draw (0.3,-0.05) node[textstyle] {Specification}; \draw (1,-1) node[textstyle, anchor=center, align=left] { {\color{doc@lstnumbers}\textbf{Pre}}:\\ ~~$n \in \N$,\\ % ~~$n \in$ \TNaCles{u8[32]},\\ ~~$P \in E(\F{p^2})$\\ % ~~$P \in$ \TNaCles{u8[32]}\\ {\color{doc@lstdirective}\textbf{Post}}:\\ ~~\texttt{CSM}$(n,P)$}; ~~\texttt{RFC}$(n,P)$}; \end{scope} % Definition of CSM \begin{scope}[yshift=-4.5 cm,xshift=0 cm] \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] {\texttt{CSM}}; % VST Theorem \begin{scope}[yshift=-3 cm,xshift=6 cm] \draw (0,0) -- (0.4, 0.4) -- (2.5,0.4) -- (2.5,0) -- cycle; \draw (0,0) -- (2.5,0) -- (2.5,-1.25) -- (0, -1.25) -- cycle; \draw (0.3,-0.05) node[textstyle] {Proof}; \draw (1.25,-0.5) node[textstyle, anchor=center] {\{{\color{doc@lstnumbers}\textbf{Pre}}\} \texttt{Prog} \{{\color{doc@lstdirective}\textbf{Post}}\}}; \draw (2.5,-1.25) node[textstyle, anchor = south east] {\color{doc@lstfunctions}{\checkmark}}; \end{scope} \path [thick, double] (5.625,-1.5) edge [out=-90, in=90] (5.625, -2.5); \path [thick, double, ->] (5.625, -2.5) edge [out=-90, in=180] (6, -3.5); \path [thick, double, ->] (5,-3.75) edge [out=0, in=180] (6, -3.75); % SECTION V % Spec of Curve nP \begin{scope}[yshift=-7.5 cm,xshift=0 cm] \draw (0,0) -- (0.4, 0.4) -- (2,0.4) -- (2,0) -- cycle; \draw (0,0) -- (2,0) -- (2,-1) -- (0, -1) -- cycle; \begin{scope}[yshift=-7.25 cm,xshift=0 cm] \draw (0,0) -- (0.4, 0.4) -- (1.75,0.4) -- (1.75,0) -- cycle; \draw (0,0) -- (1.75,0) -- (1.75,-1) -- (0, -1) -- cycle; \draw (0.3,-0.05) node[textstyle] {Definition}; \draw (1,-0.5) node[textstyle, anchor=center] {$n \cdot P$}; \draw (0.875,-0.5) node[textstyle, anchor=center] {$n \cdot P$}; \end{scope} % Correctness Theorem \begin{scope}[yshift=-7 cm,xshift=6 cm] \begin{scope}[yshift=-6.75 cm,xshift=6 cm] \draw (0,0) -- (0.4, 0.4) -- (2.5,0.4) -- (2.5,0) -- cycle; \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 \cdot P$}; \draw (1.25,-0.75) node[textstyle, anchor=center] {{\color{doc@lstnumbers}\textbf{Pre}} $\implies$\\$\text{\texttt{RFC}}(n,P) = n \cdot P$}; \end{scope} \path [thick, double, ->] (1.25,-0.5) edge (2.5, -0.5); \path [thick, double, ->] (3.75,-0.5) edge (6, -0.5); \path [thick, double, ->] (5,-3.5) edge [out=0, in=-90] (6.5, -1.25); \path [thick, double, ->] (2,-5) edge [out=0, in=-180] (3, -3.5); \path [thick, double, ->] (2,-5) edge [out=0, in=-180] (6, -7.5); \path [thick, double, ->] (2,-8) edge [out=0, in=-180] (6, -8); \path [thick, double, ->] (1.75,-3.5) edge [out=0, in=-180] (3, -3.5); \path [thick, double] (1.75,-3.5) edge [out=0, in=90] (2.25, -4); \path [thick, double] (2.25, -4) edge [out=-90, in=90] (2.25, -6.75); \path [thick, double] (2.25, -6.75) edge [out=-90, in=-180] (3, -7.5); \path [thick, double, ->] (3, -7.5) edge [out=0, in=-180] (6, -7.5); \path [thick, double, ->] (1.75,-7.75) edge [out=0, in=-180] (6, -7.75); \path [thick, dashed] (0,-5.75) edge +(8.5,0); \draw (8.5,-5.75) node[anchor=south east] {\sref{sec:C-Coq-RFC}}; \draw (8.5,-5.75) node[anchor=north east] {\sref{sec:maths}}; \end{tikzpicture}
 ... ... @@ -67,8 +67,6 @@ Require Import Tweetnacl_verif.verif_crypto_scalarmult_lemmas. Require Import Tweetnacl.Low.Get_abcdef. Require Import Tweetnacl.Low.ScalarMult_rev. Require Import Tweetnacl.Low.Constant. (* Require Import Tweetnacl.Low.Crypto_Scalarmult. *) (* Require Import Tweetnacl.Low.Crypto_Scalarmult_. *) Require Import Tweetnacl.Mid.Instances. Require Import Tweetnacl.rfc.rfc. Open Scope Z. ... ...
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!