Commit 08b93818 by Benoit Viguier

### WIP

parent 294aac6e
 ... ... @@ -40,11 +40,12 @@ $(X : Z)$, with $x = X/Z$; the point at infinity is represented as $(1:0)$. See \sref{subsec:ECC-projective} for more details. We define the opperation: \begin{align*} \texttt{xladderstep} &: (x_{Q-P}, (X_P:Z_P), (X_Q:Z_Q)) \mapsto \\ \texttt{xDBL\&ADD} &: (x_{Q-P}, (X_P:Z_P), (X_Q:Z_Q)) \mapsto \\ &((X_{2 \cdot P}:Z_{2 \cdot P}), (X_{P + Q}:Z_{P + Q})) \end{align*} In the Montgomery ladder, % notice that the arguments of \texttt{xADD} and \texttt{xDBL} % the arguments of \texttt{xADD} and \texttt{xDBL} the arguments $P$ and $Q$ of \texttt{xDBL\&ADD} are swapped depending of the value of the $k^{\text{th}}$ bit. We use a conditional swap \texttt{CSWAP} to change the arguments of the above function while keeping the same body of the loop. \label{cswap} ... ... @@ -65,7 +66,7 @@ computing a \xcoord-only scalar multiplication (see \aref{alg:montgomery-ladder} \STATE $(Q,R) \leftarrow \texttt{CSWAP}((Q,R), k^{\text{th}}\text{ bit of }n)$ % \STATE $Q \leftarrow \texttt{xDBL}(Q)$ % \STATE $R \leftarrow \texttt{xADD}(x_P,Q,R)$ \STATE $(Q,R) \leftarrow \texttt{xladderstep}(x_P,Q,R)$ \STATE $(Q,R) \leftarrow \texttt{xDBL\&ADD}(x_P,Q,R)$ \STATE $(Q,R) \leftarrow \texttt{CSWAP}((Q,R), k^{\text{th}}\text{ bit of }n)$ \ENDFOR \RETURN $X_Q/Z_Q$ ... ...
 ... ... @@ -8,3 +8,36 @@ \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} Below we provide the reasons of the diff. \begin{itemize} \item line 6-7: We tell VST that \TNaCle{long long} are aligned on 8 bytes. \item line 13-20: This is change correspond to \TNaCle{car25519}. We remove the unused variable \TNaCle{i64 c}, we remove the undefined behavior as explained in \sref{sec:Conclusion}. \item line 24-29: The signature of \end{itemize} @@ We remove the undefined behavior and @@ simplify the carry propagation. @@ b is a mask of 64 bits. @@ For-loop indexes have to be int. @@ For-loop indexes have to be int. @@ b is a 64 bit mask. @@ Initialize m to simplify verification. @@ Computations in arguments @@ are not allowed in VST. @@ For-loop indexes have to be int. @@ gain 5 bytes. @@ x only needs gf. @@ For-loop indexes have to be int. @@ simplify
 ... ... @@ -350,6 +350,10 @@ literate= % identifierstyle=\color[rgb]{0,0,0}, delim=[l][\color{doc@lstdirective}]{\#}, numbers=left, % where to put the line numbers stepnumber=1, % step between two line numbers numberstyle=\tiny, % line number font size xleftmargin=5.0ex, literate= } ... ... @@ -361,13 +365,16 @@ literate= % \newcommand{\lstbg}[3][0pt]{{\fboxsep#1\colorbox{#2}{\strut #3}}} \lstdefinelanguage{diff}{ basicstyle=\ttfamily\small, % morecomment=[f][\lstbg{red!20}]<, % morecomment=[f][\lstbg{green!20}]>, morecomment=[f][\color{doc@lstidentifiers2}]-, morecomment=[f][\color{doc@lstfunctions}]+, morecomment=[f][\color{gray}\textit]{@@}, %morecomment=[f][\textit]{---}, %morecomment=[f][\textit]{+++}, numbers=left, % where to put the line numbers stepnumber=1, % step between two line numbers numberstyle=\tiny, % line number font size xleftmargin=5.0ex, % numbers=left, % numberstyle={\tiny \color{black}},% size of the numbers % numbersep=9pt, % this defines how far the numbers are from the text } % \lstset{} ... ... @@ -398,9 +405,6 @@ literate= showspaces=false, % show spaces adding particular underscores showstringspaces=false, % underline spaces within strings % numbers=left, % where to put the line numbers stepnumber=0, % step between two line numbers numberstyle=\small, % line number font size % captionpos=b, % set the caption position to `bottom' % ... ...
 --- tweetnacl.c +++ tweetnaclVerifiableC.c @@ -5,7 +5,7 @@ typedef unsigned char u8; @@ -6,5 +6,5 @@ typedef unsigned long u32; typedef unsigned long long u64; @@ We tell VST that long long @@ are aligned on 8 bytes. -typedef long long i64; +typedef long long i64 __attribute__((aligned(8))); typedef i64 gf[16]; extern void randombytes(u8 *,u64); @@ -273,18 +273,16 @@ @@ We remove the undefined behavior and @@ simplify the carry propagation. sv car25519(gf o) @@ -274,16 +274,14 @@ { int i; - i64 c; ... ... @@ -28,24 +21,17 @@ } } @@ b is a mask of 64 bits. -sv sel25519(gf p,gf q,int b) +sv sel25519(gf p,gf q,i64 b) { @@ For-loop indexes have to be int. - i64 t,i,c=~(b-1); + int i; + i64 t,c=~(b-1); FOR(i,16) { t= c&(p[i]^q[i]); p[i]^=t; @@ -294,9 +292,10 @@ @@ -295,7 +293,8 @@ sv pack25519(u8 *o,const gf n) { @@ For-loop indexes have to be int. @@ b is a 64 bit mask. @@ Initialize m to simplify verification. - int i,j,b; - gf m,t; - FOR(i,16) t[i]=n[i]; ... ... @@ -55,46 +41,32 @@ + set25519(t,n); car25519(t); car25519(t); car25519(t); @@ -309,7 +308,8 @@ m[15]=t[15]-0x7fff-((m[14]>>16)&1); @@ -310,5 +309,6 @@ b=(m[15]>>16)&1; m[14]&=0xffff; @@ Computations in arguments @@ are not allowed in VST. - sel25519(t,m,1-b); + b=1-b; + sel25519(t,m,b); } FOR(i,16) { o[2*i]=t[i]&0xff; @@ -353,7 +353,8 @@ @@ -354,5 +354,6 @@ sv M(gf o,const gf a,const gf b) { @@ For-loop indexes have to be int. - i64 i,j,t[31]; + int i,j; + i64 t[31]; FOR(i,31) t[i]=0; FOR(i,16) FOR(j,16) t[i+j]+=a[i]*b[j]; FOR(i,15) t[i]+=38*t[i+16]; @@ -371,7 +372,7 @@ { @@ -372,5 +373,5 @@ gf c; int a; @@ gain 5 bytes. - FOR(a,16) c[a]=i[a]; + set25519(c,i); for(a=253;a>=0;a--) { S(c,c); if(a!=2&&a!=4) M(c,c,i); @@ -394,8 +395,9 @@ int crypto_scalarmult(u8 *q,const u8 *n,const u8 *p) @@ -395,6 +396,7 @@ { u8 z[32]; @@ x only needs gf. @@ For-loop indexes have to be int. - i64 x[80],r,i; - gf a,b,c,d,e,f; + i64 r; ... ... @@ -102,12 +74,9 @@ + gf x,a,b,c,d,e,f; FOR(i,31) z[i]=n[i]; z[31]=(n[31]&127)|64; z[0]&=248; @@ -430,15 +432,9 @@ sel25519(a,b,r); @@ -431,13 +433,7 @@ sel25519(c,d,r); } @@ simplify - FOR(i,16) { - x[i+16]=a[i]; - x[i+32]=c[i]; ... ... @@ -122,4 +91,3 @@ + pack25519(q,a); return 0; }
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!