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

figure for proof

parent 39d97c51
...@@ -147,6 +147,21 @@ note = {\url{https://books.google.nl/books?id=T_ShHENlqBAC&lpg=PR4&pg=PP1#v=o ...@@ -147,6 +147,21 @@ note = {\url{https://books.google.nl/books?id=T_ShHENlqBAC&lpg=PR4&pg=PP1#v=o
note = {Document ID: 5f6fc69cc5a319aecba43760c56fab04, \url{http://cryptojedi.org/papers/\#coolnacl}}, note = {Document ID: 5f6fc69cc5a319aecba43760c56fab04, \url{http://cryptojedi.org/papers/\#coolnacl}},
} }
@article{cao2018vst-floyd,
author = {Qinxiang Cao and Lennart Beringer and Samuel Gruetter and Josiah Dodds and Andrew W. Appel},
year = {2018},
title = {VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs},
journal = {Journal of Automated Reasoning},
issn = {0168-7433},
doi = {10.1007/s10817-018-9457-5},
volume = {61},
month = {6},
pages = {367--422},
number = {1-4},
url = {https://doi.org/10.1007/s10817-018-9457-5},
abstract = {The Verified Software Toolchain builds foundational machine-checked proofs of the functional correctness of C programs. Its program logic, Verifiable C, is a shallowly embedded higher-order separation Hoare logic which is proved sound in Coq with respect to the operational semantics of CompCert Clight. This paper introduces VST-Floyd, a verification assistant which offers a set of semiautomatic tactics helping users build functional correctness proofs for C programs using Verifiable C.}
}
@inproceedings{Chen2014VerifyingCS, @inproceedings{Chen2014VerifyingCS,
title = {Verifying Curve25519 Software}, title = {Verifying Curve25519 Software},
author = {Yu-Fang Chen and Chang-Hong Hsu and Hsin-Hung Lin and Peter Schwabe and Ming-Hsien Tsai and Bow-Yaw Wang and Bo-Yin Yang and Shang-Yi Yang}, author = {Yu-Fang Chen and Chang-Hong Hsu and Hsin-Hung Lin and Peter Schwabe and Ming-Hsien Tsai and Bow-Yaw Wang and Bo-Yin Yang and Shang-Yi Yang},
...@@ -256,6 +271,16 @@ note = {\url{https://books.google.nl/books?id=T_ShHENlqBAC&lpg=PR4&pg=PP1#v=o ...@@ -256,6 +271,16 @@ note = {\url{https://books.google.nl/books?id=T_ShHENlqBAC&lpg=PR4&pg=PP1#v=o
note = {\url{https://www.ams.org/notices/200811/tx081101382p.pdf}} note = {\url{https://www.ams.org/notices/200811/tx081101382p.pdf}}
} }
@incollection{Howard1995-HOWTFN,
title = {The Formul\ae-as-Types Notion of Construction},
author = {W. A. Howard},
booktitle = {The Curry-Howard Isomorphism},
year = {1995},
editor = {Philippe De Groote},
publisher = {Academia},
note = {\url{https://www.cs.cmu.edu/~crary/819-f09/Howard80.pdf}}
}
@article{Leroy-backend, @article{Leroy-backend,
author = {Xavier Leroy}, author = {Xavier Leroy},
title = {A formally verified compiler back-end}, title = {A formally verified compiler back-end},
......
...@@ -7,6 +7,11 @@ Clight description of TweetNaCl and Coq functions producing similar behaviors. ...@@ -7,6 +7,11 @@ Clight description of TweetNaCl and Coq functions producing similar behaviors.
\todo{SUBSECTION?} \todo{SUBSECTION?}
\begin{figure}[h]
\include{tikz/proof}
\caption{Overview construction of the proof}
\label{tk:ProofOverview}
\end{figure}
Verifying \texttt{crypto\_scalarmult} also implies to verify all the functions Verifying \texttt{crypto\_scalarmult} also implies to verify all the functions
......
...@@ -46,169 +46,174 @@ typedef i64 gf[16]; ...@@ -46,169 +46,174 @@ typedef i64 gf[16];
Notice this does not guaranty a unique representation of each number. i.e.\\ Notice this does not guaranty a unique representation of each number. i.e.\\
$\exists x,y \in$ \TNaCle{gf} such that $\exists x,y \in$ \TNaCle{gf} such that
\vspace{-0.25cm} \vspace{-0.25cm}
$$x \neq y\ \ \land\ \ x \equiv y \pmod{2^{255}-19}$$ $$x \neq y\ \ \land\ \ x \equiv y \pmod{2^{255}-19}$$
On the other hand it allows simple definitions of addition (\texttt{A}), On the other hand it allows simple definitions of addition (\texttt{A}),
substraction (\texttt{Z}), and school-book multiplication (\texttt{M}). substraction (\texttt{Z}), and school-book multiplication (\texttt{M}).
% and squaring (\texttt{S}). % and squaring (\texttt{S}).
\begin{lstlisting}[language=Ctweetnacl] \begin{lstlisting}[language=Ctweetnacl]
sv A(gf o,const gf a,const gf b) { sv A(gf o,const gf a,const gf b) {
int i; int i;
FOR(i,16) o[i]=a[i]+b[i]; FOR(i,16) o[i]=a[i]+b[i];
} }
sv Z(gf o,const gf a,const gf b) { sv Z(gf o,const gf a,const gf b) {
int i; int i;
FOR(i,16) o[i]=a[i]-b[i]; FOR(i,16) o[i]=a[i]-b[i];
} }
sv M(gf o,const gf a,const gf b) {
i64 i,j,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];
FOR(i,16) o[i]=t[i];
car25519(o);
car25519(o);
}
\end{lstlisting}
sv M(gf o,const gf a,const gf b) { To avoid overflows, carries are propagated by the \texttt{car25519} function.
i64 i,j,t[31]; \begin{lstlisting}[language=Ctweetnacl]
FOR(i,31) t[i]=0; sv car25519(gf o)
FOR(i,16) FOR(j,16) t[i+j]+=a[i]*b[j]; {
FOR(i,15) t[i]+=38*t[i+16]; int i;
FOR(i,16) o[i]=t[i]; FOR(i,16) {
car25519(o); o[(i+1)%16]+=(i<15?1:38)*(o[i]>>16);
car25519(o); o[i]&=0xffff;
} }
\end{lstlisting} }
\end{lstlisting}
To avoid overflows, carries are propagated by the \texttt{car25519} function. % In order to simplify the verification of this function,
\begin{lstlisting}[language=Ctweetnacl] % we extract the last step of the loop $i = 15$.
sv car25519(gf o) % \begin{lstlisting}[language=Ctweetnacl]
{ % sv car25519(gf o)
int i; % {
FOR(i,16) { % int i;
o[(i+1)%16]+=(i<15?1:38)*(o[i]>>16); % i64 c;
o[i]&=0xffff; % FOR(i,15) {
% o[(i+1)]+=o[i]>>16;
% o[i]&=0xffff;
% }
% o[0]+=38*(o[15]>>16);
% o[15]&=0xffff;
% }
% \end{lstlisting}
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}$.
Then computes a modulo reduction by $\p$ using iterative substraction and
conditional swapping. This guarantees a unique representation in $\Zfield$.
After which each 16-bit limbs are splitted into 8-bit limbs.
\begin{lstlisting}[language=Ctweetnacl]
sv pack25519(u8 *o,const gf n)
{
int i,j;
i64 b;
gf t,m={0};
set25519(t,n);
car25519(t);
car25519(t);
car25519(t);
FOR(j,2) {
m[0]=t[0]- 0xffed;
for(i=1;i<15;i++) {
m[i]=t[i]-0xffff-((m[i-1]>>16)&1);
m[i-1]&=0xffff;
} }
m[15]=t[15]-0x7fff-((m[14]>>16)&1);
m[14]&=0xffff;
b=1-((m[15]>>16)&1);
sel25519(t,m,b);
} }
\end{lstlisting} FOR(i,16) {
% In order to simplify the verification of this function, o[2*i]=t[i]&0xff;
% we extract the last step of the loop $i = 15$. o[2*i+1]=t[i]>>8;
% \begin{lstlisting}[language=Ctweetnacl]
% sv car25519(gf o)
% {
% int i;
% i64 c;
% FOR(i,15) {
% o[(i+1)]+=o[i]>>16;
% o[i]&=0xffff;
% }
% o[0]+=38*(o[15]>>16);
% o[15]&=0xffff;
% }
% \end{lstlisting}
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}$.
Then computes a modulo reduction by $\p$ using iterative substraction and
conditional swapping. This guarantees a unique representation in $\Zfield$.
After which each 16-bit limbs are splitted into 8-bit limbs.
\begin{lstlisting}[language=Ctweetnacl]
sv pack25519(u8 *o,const gf n)
{
int i,j;
i64 b;
gf t,m={0};
set25519(t,n);
car25519(t);
car25519(t);
car25519(t);
FOR(j,2) {
m[0]=t[0]- 0xffed;
for(i=1;i<15;i++) {
m[i]=t[i]-0xffff-((m[i-1]>>16)&1);
m[i-1]&=0xffff;
}
m[15]=t[15]-0x7fff-((m[14]>>16)&1);
m[14]&=0xffff;
b=1-((m[15]>>16)&1);
sel25519(t,m,b);
}
FOR(i,16) {
o[2*i]=t[i]&0xff;
o[2*i+1]=t[i]>>8;
}
} }
\end{lstlisting} }
\end{lstlisting}
\subheading{The Montgomery ladder}
\subheading{The Montgomery ladder}
\todo{How do we describe the ladder here ? Do we use the description by Timmy ? In order to compute scalar multiplications, X25519 uses the Montgomery
Do we use the simpler description in the RFC ?} $x$-coordinate double-and-add formulas.
First extract and clamp the value of $n$. Then unpack the value of $p$.
The \strikethrough{full ladder} is defined as follow. As per RFC~7748~\cite{rfc7748}, set its most significant bit to 0.
First extract and clamp the value of $n$. Then unpack the value of $p$. Finally compute the Montgomery ladder over the clamped $n$ and $p$,
As per RFC~7748~\cite{rfc7748}, set its most significant bit to 0. pack the result into $q$.
Compute the Montgomery ladder over the clamped $n$ and $p$, pack the result into $q$. \begin{lstlisting}[language=Ctweetnacl]
\begin{lstlisting}[language=Ctweetnacl] int crypto_scalarmult(u8 *q,
int crypto_scalarmult(u8 *q, const u8 *n,
const u8 *n, const u8 *p)
const u8 *p) {
{ u8 z[32];
u8 z[32]; i64 r;
i64 r; int i;
int i; gf x,a,b,c,d,e,f;
gf x,a,b,c,d,e,f; FOR(i,31) z[i]=n[i];
FOR(i,31) z[i]=n[i]; z[31]=(n[31]&127)|64;
z[31]=(n[31]&127)|64; z[0]&=248;
z[0]&=248; unpack25519(x,p);
unpack25519(x,p); FOR(i,16) {
FOR(i,16) { b[i]=x[i];
b[i]=x[i]; d[i]=a[i]=c[i]=0;
d[i]=a[i]=c[i]=0; }
} a[0]=d[0]=1;
a[0]=d[0]=1; for(i=254;i>=0;--i) {
for(i=254;i>=0;--i) { r=(z[i>>3]>>(i&7))&1;
r=(z[i>>3]>>(i&7))&1; sel25519(a,b,r);
sel25519(a,b,r); sel25519(c,d,r);
sel25519(c,d,r); A(e,a,c);
A(e,a,c); Z(a,a,c);
Z(a,a,c); A(c,b,d);
A(c,b,d); Z(b,b,d);
Z(b,b,d); S(d,e);
S(d,e); S(f,a);
S(f,a); M(a,c,a);
M(a,c,a); M(c,b,e);
M(c,b,e); A(e,a,c);
A(e,a,c); Z(a,a,c);
Z(a,a,c); S(b,a);
S(b,a); Z(c,d,f);
Z(c,d,f); M(a,c,_121665);
M(a,c,_121665); A(a,a,d);
A(a,a,d); M(c,c,a);
M(c,c,a); M(a,d,f);
M(a,d,f); M(d,b,x);
M(d,b,x); S(b,e);
S(b,e); sel25519(a,b,r);
sel25519(a,b,r); sel25519(c,d,r);
sel25519(c,d,r);
}
inv25519(c,c);
M(a,a,c);
pack25519(q,a);
return 0;
} }
\end{lstlisting} inv25519(c,c);
M(a,a,c);
pack25519(q,a);
return 0;
}
\end{lstlisting}
\subsection{Coq and VST} \subsection{Coq and VST}
\label{preliminaries:C} \label{preliminaries:C}
\todo{Describe Coq}
\todo{Describe VST} Coq~\cite{coq-faq} is an interactive theorem prover. It provides an expressive
formal language to write mathematical definitions, algorithms and theorems coupled
with their proofs. As opposed to other systems such as F*~\cite{DBLP:journals/corr/BhargavanDFHPRR17},
Coq does not use a SMT solver to discharge its proof obligations but requires
the user to specify exactly which lemmas, hypothesis to apply and uses its type
system to verify their application~\cite{Howard1995-HOWTFN}.
It also provides some automations tools so that the user can apply and try multiple
proofs techniques in an efficient manner.
The Verified Software Toolchain is \cite{cao2018vst-floyd}.
\todo{Describe Hoare Logic} \todo{Describe Hoare Logic}
......
\begin{tikzpicture}[textstyle/.style={black, anchor= south west, align=center, minimum height=0.45cm, text centered, font=\scriptsize}]
% C code
\begin{scope}[yshift=0 cm,xshift=0 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};
\draw (0.675,-0.5) node[textstyle, anchor=center] {\texttt{Prog}};
\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]
\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};
\draw (0.675,-0.5) node[textstyle, anchor=center] {\texttt{Prog}};
\draw (1.25,-1.25) node[textstyle, anchor = south east] {\color{doc@lstfunctions}{.V}};
\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,-2) -- (0, -2) -- cycle;
\draw (0.3,-0.05) node[textstyle] {Proof};
\draw (1.25,-1) node[textstyle, anchor=center] {\{Pre\} \texttt{Prog} \{Post\}};
\draw (2.5,-2) node[textstyle, anchor = south east] {\color{doc@lstfunctions}{\checkmark}};
\end{scope}
% VST Spec
\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] {
Pre:\\
~~$n$, $P$\\
Post:\\
~~\texttt{CSM}$(n,P)$};
\end{scope}
% Definition of CSM
\begin{scope}[yshift=-6 cm,xshift=0 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] {Definition};
\draw (1,-1) node[textstyle, anchor=center] {\texttt{CSM}};
\end{scope}
% Spec of Curve nP
\begin{scope}[yshift=-9 cm,xshift=0 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] {Definition};
\draw (1,-1) node[textstyle, anchor=center] {$[n]P$};
\end{scope}
% Correctness Theorem
\begin{scope}[yshift=-7 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,-2) -- (0, -2) -- cycle;
\draw (0.3,-0.05) node[textstyle] {Proof};
\draw (2.5,-2) node[textstyle, anchor = south east] {\color{doc@lstfunctions}{\checkmark}};
\draw (1.25,-1) node[textstyle, anchor=center] {Pre $\implies$\\$\text{\texttt{CSM}}(n,P) = [n]P$};
\end{scope}
\draw [very thick, ->] (1.25,-0.5) -- (2.5, -0.5);
\draw [very thick, ->] (3.75,-0.5) -- (6, -1);
\draw [very thick, ->] (5,-4) -- (6.5, -2);
\draw [very thick, ->] (2,-6.5) -- (3.5, -5);
\draw [very thick, ->] (2,-7.5) -- (6, -7.75);
\draw [very thick, ->] (2,-10) -- (6, -8.25);
\end{tikzpicture}
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