Commit dc9fe4e1 by Benoit Viguier

### WIP

parent a88d3f80
 ... ... @@ -4,6 +4,106 @@ In this section we describe techniques used to prove the equivalence between the Clight description of TweetNaCl and Coq functions producing similar behaviors. \subsection{Correctness Specification} We show the soundness of TweetNaCl by proving the following specification matches a pure Coq function. This defines the equivalence between the Clight representation and a Coq definition of the ladder. \begin{CoqVST} Definition crypto_scalarmult_spec := DECLARE _crypto_scalarmult_curve25519_tweet WITH v_q: val, v_n: val, v_p: val, c121665:val, sh : share, q : list val, n : list Z, p : list Z (*------------------------------------------*) PRE [ _q OF (tptr tuchar), _n OF (tptr tuchar), _p OF (tptr tuchar) ] PROP (writable_share sh; Forall (fun x => 0 <= x < 2^8) p; Forall (fun x => 0 <= x < 2^8) n; Zlength q = 32; Zlength n = 32; Zlength p = 32) LOCAL(temp _q v_q; temp _n v_n; temp _p v_p; gvar __121665 c121665) SEP (sh [{ v_q }] <<(uch32)-- q; sh [{ v_n }] <<(uch32)-- mVI n; sh [{ v_p }] <<(uch32)-- mVI p; Ews [{ c121665 }] <<(lg16)-- mVI64 c_121665) (*------------------------------------------*) POST [ tint ] PROP (Forall (fun x => 0 <= x < 2^8) (CSM n p); Zlength (CSM n p) = 32) LOCAL(temp ret_temp (Vint Int.zero)) 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{CoqVST} 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 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}, \VSTe{v_q} and \VSTe{v_n}. \item[] \VSTe{SEP}: \VSTe{sh [{ v_p $\!\!\}\!\!]\!\!\!$ <<(uch32)-- mVI p}\\ In the memory share \texttt{sh}, the address \VSTe{v_p} points to a list of integer values \VSTe{mVI p}. \item[] \VSTe{PROP}: \VSTe{Forall (fun x => 0 <= x < 2^8) p}\\ In order to consider all the possible inputs, we assumed each elements of the list \texttt{p} to be bounded by $0$ included and $2^8$ excluded. \item[] \VSTe{PROP}: \VSTe{Zlength p = 32}\\ We also assumed that the length of the list \texttt{p} is 32. This defines the complete representation of \TNaCle{u8[32]}. \end{itemize} As Post-condition we have: \begin{itemize} \item[] \VSTe{POST}: \VSTe{tint}\\ The function \texttt{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)}\\ 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 result of the \VSTe{crypto_scalarmult} over \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]}. \end{itemize} This specification shows that \VSTe{crypto_scalarmult} in C computes the same result as \VSTe{CSM} in Coq provided that inputs are within their respective bounds. 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}) in Coq (for the sake of simplicity we do not display the conversion in the theorem). \begin{theorem} \label{CSM-correct} For all $n \in \N, n < 2^{255}$ and where the bits 1, 2, 5 248, 249, 250 are cleared and bit 6 is set, for all $P \in E(\F{p^2})$, for all $p \in \F{p}$ such that $P.x = p$, there exists $Q \in E(\F{p^2})$ such that $Q = nP$ where $Q.x = q$ and $q$ = \VSTe{CSM} $n$ $p$. \end{theorem} A more complete description in Coq of Theorem \ref{CSM-correct} with the associated conversions is as follow: \begin{lstlisting}[language=Coq] Theorem Crypto_Scalarmult_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 (ZUnpack25519 (ZofList 8 p)) = P#x0 -> ZofList 8 (Crypto_Scalarmult n p) = (P *+ (Z.to_nat (Zclamp (ZofList 8 n)))) _x0. \end{lstlisting} \subsection{Number Representation and C Implementation} As described in Section \ref{sec:impl}, numbers in \TNaCle{gf} are represented ... ...
 ... ... @@ -2,25 +2,20 @@ \label{preliminaries} \subsection{The X25519 key exchange} \F{p}, \F{p^2}, Coordinates, X-coordinates in \F{p}. XXX: math definition from Cure25519 paper. XXX: math definition from Curve25519 paper. \subsection{X25519 in TweetNaCl} \subheading{The Montgomery ladder} \todo{Ladder algorithm C code} \todo{Ladderstep algorithm C code} \subheading{Arithmetic in \Ffield} Given a natural number $n$ and a value $x \in \F{p}$, Curve25519 is a function over a $\F{p}$-restricted Given a natural number $n$ and a value $x \in \F{p}$, X25519 is a function over a $\F{p}$-restricted $x$-coordinate computing a scalar multiplication on $E(\F{p^2})$. As a result of this restriction, all computations are done over $\F{p}$. Numbers in that field can be represented with 256 bits. We represent them in 8-bit limbs (respectively 16-bit limbs), making use of a base $2^8$ (respectively $2^{16}$). Consequently, inputs of the Curve25519 function are seen as arrays of bytes. Consequently, inputs of the X25519 function are seen as arrays of bytes. Computations inside this function makes use of the 16-bit limbs representation. Those are placed into 64-bits signed container in order to mitigate overflows or underflows. \begin{lstlisting}[language=Ctweetnacl] ... ... @@ -32,8 +27,8 @@ $\exists x,y \in$ \TNaCle{gf} such that \vspace{-0.25cm} $$x \neq y\ \ \land\ \ x \equiv y \pmod{2^{255}-19}$$ On the other hand it allows simple definitions of addition (\texttt{A}), substraction (\texttt{Z}), and school-book multiplication (\texttt{M}). On the other hand it allows simple definitions of addition (\texttt{A}), substraction (\texttt{Z}), and school-book multiplication (\texttt{M}). % and squaring (\texttt{S}). \begin{lstlisting}[language=Ctweetnacl] sv A(gf o,const gf a,const gf b) { ... ... @@ -84,11 +79,15 @@ $\exists x,y \in$ \TNaCle{gf} such that % } % \end{lstlisting} At the end of the Montgomery ladder, \texttt{inv25519} computes the inverse over \Zfield. It uses Fermat's little theorem by the exponentiation to $2^{255}-21$ with the Square-and-multiply algorithm. Inverse in \Zfield are computed with \texttt{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$. % 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} The last step of \texttt{crypto\_scalarmult} is the packing of the limbs: an array of 32 bytes. It first performs 3 carry propagations in order to guarantee that each 16-bit limbs values are between $0$ and $2^{16}$. ... ... @@ -124,7 +123,7 @@ $\exists x,y \in$ \TNaCle{gf} such that } \end{lstlisting} The full Montgomery ladder is defined as follow. \subheading{The Montgomery ladder} The full ladder is defined as follow. First extract and clamp the value of $n$. Then unpack the value of $p$. Compute the Montgomery ladder over the clamped $n$ and $p$, pack the result into $q$. \begin{lstlisting}[language=Ctweetnacl] ... ... @@ -222,104 +221,3 @@ This garantees us the correctness of the implementation. \caption{Structural construction of the proof} \label{tk:ProofStructure} \end{figure} \subsection{Correctness Specification} We show the soundness of TweetNaCl by proving the following specification matches a pure Coq function. This defines the equivalence between the Clight representation and a Coq definition of the ladder. \begin{CoqVST} Definition crypto_scalarmult_spec := DECLARE _crypto_scalarmult_curve25519_tweet WITH v_q: val, v_n: val, v_p: val, c121665:val, sh : share, q : list val, n : list Z, p : list Z (*------------------------------------------*) PRE [ _q OF (tptr tuchar), _n OF (tptr tuchar), _p OF (tptr tuchar) ] PROP (writable_share sh; Forall (fun x => 0 <= x < 2^8) p; Forall (fun x => 0 <= x < 2^8) n; Zlength q = 32; Zlength n = 32; Zlength p = 32) LOCAL(temp _q v_q; temp _n v_n; temp _p v_p; gvar __121665 c121665) SEP (sh [{ v_q }] <<(uch32)-- q; sh [{ v_n }] <<(uch32)-- mVI n; sh [{ v_p }] <<(uch32)-- mVI p; Ews [{ c121665 }] <<(lg16)-- mVI64 c_121665) (*------------------------------------------*) POST [ tint ] PROP (Forall (fun x => 0 <= x < 2^8) (CSM n p); Zlength (CSM n p) = 32) LOCAL(temp ret_temp (Vint Int.zero)) 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{CoqVST} 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 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}, \VSTe{v_q} and \VSTe{v_n}. \item[] \VSTe{SEP}: \VSTe{sh [{ v_p $\!\!\}\!\!]\!\!\!$ <<(uch32)-- mVI p}\\ In the memory share \texttt{sh}, the address \VSTe{v_p} points to a list of integer values \VSTe{mVI p}. \item[] \VSTe{PROP}: \VSTe{Forall (fun x => 0 <= x < 2^8) p}\\ In order to consider all the possible inputs, we assumed each elements of the list \texttt{p} to be bounded by $0$ included and $2^8$ excluded. \item[] \VSTe{PROP}: \VSTe{Zlength p = 32}\\ We also assumed that the length of the list \texttt{p} is 32. This defines the complete representation of \TNaCle{u8[32]}. \end{itemize} As Post-condition we have: \begin{itemize} \item[] \VSTe{POST}: \VSTe{tint}\\ The function \texttt{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)}\\ 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 result of the \VSTe{crypto_scalarmult} over \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]}. \end{itemize} This specification shows that \VSTe{crypto_scalarmult} in C computes the same result as \VSTe{CSM} in Coq provided that inputs are within their respective bounds. 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}) in Coq (for the sake of simplicity we do not display the conversion in the theorem). \begin{theorem} \label{CSM-correct} For all $n \in \N, n < 2^{255}$ and where the bits 1, 2, 5 248, 249, 250 are cleared and bit 6 is set, for all $P \in E(\F{p^2})$, for all $p \in \F{p}$ such that $P.x = p$, there exists $Q \in E(\F{p^2})$ such that $Q = nP$ where $Q.x = q$ and $q$ = \VSTe{CSM} $n$ $p$. \end{theorem} A more complete description in Coq of Theorem \ref{CSM-correct} with the associated conversions is as follow: \begin{lstlisting}[language=Coq] Theorem Crypto_Scalarmult_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 (ZUnpack25519 (ZofList 8 p)) = P#x0 -> ZofList 8 (Crypto_Scalarmult n p) = (P *+ (Z.to_nat (Zclamp (ZofList 8 n)))) _x0. \end{lstlisting} % Its proof is explained in the next section.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!