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

add more text

parent 00abef2b
\section{Introduction}
Implementing cryptographic primitives without any bugs is hard. While tests
provides a decent code coverage, they don't cover 100\% of the possible values.
Using the \textit{clightgen} tool from compcert \cite{Leroy-backend}, we can
generate the \textit{semantic version} (Clight\cite{Blazy-Leroy-Clight-09}) of
the C code. Using the Floyd–Hoare logic\cite{1969-Hoare} with the Verifiable
Software Toolchain (VST)\cite{2012-Appel} we can show that the semantic of the
program is equivalent to some functions in Coq. We can then prove that these
\textit{equivalent functions} do respect the semantic of the arithmetic.
\section{Curve25519 implementation}
\subsection{Implementation}
256 bits words are cut into limbs of 16 bits placed into 64 bits signed
containers.
\begin{lstlisting}[language=C]
typedef long long i64;
typedef i64 gf[16];
\end{lstlisting}
\begin{lstlisting}[language=C]
sv A(gf o,const gf a,const gf b) {
int 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);
}
sv car25519(gf o) {
int i;
i64 c;
FOR(i,16) {
o[i]+=(1LL<<16);
c=o[i]>>16;
o[(i+1)*(i<15)]+=c-1+37*(c-1)*(i==15);
o[i]-=c<<16;
}
}
\end{lstlisting}
\subsection{What need to be proven?}
\textbf{Soundness} and \textbf{Correctness}.
We show that TweetNaCl's code is \textbf{sound} also know as \textit{shape analysis} \ie
\begin{itemize}
\item absence of array out-of-bounds,
\textit{For each array access, VST requires to prove the range.}
\item absence of overflows/underflow.
\textit{for each operation, VST requires to prove that the resulting value are in ranges.}
\end{itemize}
We also show that TweetNaCl's code is \textbf{correct}:
\begin{itemize}
\item Curve25519 is correctly implemented
\item The number representation
\end{itemize}
\subsection{Correctness Theorem}
The soundness is implied by the functionnal definition of the theorem.
\section{Mathematical Model}
\textbf{ASK TIMMY}
\section{Number representation and C implementation}
\section{Related Works}
\begin{itemize}
\item HACL*
\item Proving SHA-256 and HMAC
\item \url{http://www.iis.sinica.edu.tw/~bywang/papers/ccs17.pdf}
\item \url{http://www.iis.sinica.edu.tw/~bywang/papers/ccs14.pdf}
\item \url{https://cryptojedi.org/crypto/#gfverif}
\item \url{https://cryptojedi.org/crypto/#verify25519}
\end{itemize}
\section{Using VST}
\subsection{The Trusted Base}
The soundness of our proof relies on a trusted base
, i.e. a foundation of specifications and implementations
that must stay correct with respect to the specifications.
\begin{itemize}
\item \textbf{Calculus of Inductive Construction} : The intuitionistic logic
used by Coq must be consistent in order to trust the proofs. We assumed that
the functional extensionality was also consistent with that logic.
$
\begin{array}{c}
\forall A\ B (f\ g : A \to B ),\\
( \forall x : A , f(x) = g(x) ) \implies f = g
\end{array}
$
\item \textbf{Specification, model...}
\item The last part of the trusted base is about the \textbf{Coq kernel}, the
\textbf{Ocaml compiler}, the \textbf{Ocaml Runtime} and the \textbf{CPU}.
These are common to all proofs done with this architecture \cite{2015-Appel,coq-faq}.
\end{itemize}
\subsection{Feelings of a VST user}
This approach is \textbf{slow}, \textbf{tedious} and \textbf{frustrating}.
The time cost way to big for such a proof and definitively not applicable for a
cryptographic engineer.
Necessity to prove everything at least 3 to 4 times.
Necessity to go back into your specification multiple times to refine your model.
e.g. prove \texttt{M(o,a,b)} later notice that you can have aliasing, need to redifine
your theorem to prove \texttt{M(o,a,a)} (\textit{squaring}) and other variants such as:
\texttt{M(a,a,b)} and \texttt{M(b,a,b)}.
Prove \texttt{M(o,a,b)} where o is a \texttt{list $\Z$} and then realize that
\texttt{o} can be a list of \textit{undefined}. Thus needs to reprove the above
theorem again.
The \texttt{forward} and \texttt{entailer} tactics are slow.
Specification and proofs does not need to be in the same file (as initially \textit{implied}
by the examples provided by the VST repository). Putting the specification of each
functions in separate file reduce the amount of dependencies. One does not need
to wait for the proof of \texttt{M(b,a,b)} to compile the proof of \texttt{crypto\_scalarmult(q,n,p)}.
This separation allows a high degree of parallelism during compilation \texttt{make -j},
greatly reducing the amount of time required.
Two years ago:
\url{https://www.imperialviolet.org/2014/09/11/moveprovers.html}
\url{https://www.imperialviolet.org/2014/09/07/provers.html}
curve25519.pdf: curve25519.tex collection.bib
FILES := $(wildcard *.tex) $(wildcard *.sty)
curve25519.pdf: $(FILES) collection.bib
latexmk -pdf curve25519.tex
.PHONY: clean
......
@STRING{LNCS = {LNCS}}
@STRING{SV = {Springer}}
@misc{ding2012firstdraft,
author = {Jintai Ding},
title = {New cryptographic constructions using generalized learning with errors problem},
howpublished = {{IACR} Cryptology ePrint Archive report 2012/387},
year = {2012},
note = {\url{http://eprint.iacr.org/2012/387}},
@article{1969-Hoare,
author = {C. A. R. Hoare},
title = {An Axiomatic Basis for Computer Programming},
journal = {Commun. ACM},
issue_date = {Oct. 1969},
volume = {12},
number = {10},
month = {oct},
year = {1969},
issn = {0001-0782},
pages = {576-580},
numpages = {5},
note = {\url{http://doi.acm.org/10.1145/363235.363259}},
url = {http://doi.acm.org/10.1145/363235.363259},
doi = {10.1145/363235.363259},
acmid = {363259},
publisher = {ACM}
}
@article{2007-Blazy-C-chronique,
author = {Sandrine Blazy},
title = {Comment gagner confiance en {C} ?},
journal = {Technique et Science Informatiques},
year = {2007},
volume = {26},
number = {9},
pages = {1195-1200},
note = {\url{http://hal.inria.fr/inria-00292049/}},
hal = {http://hal.inria.fr/inria-00292049/},
pubkind = {journal-fr-mono}
}
@article{Leroy-backend,
author = {Xavier Leroy},
title = {A formally verified compiler back-end},
journal = {Journal of Automated Reasoning},
volume = {43},
number = {4},
pages = {363--446},
year = {2009},
note = {\url{http://gallium.inria.fr/~xleroy/publi/compcert-backend.pdf}},
urlpublisher = {http://dx.doi.org/10.1007/s10817-009-9155-4},
hal = {http://hal.inria.fr/inria-00360768/},
pubkind = {journal-int-mono}
}
@inproceedings{Bat68,
author = {Kenneth E. Batcher},
title = {Sorting networks and their applications},
booktitle = {AFIPS conference proceedings, volume 32: 1968 Spring Joint Computer Conference},
publisher = {Thompson Book Company},
year = {1968},
pages = {307--314},
note = {\url{http://www.cs.kent.edu/~batcher/conf.html}},
@article{Blazy-Leroy-Clight-09,
author = {Sandrine Blazy and Xavier Leroy},
title = {Mechanized semantics for the {Clight}
subset of the {C} language},
year = {2009},
journal = {Journal of Automated Reasoning},
volume = {43},
number = {3},
pages = {263-288},
note = {\url{http://gallium.inria.fr/~xleroy/publi/Clight.pdf}},
hal = {http://hal.inria.fr/inria-00352524/},
urlpublisher = {http://dx.doi.org/10.1007/s10817-009-9148-3}
}
@misc{Bur16,
author = {Jeff Burdges},
title = {Post-Quantum Secure Hybrid Handshake Based on {NewHope}},
howpublished = {Posting to the tor-dev mailing list},
year = {2016},
note = {\url{https://lists.torproject.org/pipermail/tor-dev/2016-May/010886.html}},
@inproceedings{ BGJ+15,
author = {Daniel J. Bernstein and Bernard van Gastel and Wesley Janssen and Tanja Lange and Peter Schwabe and Sjaak Smetsers},
title = {{TweetNaCl}: A crypto library in 100 tweets},
booktitle = {Progress in Cryptology -- {LATINCRYPT 2014}},
editor = {Diego Aranha and Alfred Menezes},
publisher = SV,
series = LNCS,
volume = {8895},
year = {2015},
pages = {64--83},
note = {Document ID: c74b5bbf605ba02ad8d9e49f04aca9a2, \url{http://cryptojedi.org/papers/\#tweetnacl}},
}
@misc{Ang16,
author = {Yawning Angel},
title = {Post-Quantum Secure Hybrid Handshake Based on {NewHope}},
howpublished = {Posting to the tor-dev mailing list},
year = {2016},
note = {\url{https://lists.torproject.org/pipermail/tor-dev/2016-May/010896.html}},
VeriSmall: Verified Smallfoot Shape Analysis, by Andrew W. Appel. In CPP 2011: First International Conference on Certified Programs and Proofs, Springer LNCS 7086, pp. 231-246, December 2011.
@inproceedings{2012-Appel,
author = {Andrew W. Appel},
title = {Verified Software Toolchain},
booktitle = {{NASA} Formal Methods - 4th International Symposium, {NFM} 2012, Norfolk,
VA, USA, April 3-5, 2012. Proceedings},
editor = {Alwyn Goodloe and Suzette Person},
publisher = SV,
series = LNCS,
volume = {7226},
year = {2012},
pages = {2},
note = {\url{https://doi.org/10.1007/978-3-642-28891-3_2}},
url = {https://doi.org/10.1007/978-3-642-28891-3_2},
doi = {10.1007/978-3-642-28891-3_2},
}
@misc{ADPS15,
author = {Erdem Alkim and L{\'e}o Ducas and Thomas Pöppelmann and Peter Schwabe },
title = {Post-quantum key exchange -- a new hope},
howpublished = {{IACR} Cryptology ePrint Archive report 2015/1092},
@article{2015-Appel,
author = {Andrew W. Appel},
title = {Verification of a Cryptographic Primitive: SHA-256},
journal = {ACM Trans. Program. Lang. Syst.},
issue_date = {April 2015},
volume = {37},
number = {2},
month = apr,
year = {2015},
note = {\url{https://eprint.iacr.org/2015/1092/20160329:201913}},
issn = {0164-0925},
pages = {7:1--7:31},
articleno = {7},
numpages = {31},
note = {\url{http://doi.acm.org/10.1145/2701415}},
url = {http://doi.acm.org/10.1145/2701415},
doi = {10.1145/2701415},
acmid = {2701415},
publisher = {ACM},
}
@misc{BCLV16,
author = {Daniel J. Bernstein and Chitchanok Chuengsatiansup and Tanja Lange and Christine van Vredendaal},
title = {{NTRU} {P}rime},
howpublished = {{IACR} Cryptology ePrint Archive report 2016/461},
year = {2016},
note = {\url{https://eprint.iacr.org/2016/461}},
@misc{coq-faq,
title = {{The Coq Proof Assistant} -- {Frequently Asked Questions}},
note = {\url{https://coq.inria.fr/faq}}
}
@misc{PLP16,
author = {Rafael del Pino and Vadim Lyubashevsky and David Pointcheval },
title = {The Whole is Less than the Sum of its Parts: Constructing More Efficient Lattice-Based {AKEs}},
howpublished = {{IACR} Cryptology ePrint Archive report 2016/435},
year = {2016},
note = {\url{https://eprint.iacr.org/2016/435}},
}
@misc{LN16,
author = {Patrick Longa and Michael Naehrig},
title = {Speeding up the Number Theoretic Transform for Faster Ideal Lattice-Based Cryptography},
howpublished = {{IACR} Cryptology ePrint Archive report 2016/504},
year = {2016},
note = {\url{https://eprint.iacr.org/2016/504}},
}
@misc{GS16,
author = {Shay Gueron and Fabian Schlieker},
title = {Speeding up {R-LWE} post-quantum key exchange},
howpublished = {{IACR} Cryptology ePrint Archive report 2016/467},
year = {2016},
note = {\url{https://eprint.iacr.org/2016/467}},
}
@misc{BSV15,
author = {Daniel J. Bernstein and Peter Schwabe and Gilles Van Assche},
......@@ -94,7 +141,7 @@
title = {Fast prime field elliptic-curve cryptography with 256-bit primes},
journal = {Journal of Cryptographic Engineering},
volume = {5},
number = {2},
number = {2},
year = {2014},
pages = {141--151},
note = {\url{https://eprint.iacr.org/2013/816/}},
......@@ -206,7 +253,7 @@
@inproceedings{BCLS14,
author = {Daniel J. Bernstein and Chitchanok Chuengsatiansup and Tanja Lange and Peter Schwabe},
title = {Kummer strikes back: new {DH} speed records},
booktitle = {Advances in Cryptology -- {EUROCRYPT 2015}},
booktitle = {Advances in Cryptology -- {EUROCRYPT 2015}},
editor = {Tetsu Iwata and Palash Sarkar},
publisher = SV,
series = LNCS,
......@@ -223,7 +270,7 @@
series = {AFIPS Proceedings},
volume = {29},
year = {1966},
pages = {563--578},
pages = {563--578},
note = {\url{http://cis.rit.edu/class/simg716/FFT_Fun_Profit.pdf}},
}
......@@ -516,7 +563,7 @@
}
@inproceedings{CFN+14,
author = {Stephen Checkoway and Matthew Fredrikson and Ruben Niederhagen and Adam Everspaugh and Matthew Green and
author = {Stephen Checkoway and Matthew Fredrikson and Ruben Niederhagen and Adam Everspaugh and Matthew Green and
Tanja Lange and Thomas Ristenpart and Daniel J. Bernstein and Jake Maskiewicz and Hovav Shacham},
title = {On the practical exploitability of {Dual EC} in {TLS} implementations},
booktitle = {Proceedings of the 23rd USENIX security symposium},
......@@ -596,11 +643,11 @@
@inproceedings{dagdelen2013fiatquantum,
author = {{\"{O}}zg{\"{u}}r Dagdelen and Marc Fischlin and Tommaso Gagliardoni},
title = {The {Fiat-Shamir} Transformation in a Quantum World},
booktitle = {Advances in Cryptology - {ASIACRYPT 2013}},
booktitle = {Advances in Cryptology - {ASIACRYPT 2013}},
editor = {Kazue Sako and Palash Sarkar},
series = LNCS,
publisher = SV,
volume = {8270},
volume = {8270},
year = {2013},
pages = {62--81},
note = {\url{https://eprint.iacr.org/2013/245/}},
......@@ -631,7 +678,7 @@
pages = {512--529},
note = {\url{http://www.iacr.org/archive/ches2012/74280511/74280511.pdf}},
}
@book{ChGeFftBlackBox00,
author = {Eleanor Chu and Alan George},
title = {Inside the {FFT} Black Box Serial and Parallel Fast {Fourier} Transform Algorithms},
......@@ -728,7 +775,7 @@
pages = {169--178},
note = {\url{https://www.cs.cmu.edu/~odonnell/hits09/gentry-homomorphic-encryption.pdf}},
}
@misc{cade2013fplll,
author = {Cad{\'e}, David and Pujol, Xavier and Stehl{\'e}, Damien},
title = {fplll 4.0.4},
......@@ -788,7 +835,7 @@
pages = {210--268},
note = {\url{http://www-personal.umich.edu/~romanv/papers/non-asymptotic-rmt-plain.pdf}}
}
@article{regev2009lwe,
author = {Oded Regev},
title = {On lattices, learning with errors, random linear codes, and cryptography},
......@@ -909,7 +956,7 @@
volume = {1163},
year = {1996},
pages = {382--394},
note = {\url{http://oai.cwi.nl/oai/asset/1940/1940A.pdf}},
note = {\url{http://oai.cwi.nl/oai/asset/1940/1940A.pdf}},
}
@inproceedings{brakerski2013classical,
......@@ -1028,4 +1075,3 @@
year = {2016},
note = {\url{http://csrc.nist.gov/publications/drafts/nistir-8105/nistir_8105_draft.pdf}}
}
......@@ -13,21 +13,16 @@
% the .sty file from the LaTeX source template, so that people can
% more easily include the .sty file into an existing document. Also
% changed to more closely follow the style guidelines as represented
% by the Word sample file.
% by the Word sample file.
% Note that since 2010, USENIX does not require endnotes. If you want
% foot of page notes, don't include the endnotes package in the
% foot of page notes, don't include the endnotes package in the
% usepackage command, below.
% This version uses the latex2e styles, not the very ancient 2.09 stuff.
\documentclass[letterpaper,twocolumn,10pt]{article}
\usepackage{usenix,epsfig}
%\usepackage{etex}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage[pdf]{pstricks}
\usepackage{multido}
\usepackage{setup}
\newif\ifpublic
\publictrue
......@@ -35,45 +30,6 @@
\newif\iffull
\fulltrue
\usepackage{amsfonts,amsmath,amscd,amssymb,array}
\usepackage{type1cm}
\newcommand{\lstsize}{\fontsize{8.5pt}{8.5pt}\selectfont}
\usepackage{algorithm}
\usepackage{algorithmic}
\usepackage{xcolor}
\definecolor{linkcolor}{rgb}{0.65,0,0}
\definecolor{citecolor}{rgb}{0,0.65,0}
\definecolor{urlcolor}{rgb}{0,0,0.65}
\usepackage[colorlinks=true, backref=page, linkcolor=linkcolor, urlcolor=urlcolor, citecolor=citecolor]{hyperref}
%\usepackage{breakurl}
\usepackage{ctable}
\usepackage{cite}
\usepackage{dsfont}
\usepackage{xspace}
\usepackage{subfig}
\usepackage{float}
\floatstyle{ruled}
\newfloat{Listing}{htb}{lst}
\floatstyle{plain}
\newfloat{Protocol}{htb}{proto}
\newcounter{subListing}
\newcounter{subListing@save}
\renewcommand{\thesubListing}{\alph{subListing}}
\renewcommand{\tabcolsep}{4pt}
\def\subheading#1{\medskip\noindent{\boldmath\textbf{#1}}~\ignorespaces}
\newcommand{\todo}[1]{\marginpar{\baselineskip0ex\rule{2,5cm}{0.5pt}\\[0ex]{\tiny\textsf{#1}}}}
\input{macros}
\begin{document}
......@@ -108,7 +64,12 @@ Date: somewhen in 2018.}
By using the Coq formal proof assistant with the VST library, we prove the
soundness and correctness of TweetNaCl's Curve25519 implementation.
%\input{intro}
\input{1_Introduction.tex}
\input{2_Implementation.tex}
\input{3_Maths.tex}
\input{4_NumberAndImplementation.tex}
\input{5_RelatedWorks.tex}
\input{6_UsingVST.tex}
\vspace*{1cm}
{\footnotesize \bibliographystyle{acm}
......@@ -119,10 +80,3 @@ soundness and correctness of TweetNaCl's Curve25519 implementation.
\end{document}
......@@ -34,60 +34,11 @@
\newcommand{\LDDecode}{\algo{Decode}}
\usepackage{soul}\let\strikethrough\st\let\st\undefined
\newcommand{\PeiktertROUND}[1]{\langle #1 \rangle_2}
\newcommand{\PeiktertRec}{\textsf{rec}\xspace}
\newcommand{\PeiktertDbl}{\textsf{dbl}\xspace}
\newcommand{\PeiktertALICE}{Alice}
\newcommand{\PeiktertBOB}{Bob}
\newcommand{\NewHope}{\textsc{NewHope}\xspace}
\newcommand{\JarJar}{\textsc{JarJar}\xspace}
\newcommand{\NewhopeALICE}{Alice}
\newcommand{\NewhopeBOB}{Bob}
\newcommand{\NewhopeSERVER}{server}
\newcommand{\NewhopeCLIENT}{client}
\newcommand{\NewhopeRAND}{\{0,1\}^{256}}
\newcommand{\NewhopeGENA}{\textsf{prg}\xspace}
\newcommand{\NewhopeSEED}{seed\xspace}
\newcommand{\NewhopeHASHXOF}{\textsf{SHAKE-128}\xspace}
\newcommand{\NewhopePARSE}{\textsf{Parse}\xspace}
\newcommand{\NewhopeHASH}{\textsf{SHA3-256}\xspace}
\newcommand{\NewhopeREC}{{\textsf{Rec}}\xspace}
\newcommand{\NewhopeHelpREC}{{\textsf{HelpRec}}\xspace}
\newcommand{\NewhopeSENDA}{{\textsf{encodeA}}\xspace}
\newcommand{\NewhopeSENDB}{{\textsf{encodeB}}\xspace}
\newcommand{\NewhopeRECVA}{{\textsf{decodeA}}\xspace}
\newcommand{\NewhopeRECVB}{{\textsf{decodeB}}\xspace}
\newcommand{\NewhopeLDDECODE}{\textsf{Decode}\xspace}
\newcommand{\NewhopeValuek}{16}
\newcommand{\NewhopeValuekhalf}{8}
\newcommand{\NewhopeErrorDist}{\psi^n_{\NewhopeValuek}}
\newcommand{\NewhopeErrorDistOne}{\psi_{\NewhopeValuek}}
\newcommand{\NewhopeK}{\nu}
\newcommand{\NewhopeKey}{\mu}
\newcommand{\NTT}{\mbox{\textsf{NTT}}\xspace}
\newcommand{\INVNTT}{\ensuremath{\mbox{\textsf{NTT}}^{-1}}\xspace}
\newcommand{\pw}{\circ}
\newcommand{\NewhopeRing}{\ensuremath{\mathcal{R}_q}}
\usepackage{soul}\let\strikethrough\st\let\st\undefined
\newcommand{\T}{L}
%\newcommand{\F}{\mathbb{Z}}
\newcommand{\Z}{\mathbb{Z}}
\newcommand{\ZZ}{\mathbb{Z}}
\newcommand{\corr}{\,\hat{=}\,}
......@@ -143,9 +94,6 @@
\newcommand{\roundd}[1]{\ensuremath{\lfloor #1 \rceil_d}}
\newcommand{\norm}[1]{\ensuremath{||#1||}}
%\newcommand{\KeyGen}{\ensuremath{\mathsf{KeyGen_{BG}}}}
%\newcommand{\Sign}{\ensuremath{\mathsf{Sign_{BG}}}}
%\newcommand{\Verify}{\ensuremath{\mathsf{Verify_{BG}}}}
\newcommand{\KeyGen}{\keygen}
\newcommand{\Sign}{\sign}
\newcommand{\Verify}{\verify}
......@@ -245,9 +193,6 @@
\newcommand{\Spo}{{\bf S}}
\newcommand{\Ypo}{{\bf Y}}
\newcommand{\NTTPSI}{{\gamma}}
\newcommand{\algo}[1]{\textsf{#1}}
\newcommand{\PeikertDBL}{\algo{dbl}}
......@@ -256,3 +201,4 @@
\newcommand{\PowMul}{{\text{\sf PowMul}}}
\newcommand{\PowMulPsi}{{\text{\sf PowMul}_{\psi}}}
\newcommand{\ie}{{\it i.e.}}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage[pdf]{pstricks}
\usepackage{multido}
% \usepackage{etex}
\usepackage{amsfonts,amsmath,amscd,amscd,amssymb,array}
\usepackage{type1cm}
\newcommand{\lstsize}{\fontsize{8.5pt}{8.5pt}\selectfont}
\usepackage{algorithm, algorithmic}